@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00214524, author = {伴野, 良太郎 and 松岡, 航太郎 and 松本, 直樹 and Song, Bian and 和賀, 正樹 and 末永, 幸平 and Ryotaro, Banno and Kotaro, Matsuoka and Naoki, Matsumoto and Song, Bian and Masaki, Waga and Kohei, Suenaga}, book = {コンピュータセキュリティシンポジウム2021論文集}, month = {Oct}, note = {本研究では,Alice が Bob にデータを提供し,Bob が Alice のデータに対して線形時相論理(LTL)によって 記述された仕様を用いてオンラインモニタリングを行う際に,Alice のデータやモニタリング結果を Bob から秘匿し, また Bob の仕様を Alice から秘匿するプロトコル(秘匿 LTL オンラインモニタリング)を提案する.我々の知る限りにおいて,本手法は秘匿 LTL オンラインモニタリングを行う初めてのプロトコルである.本研究では,LTL 式を変換し得られた DFA を,完全準同型暗号の一種である TFHE を用いて実行する.その手法として,(i) 入力を末尾から用いる既存のオフラインアルゴリズムを DFA を反転させることでオンラインの設定に転用する手法,及び (ii) DFA の現状態を暗号文として保持し,各入力によって起こる状態の遷移を TFHE で可能な操作を用いて暗号文上で行う手法の 2 つを提案した.またケーススタディとして,血糖値のモニタリングを行う LTL 式と,1 型糖尿病患者のシミュレーションデータを用い,値の計測間隔である 1 分よりも速く各値の処理を行えることを確認した., We propose a protocol to achieve oblivious Linear Temporal Logic (LTL) online monitoring. Under an oblivious LTL monitoring setting, Alice holds private data, and Bob monitors her data with private specification described by LTL. With an oblivious LTL protocol, we can prevent Bob from learning the data and the monitoring results from Alice, while also guaranteeing that Alice knows nothing about the specification of Bob. To the best of our knowledge, this is the first privacy-preserving protocol for LTL online monitoring. We first convert the LTL formula to a DFA. Then, the DFA is evaluated over TFHE, one kind of fully homomorphic encryption schemes. We propose two implementations: i) we tweak the existing offline algorithm to read the inputs from back to front by reversing the DFA; and ii) we keep the current state of the DFA as ciphertexts, and perform state transitions with homomorphic operations.}, pages = {922--929}, publisher = {情報処理学会}, title = {完全準同型暗号を用いた秘匿LTLオンラインモニタリング}, year = {2021} }