The Formal Research Of Quantum Cryptographic Protocols Based On Probability

Quantum cryptography is the science which uses properties of quantum mechanics to achieve cryptography. It is the combination of the classical cryptography and the quantum mechanics. It is also an interdiscipline with important significance for scientific research. As the quantum cryptography possesses the basic properties of quantum mechanics: the Heisenberg uncertainty principle and non-cloning theorem, any measurement of any component of the whole quantum cryptography system will inevitably bring about disturbances to the whole system, and such disturbances will inevitably be detected.Therefore, the unconditional security of quantum cryptography is guaranteed. After more than three decades of rapid development, the research of quantum cryptographic protocol has made great progress and become one of the most important branches of cryptography,and it is also one of the most important hot topics.Although the quantum mechanics guarantees the unconditional security of quantum cryptographic protocols, the security proof of quantum cryptographic protocols is still one of the most important and difficult issues in the current study. At present, the security of quantum cryptographic protocols is mainly based on the traditional mathematical methods, which requires a high knowledge background and individual capability. The formal verification method is automated, which can greatly reduce the difficulty of the verification process, and simplify the complexity of the verification process.The most crucial issue of quantum cryptography protocols is its security. The security properties of these protocols can be proved but in ways with much difficulty.Formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property,using formal methods of mathematics. Model checking is one kind of formal verification method, which uses the state space search approach to exhaustively and automatically check whether the given system model meets its design specifications. The advantages are that the testing process is fully automated and the verification is fast and efficient.Based on the projects of the National Natural Science Foundation of China, the contributions of this dissertation are mainly on the research of the security problems of quantum cryptography protocols, including the quantum key distribution protocols, the quantum privacy comparison protocols, the semi-quantum key distribution protocols etc.,and with the usage of the probabilistic model checking methodology of formal verification, the security properties of several quantum cryptography protocols are verified, and the modeling library of eavesdropping methods in the protocols is built. The details are described as follows:Based on a brief introduction of quantum cryptography, we describe two famous quantum key distribution protocols, BB84 and B92. Then we use the probabilistic model checker PRISM to abstract the execution process of the protocols, and analyze the security properties of the protocols by establishing models of the systems.We introduce the developing procedure of quantum privacy protocols. By adopting a newly proposed quantum privacy comparison protocol based on multi-party entanglement state, we creatively adopt the probabilistic formal verification methodology to analyze its security property. The results show that the protocols is secure against the interceptresend attack.In the research domain of semi-quantum cryptographic protocols, we introduce the latest proposed semi-quantum key distribution protocols. We adopt the PRISM tool to abstract and build a model of the execution procedure, and its security property against the intercept-resend attack, the random substitute attack and general attack is verified.For both classical and quantum protocol, security is their most important property.So the study of eavesdropping methodology is an indispensable part in the research of quantum cryptography. And as the diversity of the constructive hierarchy of different protocols, even with the same eavesdropping method, there are also many differences in the implementation process. Therefore, we build a model library by abstracting and modeling different eavesdropping/attack methodologies. Users only need to make some appropriate modification and adjustment in the description of the attack models, they can employ the models in their own research. This can not only greatly simplify the difficulty of the verification, but also enhance the speed and the efficiency of the verification, which is one of the goals that the formal method of automated verification wants to achieve.