TY - GEN
T1 - Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
AU - Banno, Ryotaro
AU - Matsuoka, Kotaro
AU - Matsumoto, Naoki
AU - Bian, Song
AU - Waga, Masaki
AU - Suenaga, Kohei
N1 - Publisher Copyright:
© 2022, The Author(s).
PY - 2022
Y1 - 2022
N2 - In many Internet of Things (IoT) applications, data sensed by an IoT device are continuously sent to the server and monitored against a specification. Since the data often contain sensitive information, and the monitored specification is usually proprietary, both must be kept private from the other end. We propose a protocol to conduct oblivious online monitoring—online monitoring conducted without revealing the private information of each party to the other—against a safety LTL specification. In our protocol, we first convert a safety LTL formula into a DFA and conduct online monitoring with the DFA. Based on fully homomorphic encryption (FHE), we propose two online algorithms (Reverse and Block) to run a DFA obliviously. We prove the correctness and security of our entire protocol. We also show the scalability of our algorithms theoretically and empirically. Our case study shows that our algorithms are fast enough to monitor blood glucose levels online, demonstrating our protocol’s practical relevance.
AB - In many Internet of Things (IoT) applications, data sensed by an IoT device are continuously sent to the server and monitored against a specification. Since the data often contain sensitive information, and the monitored specification is usually proprietary, both must be kept private from the other end. We propose a protocol to conduct oblivious online monitoring—online monitoring conducted without revealing the private information of each party to the other—against a safety LTL specification. In our protocol, we first convert a safety LTL formula into a DFA and conduct online monitoring with the DFA. Based on fully homomorphic encryption (FHE), we propose two online algorithms (Reverse and Block) to run a DFA obliviously. We prove the correctness and security of our entire protocol. We also show the scalability of our algorithms theoretically and empirically. Our case study shows that our algorithms are fast enough to monitor blood glucose levels online, demonstrating our protocol’s practical relevance.
UR - https://www.scopus.com/pages/publications/85135773268
U2 - 10.1007/978-3-031-13185-1_22
DO - 10.1007/978-3-031-13185-1_22
M3 - 会议稿件
AN - SCOPUS:85135773268
SN - 9783031131844
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 447
EP - 468
BT - Computer Aided Verification - 34th International Conference, CAV 2022, Proceedings
A2 - Shoham, Sharon
A2 - Vizel, Yakir
PB - Springer Science and Business Media Deutschland GmbH
T2 - 34th International Conference on Computer Aided Verification, CAV 2022
Y2 - 7 August 2022 through 10 August 2022
ER -