基于全同态加密的针对安全性 LTL 规范的 oblivious 在线监控
密码学与安全
2022-06-09 v1 形式语言与自动机理论
计算机科学中的逻辑
摘要
在许多物联网（IoT）应用中，由 IoT 设备感知的数据被持续发送至服务器，并依据某规范进行监控。由于数据常包含敏感信息，且被监控的规范通常为专有内容，二者均须对另一端保密。我们提出一种协议，用于针对安全性 LTL（线性时序逻辑）规范进行 oblivious 在线监控——即在不向对方泄露各参与方私有信息的情况下进行的在线监控。在我们的协议中，首先将安全性 LTL 公式转换为 DFA（确定性有限自动机），并利用该 DFA 进行在线监控。基于全同态加密（FHE），我们提出两种在线算法（Reverse 与 Block）以 oblivious 方式运行 DFA。我们证明了整个协议的正确性与安全性。我们还从理论与实证两方面展示了算法的可扩展性。案例研究表明，我们的算法速度足以在线监控血糖水平，证明了协议的实际相关性。
引用
@article{arxiv.2206.03582,
title = {Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption},
author = {Ryotaro Banno and Kotaro Matsuoka and Naoki Matsumoto and Song Bian and Masaki Waga and Kohei Suenaga},
journal= {arXiv preprint arXiv:2206.03582},
year = {2022}
}
备注
This is the extended version of a paper to appear at CAV 2022