Security Analysis of Semi-Quantum Cryptography Protocols by Model Checking

For cryptography protocols, security is its most core issue, and is the same for quantum cryptography protocols. Researchers can adopt many methods to prove that these protocols are secure, but there exists much difficulty. By using the method of formal verification and the technique of model checking, a fully automated probabilistic model checking tool-PRISM can be used to model these protocols and verify the security properties. Such a methodology can not only avoid the computational complexity of the traditional verification methods based on mathematics, but also improve efficiency and accelerate the verification process. The verification results show that the detection rate of eavesdropping is approximately close to 1 when sufficient photons are transmitted. The semi-quantum cryptography protocols is as secure as the full quantum protocols.