The Research And Implementation On The Formal Verification Technique Of Security Protocol

A protocol is defined as the execution steps and the execution rules arranged by two or more participants for finishing a task. There are three requirements in the definition :(1)There exist at least two participants; (2)The protocol is represented by a sequence of steps of message exchanging and message processing among the participants of the protocol; (3)The purpose of running a protocol is to finish a task or reach some common understanding.Security protocol is a type of communication protocol based on cryptography, which runs over the computer network or distributed systems, and arranges the execution steps and the execution rules with the cryptographic algorithms among the participants who implement tasks such as key distribution, identity authentication, e-commerce transaction etc.The correctness of security protocols is critical for the transactions over the open networks The runnings of the security protocols do not always achieve their design objectives for the reasons that the interleaving run of security protocol's infinite sessions and the attacker's deliberate demolishment. Formal methods have been proved to be an effective way for the analysis and verification of security protocols. The analysis and the verification of security protocols have been the focus in the domain of formal methods.In this dissertation, security protocols are the main research objectives, and the effective formal verification methods are the main research contents. Primary innovative work in this paper can be summarized as following:(1) Security protocol's modelling approach, formal verification methods and the algorithms for constructing counter-examplesBruno Blanchet presents the security protocol's model based on Horn logic and this model is obtained from the model based on linear logic by abstract interpretation, program transformation and Skolemization of the atomic formulae with existential quantifiers. The security protocol's model based on process algebra can also be transformed into the the model based on Horn logic by a group of transformation rules. In this model, the senders and the receivers of messages are not described, and the formal characterizations of the honest-roles and the attacker can not be distinguished.Based on Bruno Blanchet's security protocol model, the extended model based on Horn logic and the extended model based on process algebra are presented. Based on Bruno Blanchet's verification method, a modified verification method for the security protocol's extended model based on Horn logic is presented, and security protocol's counter-examples can be constructed automatically from theverification process. If the verification process proves the extended model based on Horn logic satisfies the security protocol, then the security protocol satisfies the security property by the property of abstract interpretation; If the verification process shows the extended model does not satisfy the security property, then the security protocol may or may not satisfy the security property since abstract interpretation may introduce false attacks. Automatically constructing the security protocol's counter-examples contributes to distinguishing false attacks, finding the reasons causing the security protocol's flaws and fixing the flawed security protocols. Based on the modified verification process of the security protocol's extended model based on Horn logic, the algorithm for automatically constructing security protocol's counter-examples is presented.The verification problem of security protocol's correctness is undecidable, and the security protocols' verification process does not always terminate. To verity security protocol more effectively, averifiaction strategy is presented: verify security properties every k(k≥1) iterative computation steps ofthe fixpoint of the security protocol's logic program.(2) The unification algorithm of the unification problem in the ACUN theory, security protocol with XOR's formal verification methodsSecurity protocol with XOR are the protocols in which the operator exclusive-or is a protocol primitive In the Dolev-Yao model, the attacker can not utilize the algebraic properties of protocol primitives to attack security protocols, which cause some attacks of security protocol with XOR not be found.ACUN theory characterizes the algebraic properties of the operator exclusive-or. Based on Gaussian Elimination, a solving algorithm of the most general unifier of the elementary unification problem and the unification problem with constants in ACUN theory is presented. Based on the term's canonical decomposition and the uniqueness of the canonical decomposition, a solving algorithm of the most general unifier of the unification problem with linear constants restriction in ACUN theory is presented. Based on the decomposition algorithm for the unification problem in the union of disjoint equational theories, the unification algorithm of the general unification problem in ACUN theory is presented. Introduce the concept maximal ordering and prove the general unification problem in ACUN theory only need to solve the unification problem with linear constants restriction induced by all maximal linear orderings instead of all the linear orderings.Based on the modified verification method and the algorithm for the general unification problem in ACUN theory, the verificatiuon method for the security protocol with XOR is also presented.(3) Design and develop a verification tool prototype SPVT based on Objective CamlBased on the algorithms in this dissertation, a verification tool prototype, SPVT, is designed and developed for verifying security protocol. SPVT is developped with the functional programming language Objective-Caml 3.06. SPVT can be used to automatically verify the secrecy property and the authentication property. If the verification process shows the security protocol does not satisfy the security property, SPVT automatically constructs the corresponding counter-examples, and the counter-examples are described by the standard description of the security protocol.