Presenter: Yiyang Zhou
Abstract: Quantum key distribution (QKD) protocols are cryptographic techniques that provide an unconditionally secure key for communication parties. However, due to the limitations of hardware devices, practical QKD systems are vulnerable to photon number splitting (PNS) attacks. To counteract this attack, researchers have proposed a decoy-state variant of QKD.
As part of a cryptographic communication protocol, the security of this variant is of great concern. However, current security analyses are mainly based on theoretical derivations and mathematical proofs, which are insufficient to ensure the security of practical systems in various scenarios.
The main difficulty in analyzing the security of quantum systems lies in their inherent stochastic behavior and uncertainty. In this paper, we employ probabilistic model checking to encode the stochastic behavior of each component of the QKD protocol into a model checker. We verified the security nature of the protocol under multiple parameters to ensure the information security of the communication parties.