Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption

Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
复制标题

通过全同态加密对安全 LTL 规范进行不经意的在线监控

DOI:
10.1007/978-3-031-13185-1_22
复制
发表时间:
2022
期刊:
34th International Conference on Computer-Aided Verification
影响因子:
--
通讯作者:
Suenaga Kohei
Suenaga Kohei
中科院分区:
--
文献类型:
--
作者:
Banno Ryotaro;Matsuoka Kotaro;Matsumoto Naoki;Bian Song;Waga Masaki;Suenaga Kohei

文献摘要

相似文献

在许多物联网 (IoT) 应用中,物联网设备感测的数据会持续发送到服务器并根据规范进行监控。由于数据通常包含敏感信息,并且受监控的规范通常是专有的,因此两者都必须对另一端保密。我们提出了一种协议,用于根据安全 LTL 规范进行不经意的在线监控(即在不向另一方透露各方私人信息的情况下进行在线监控)。在我们的协议中,我们首先将安全LTL公式转换为DFA,并使用DFA进行在线监控。基于全同态加密(FHE),我们提出了两种在线算法(ReverseandBlock)来不经意地运行 DFA。我们证明了整个协议的正确性和安全性。我们还从理论上和经验上展示了我们算法的可扩展性。我们的案例研究表明,我们的算法足够快,可以在线监测血糖水平,证明了我们的协议的实际相关性。
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 conductoblivious 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 onfully homomorphic encryption (FHE), we propose two online algorithms (ReverseandBlock) 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.