Research Of Efficient Verification For Security Protocol Based On Model Checking

The security protocol is widely used in various communication systems,and its security depends not only on the underlying encryption algorithm,but also on its design.If the security protocol is not designed to be secure,it is easy for an intruder to exploit its vulnerability and launch a cyber-attack,causing great damage.It is difficult for the traditional non-formal method to find out the flaws of the security protocol comprehensively and systematically,and the formal method becomes one of the most effective methods to analyze the security protocol with the help of its mathematical rigor.Model checking is one of the formal methods,and it has attracted much attention of researchers because of its simplicity,high degree of automation,and ability to provide counterexample paths.In this paper,model checking technology is used to analyze security protocols.First,the operational semantics and security attributes used to describe security protocols are defined.Then,a message specification strategy based on protocol state is proposed to alleviate state explosion.The construction of security protocols with Promela modeling language is introduced in detail.Finally,the model checker SPIN is used to verify and analyze the NSPK and RPC protocol models.The main research results of this paper are as follows:(1)The operational semantics and security attributes of the security protocol are proposed.First,the role items and role events under the static protocol specification are defined,and the related concepts such as session items,instances,and threads under the dynamic protocol operation are defined,and operational semantic rules are given.Three concepts of honest 、 actor and other are introduced,and three security properties of secrecy,secret consistency and authentication are formally defined according to the finite trace transition rules of operational semantics.(2)The intruder model is formally defined.First,the session item and knowledge base are further divided,and then the intruder behavior framework and four attack capabilities are defined,and the corresponding algorithm description is given.According to the above definition,it provides a unified modeling framework and standard for subsequent intruder modeling.(3)In the protocol modeling based on SPIN,there are two types of methods for intruders to construct attack packets.The basic principles and the advantages and disadvantages of these two methods are elaborated in detail.Combining these two methods,this paper proposes a message reduction method based on the protocol state.This method achieves the purpose of reducing the number of invalid attack packets by dynamically detecting the state of each honest subject and constructing attack packets in the corresponding state,thereby alleviating the state explosion problem.(4)On the basis of the above work,the steps of building a security protocol model in Promela are described in detail,including: data pre-definition,honest subject modeling,intruder modeling,and security properties characterization.According to the modeling scheme,SPIN is used to verify and analyze the NSPK and RPC protocol models,and the loopholes in the protocol are successfully found.Compared with the existing work,the modeling scheme in this paper is more versatile.When constructing different protocol models,it can be quickly verified only by modifying part of the code;the verification efficiency is higher,and the number of state spaces and transitions generated is lower.