量子密钥分发协议BB84与B92的CQP建模与PRISM分析

密码协议的安全性证明从理论上确立了协议的强度及其可运行所受的约束，但它没有考虑协议的整体设计。过去，模型检测已成功应用于经典密码协议，以排除原本可能被忽视的设计缺陷。量子密码协议与经典协议的不同之处在于其能够检测窃听者的存在。尽管BB84和B92协议已被证明具有无条件安全性，但在本文中，我们表明识别窃听者的存在受到所交换量子比特数量的限制。我们首先在CQP中对协议建模，然后解释将其转化为PRISM模型的机制。我们主要关注协议检测主动窃听者的能力，以及窃听者在未被任一方检测到的情况下获取共享密钥的程度。最后，我们通过比较协议性能得出结论。