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

摘要

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