A Research On The Formal Analysis Of Quantum Cryptography Protocols

Quantum cryptography protocols have the feature of unconditonal security. As long as so far, it is still a difficult problem to prove the unconditional security of quantum cryptography protocols,although QKD protocols are completely proved to be unconditional secure. And the existed proving methods seem to be very complex,Formalization is a popular way to analyze the traditonal protocols.Based on the Formal-Analyzing principles, Quantum cryptography protocols will be analyzed.It improves the efficiency of analysis in evidence,and simplifies the procedures of analysis in a comparablely uniform way,at the same time,it will make the computer auto analysis more easy.First,a research on the methods of proving the security of QKD protocols is done,A conclusion about the advantages and disadvantages of the proving methods can be obtained By comparation,and the significant trait of these methods can be obtained. As is the preparation for the formal analysis to quantum cryptography protocols., Three proving methods is introduced in detail,and a conclusion of each is followed.A new method of analyzing the security of the quantum cryptography protocols which is called BAN-Logic Proving is proposed. New initial hypotheses of BAN-Logic are proposed based on the security conclusions which are obtained by D.Mayers in his papes, then a formally description of the quantum cryptography protocols is followed. A conclusion of the security in BAN-Logic is obtained at the end.This method can simplify the procedures of the security proving,and the efficiency can be greatly improved.Another new method of the security analysis on quantum cryptography protocols based on Petri-Net is proposed by the following. Referring to Eli.Biham's proving, Eve'attack is replaced by an equivalent one which is called symmetric attack, then,a series of steps how to construct a Petri-Net model of BB84 protocol is introduced,and an analysis of the security is followed based on this Petri-Net model.The quantum cryptography protocols can ensure the securiy of the exchanging messages by their ability of detecting the eavesdropping.As long as so far,eavesdropping detection is realized by comparing the error rate of the test bits and the max tolerant error rate.By a research on the second-stair statistical laws of the error string in a QKD protocol,a new way of eavsdropping detection is introduced which is named as Error-String-Modeling.With the techniques of string rebuilding,one-step estimating, wave reshaping, an estimated error string is obtained, then the error rate of the information string can be worked out.This way of testing the eavesdropping can improve the efficiency, thus it makes the protocol more secure.Based on the quantum characteristics of quantum cryptography protocols, the quantum cryptography protocols can be analyzed on BAN-Logic,Petri-Net,and Error-String-Modeling, which provide new ways to analyze the quantum cryptography protocols with high efficiency,and seem to be more simple and uniform.