量子密钥分配协议的Petri网建模及安全性分析

Security analysis on the Petri-net model of quantum key distribution protocol

量子密钥分配协议已经被证明具有无条件安全特性,但是证明过程比较复杂,不利于推广到其他量子密码协议的安全性分析和证明中。为了简化量子密码协议的安全性证明以及建立一种通用的证明方法,基于Petri网提出一种量子密钥分配协议的形式化分析方法,根据Biham的等效对称化攻击模型,将协议分为主体模型和攻击模型两部分,建立了BB84协议的Petri网模型,然后对模型进行安全性分析,分析结果表明,BB84协议是无条件安全的。该方法提高了安全性分析效率,形式上简洁统一,容易推广到其他量子密码协议的安全性分析中。

Quantum key distribution protocols are already proved to be unconditionally secure, however, the complexity of the existed proving versions makes it a difficult way to further spread into the security proving of other quantum cryptography protocols. To address this problem, a new method of security analysis of QKD protocols is introduced. Based on the equivalence attack model of QKD protocols which is refered to Biham＇s proving, the protocol is divided into two parts： the body and the attack, then a Petri-net model of BB84 is obtained, and a security analysis is followed. The formal annlysis of QKD protocols based on Petri-net can improve the efficiency of security analysis. Because of its simpleness and unification, it becomes more easy to apply this method to other quantum cryptography protocols.