基于模型检测的半量子密码协议的安全性分析

Security Analysis of Semi-Quantum Cryptography Protocols by Model Checking

对于密码协议而言,安全性是其最核心的关键问题,对于量子密码协议来说也一样。研究人员可以通过各种手段证明这些协议是安全的,但存在极大的困难,因为这对数学功底有着很高的要求。该文利用全自动化的技术——模型检测,采用了形式化验证方法,即基于概率的模型检测工具PRISM,来对半量子密码协议进行建模并验证其安全性。该方法避免了传统基于数学方法验证的繁杂,提高了验证的速度和效率。验证的结果也表明,当传输足够多的光子时,检测出窃听的概率无限趋近于1,和全量子密码协议一样,半量子密码协议也是安全的。

For cryptography protocols, security is its most core issue, and is the same for quantum cryptography protocols. Researchers can adopt many methods to prove that these protocols are secure, but there exists much difficulty. By using the method of formal verification and the technique of model checking, a fully automated probahilistic model checking tool - PRISM can be used to model these protocols and verify the security properties. Such a methodology can not only avoid the computational complexity of the traditional verification methods based on mathematics, but also improve efficiency and accelerate the verification process. The verification results show that the detection rate of eavesdropping is approximately close to 1 when sufficient photons are transmitted. The semi-quantum cryptography protocols is as secure as the full quantum protocols.