密钥交换协议允许事先互不相识的双方共享一个公共加密密钥,以便随后交换对称加密消息。当前的密钥交换协议基于公钥加密。因此,它们的安全性基于知道公钥、找到私钥或用公钥加密的密钥的难度。随着量子计算机的出现,当前的非对称算法将不再提供这样的保证 [1]。量子密钥分发协议(量子密钥分发,QKD)的安全性基于量子物理的特性,特别是不可克隆定理 [2];该定理指出,不可能完美地克隆粒子(量子比特)的量子态。如果攻击者试图读取两个参与者交换的量子比特(通常是光子的偏振态),那么她必然会修改量子态,因此可以即时检测到。然而,QKD 的局限性之一仍然是双方可以交换的最大地理距离,目前为几百公里 [3]。ETSI 提出了 QKD 网络的协议标准 [4]。在这里,我们建议使用 ProVerif 工具对其进行正式验证。