Research On The Security Analysis Method Of Quantum Communication Protocol Based On Model Checking

With the deepening of information technology,the importance of information security has been paid more and more attention by various industries,corresponding to the rapid development of cryptography technology.The security of encryption algorithm in classical cryptography is based on its computational complexity,that is to say,it takes a great deal of time to solve the mathematical problems related to the cryptographic system by using the existing techniques.With the rapid development of large-scale distributed computing,algorithm optimization and quantum computer,the security of classical cryptographic algorithms is facing a severe test.In recent years,researchers have made use of the unique characteristics of quantum mechanics to solve the problem of information security,which opens a new way for the development of information security.Quantum communication,as a cross subject of quantum mechanics,communication and classical cryptography,has become a hot research direction in the field of information security in the past ten years.The security of quantum communication is guaranteed by the Heisenberg uncertainty principle,the quantum non-cloning theorem,the correlation and nonlocality of entangled particles,and not by the computational complexity.Therefore,even in the future,quantum secure communication can resist the attack of quantum computing.Compared with traditional communication,quantum communication has the characteristics of unconditional security,which is the biggest advantage of quantum communication.The unconditional security is for the existence of eavesdroppers,that is,quantum communication can ensure that: if there are eavesdroppers,the eavesdropping behavior of eavesdroppers will be found by legitimate users.Although quantum communication has irreplaceable advantages,the security of quantum secure communication protocol is complex and difficult.Security,as the most important part of quantum communication protocol,requires the researchers to prove its security from a theoretical point of view with rigorous mathematical logic and deep mathematical reasoning.In order to simplify the security proof,firstly,from the point of view of probabilistic model-based detection,this paper verifies that the polarization state ofsingle photon is regarded as an attractive particle to determine whether there are eavesdroppers,and the experimental results are satisfactory.The modeling detection methods of various quantum communication protocols(including quantum key distribution protocol,quantum secret sharing protocol and quantum equal exchange protocol)are mainly designed.Finally,from the mathematical point of view,the quantum key distribution is proved.The feasibility and security of modeling detection of protocols such as quantum secret sharing and quantum equal exchange provide some valuable new ideas and methods for the security analysis and proof of quantum secure communication protocols.