Analysis Of Cryptographic Protocol Based On Dynamic Epistemic Logic

With the advent of the fifth Generation network communication era,information security has become one of the issues people concern.Without information security,there will be no national security.For protecting information security,network protocols with cryptographic mechanisms are called cryptographic protocols.The design and analysis of the cryptographic protocol is the research focus in the information security.If the protocol logic itself exists flaws that like leaving an unattended back door in a solid city wall,then unauthorized persons can obtain information or produce forgery without breaking through the password.In order to ensure the correctness of cryptographic protocol,many researchers have carried out various security analysis and verification of the protocol,among which logic has become a major tool.A logical method is used to effectively analyze and verify the security of specific cryptographic protocols for avoiding the harm caused by defects from design in this research.Epistemic logic is an important branch of modal logic.With the development of artificial intelligence and model detection,epistemic logic is widely used in computer science.In this paper,dynamic epistemic logic is used to analyze and verify cryptographic protocols,and extended epistemic logic theory is used to describe cryptographic protocols with nonmonotony of knowledge.Our work in this research is as follows:1.A specific cryptographic protocol is analyzed.Based on the epistemic action of dynamic epistemic logic,a language is constructed to describe the specific cryptographic protocol,and its syntax and semantics are given to describe the protocol.The initial model is constructed by Kripke model,and the corresponding model is changed according to the transformation rules.This change process is the implementation process of the protocol.The whole protocol is formalized completely,and the logical analysis shows that the protocol is secure.2.A specific cryptographic protocol is verified.Based on the action model of dynamic epistemic logic,a language describing the specific cryptographic protocol is constructed to verify the security of the protocol.The actions stipulated in the protocol and attacker's actions are described formally.According to the update model,the action execution process of the protocol is given.The protocol analysis process is detailed and intuitive.The security target model of the protocol is given,and it is proved that the protocol meets the security requirements.3.A cryptographic protocol with nonmonotonicity of knowledge is analyzed.In view of the fact that knowledge is not monotonic,a knowledge nonmonotonic language based on dynamic epistemic logic is constructed to describe a cryptographic protocol with knowledge nonmonotony.The action of "forget" is used to express the forgetting of knowledge,which reflects the nonmonotony of knowledge.Register model is used to represent the knowledge of the agents.The implementation of epistemic action leads to the change of the knowledge of the agents.The implementation process of change protocol based on Kripke model is described concisely and intuitively.The theoretical knowledge of epistemic logic is enriched and expanded,and these theories is applied in practice in our research.With Kripke model,the analyzed protocol is fully formalized,making the knowledge known by the agent clear at a glance.Therefore,the security of these protocols is clearly reflected.The analysis process is simple and intuitive.The application of dynamic epistemic logic to the formal analysis of cryptographic protocols,on the one hand,is conducive to the expansion of logic knowledge,on the other hand,is conducive to the formalized development of cryptographic protocols,which highlights the important role of logic in the field of computer science.In the process of analysis,the potential defects of cryptographic protocol can be corrected in time to avoid the security harm caused by protocol defects and reduce the loss caused by the use of insecure protocol.Therefore,our study has strong immediate significance and value for practical application.