查看文章

Quantum cryptography or Quantum Key Distribution (QKD) solves the key distribution problem by allowing the exchange of a cryptographic key between two remote parties with absolute security, guaranteed by the laws of physics. Actually, the progress of research in this field allows the anticipation of Quantum Cryptography to be available outside of laboratories within the next few years. Efforts are made to improve the performance and reliability of the implemented technologies. Despite this progress, several challenges remain. For example, the task of how to test the apparatuses of Quantum Cryptography did not yet receive enough attention. These apparatuses become complex and demand a big verification effort. In this paper we are focused on an approach based on the technique of probabilistic model checking in studying the security of QKD protocols. We use the model checker PRISM to analyze the security of B92 protocol and we are interested in the specific security property of eavesdropping detection. We have shown that this property is affected by the power of eavesdropper and the parameters of quantum channel.