Study On Algebra Methods For Cryptographic Protocol Verification

Cryptographic protocol is the basis of network communication and security applications, and it is an important component of security infrastructure. Protocol design and its verification are key tasks in the realm of protocol engineering, which involves: protocol design, protocol description, protocol verification, protocol performance test, protocol implementation and protocol maintenance.Since the 1970's, lots of protocol verification methods have been proposed and they can be classified into four categories, namely: modal logic method, model checking method which bases on FSM, theorem proving method that bases on security algebra model and program analysis method. Among them, theorem proving method is the main research point as it can give the proof the protocol's correctness.Owing to the subtlety of security goal, the complexity of network environment, the uncertainty of the penetrator's ability and the high parallelization of protocol run, verification of a cryptographic protocol can be very difficult, so various of methods are adopted to solve the problem, such as: state checking, Invariant set and equivalence testing etc.In this article, a detailed analysis is given to the formal verification methods of security protocols, and we paid more attention to those methods based on pi calculus, which involves: the spi calculus framed bisimulation method for protocol analysis and applied pi calculus. and the main contributions of our work are:(1) Give a detailed analysis to the spi calculus, which includes: the spi's framework, operational semantics and proof technical for process equivalence etc. furthermore, we analyzed the correctness of a variant of the Otway—Rees protocol by spi.(2) spi extended the terms and process of the standard pi calculus so as to define cryptographic operations, but spi neglected the security semantics of these operations, which limited its application in the realm of protocol analysis, and we proved the non-repudiation protocol: ZG by importing the message origination test, thus extended the applicability of spi calculus.(3) Framed bisimulation is an effective method to prove "observe equivalence" between processes. It uses a pair of frame and theory to denote the environment knowledge while protocol run. In this chapter, we introduced the syntax, operational semantics and main theorems about this method.(4) Applied pi calculus is a specialization of the pi calculus so as to make the verification of cryptographic protocol more smoothly, and there are lots of new conception in the applied pi calculus, which involves: function application, equational theory, active substitution, static equivalence, evaluation context, etc. In the paper, we analyzed the dependency between the main and the sub-protocol of a compound protocol, put up the definition of disjoint verification, and interpreted its usage in the field of protocol engineering by examples.