Verification of Quantum Cryptography Protocols by Model Checking

Unlike classical cryptography which is based on mathematical functions, Quantum Cryptography or Quantum Key Distribution (QKD) exploits the laws of quantum physics to offer unconditionally secure communication. The progress of research in this field allows the anticipation of QKD to be available outside of laboratories within the next few years and efforts are made to improve the performance and reliability of the implemented technologies. But despite this big progress, several challenges remain. For example the task of how to test the devices of QKD did not yet receive enough attention. These apparatuses become heterogeneous, complex and so demand a big verification effort. In this paper we propose to study quantum cryptography protocols by applying the technique of probabilistic model checking. Using PRISM tool, we analyze the security of BB84 protocol and we are focused on the specific security property of eavesdropper's information gain on the key derived from the implementation of this protocol. We show that this property is affected by the parameters of the eavesdropper’s power and the quantum channel.