Study On Formal Verification Of Security Protocol

With the development of cumputer networks, information security has become a vital issue ininformation times. Among the many ways to protect the data on the networks; security protocolis an effective one. However, as we know, it’s quite difficult to design a correct and reliablesecurity protocol. Many deployed protocols are proved to be insecure and several vulnerabilitieshave been exploited until recently. To fix this problem, researchers have tried to use formalmethods to analyze and verify security protocols.In this thesis, we concern the formal verificaiton of security protocol in symbolic model andmainly focus on the methods of modeling and verifying security protocol with applied picalculus. During the whole research, we have received lots of achievements, which are listedbelow:(1): Analyzing the approaches of modeling and verifying security protocol in applied picalculus. Firstly, we analyze the way of modeling both security protocols and security propertieswith applied pi calculus, and then we investigate the two techniques that are widely used toverify protocols. The first one is the reachability analysis based on protcol traces, and the otherone is the bisimulation checking based on the equivalence of protocol processes. We havepointed out the disadvantages and challenges of both techniques. In the end, we present severalimproments.(2): Analyzing the constraint based approaches of secrecy verification and constraint solvingtechniques.We use constraint systems to represent the infinite traces of security protocols.Constraint systems are symbolic abstract of protocol execution traces. In this way, we reduce theproblem of protocol verificaiton to the problem of checking the satisfaction of constraint systems.Then we deliberate the constraint solving algorithm proposed by Hubert Comon Lundh, andprove its correctness, completeness and termination. Although it is a practical algorithm, it is stillinefficient.(3) Analyzing the procedure of deciding trace equivalence. Since the observationalequivalence of applied pi calculus is undecidable, we only consider a decidablefragement--simple process. Based on the work of Vincent Cheval, we present an improvementand an Ocaml implementation of the original algorithm. And we propose the first practicaldecision procedure for trace equivalence in presence of XOR. With this procedure, we can alsoverify complex security properties which are described as trace equivalence. Moreover, since thetrace equivalence and observational equivalence are consistent for simple processes, ourprocedure can be used to decide observational equivalence too.