Formal Analysis Of Security Protocols Based On Model Checking

Security protocols,as one of the standards for data exchange in networks,play a crucial role in ensuring the communication security of the Internet of Things and 5G networks.With the increasingly issues of network security,the security protocol,as an important part of network security,is the security information exchange protocol based on the crytptography.If a security protocols itself has security risks,once a malicious attack occurs,the property,privacy and even normal life of network users will be greatly affected.How to design a secure network security protocol has become a common concern in the academic and industrial area.Formal methods,starting from mathematical algorithms,is able to help researchers to guarantee the security property of security protocols more comprehensively and completely by finding potential attacks.Formal methods has been successfully applied by researchers,and a large number of potential security risks in practical security protocols have been found.However,it takes a lot of time and efforts for experts to verify security protocols by using formal analysis technology.From the perspective of model checking and theorem proving,this paper conducts research on automatic analysis and verification of security protocols.At present,Alice?Bob language is widely used in the industry to describe the message exchange process between principals in security protocols.However,due to the lack of unified specifications and clear semantic definitions,Alice?Bob language cannot be directly applied to Formal Verification tools.In addition,since model checking is hard to solve the problem of state space explosion,we propose a constrained automatic analysis and validation mechanism for security protocols,which solves the problem of state space explosion efficiently.Finally,it can analyze and design the security protocol comprehensively and completely.The main research achievements are summarized as follows:1.An effective Alice?Bob specification is proposed,which can provide customized language description capabilities while keeping simplicity and consistency,and formally realizes the process of pictures.Network protocols that support steering and algebraic reasoning,both in the form of multi-agent participation(eg OtwayRees)and protocol key exchange(eg Diffie-Hellman)that can be easily described.2.An automatic verification method of security protocol is proposed,which adopts explicit Alice?Bob language specification for modeling security protocols.Based on this method,a set of methodologies and implementation tools for model transformation,analysis and verification are proposed,which can convert Alice?Bob specification model into the Murphi model checking tool for verification.We propose the first operation semantics of Strand Space theorem to formally describe the behavior of principals.Within the operational semantics,the semantic consistency between the intermediate format and the Murphi formal model can be well guaranteed.Furthermore,a pattern matching procedure is proposed to formalize the behavior of receiving message actions,which facilitates formal reasoning in the operational semantic context.3.A formally verified scheme based on the operation semantics of extended Strand Space theorem is proposed,and the security protocol is modeled and verified in the Murphi model checker,which includes encoding recursively defined messages as well as modeling the behavior of regular principals and malicious intruders in the Delvo-Yao model.We use a specific reduction strategy to constrain the model to concatenated messages and encrypted messages,and only construct the compound messages accepted by the regular principals,so as to realize the encoding form of Strand Space operation semantics in Murphi,and conduct model verification analysis of security protocols.