The Formal Analysis Of Security Protocol

At the present time, following the inundant developing of computer and compunication,the importance of security protocols became more and more evident. Security protocols take charge of distributing keys and authenticating identity.Once there is a flaw in a security protocol itself,the security of communication would face danger.The paper analyse the security protocol on the basis of BAN logic and Symbolic Model Checking.The main work of this paper are as follows:(1) Using BAN logic idealize the YAHALOM protocol,and building initial state assumption of the Validity Kas,Kab and Kbs, the authority of the server S,the freshness of the random number Na and Nb,etc. And executing reasoning prove on the basis of the six rules which provide by BAN logic,in order to verify the protocol which can achieve the first goals and the second goals provided in this paper or not.At the same time,we analyze the reasoning result,if the protol can not acheieve all the goals,it means that the protocol has some presence of security vulnerabilities.Then we will propose some constructive suggestions on the results of the analysis reasoning to improve YAHALOM;(2) SMV is an automated tool for the verification of security protocol. The paper explains the syntax and semantics of symbolic model checking software SMV and constructs the finite state machine model for three communication entities of YAHALOM protocol on the basis of small system model.At the same time,we create three state transition diagrams for the honest communication entities of initiator A,responder B and server S.Of course,we will also create state transition diagrams for the intruder I which will intend A,B or S. Then we will provide the natural language description of the diagram which shows the state transition of three honest communication entities,and construct detailed modele for YAHALOM protocol. Then we describe the authentication, confidentiality, security and integrity of the CTL property according to the SMV syntax and semantics. Finally the SMV software will execute the model,in order to verify the YAHALOM agreeing the R1～R6CTL properties or not,and the system will give true or false,if the result is false, The system will automatically give a counter-example, Then we can put forward the feasible proposal on the basis of analyzing the counterexample to the improvement of YAHALOM protocol.(3) Comparison of the two methods of verification from the perspective of time complexity and space complexity, in order to do a more in-depth understanding of the formalization of security protocol verification.