Research On Formal Methods For Cryptographic Protocols Analysis

The security of cryptographic protocols is the key of network security. The analysis of cryptographic protocols is an important approach to open out whether cryptographic protocols have some secure flaws. Comparing with informal techniques, formal analysis can detect some secure flaws comprehensively. Based on systemic analysis of the formal analysis methods and computational approach, the research content included in this dissertation is divided into three parts:Firstly, the dissertation relaxes the perfect encryption assumption in formal models, by allowing the adversary to break encryptions through a special operation.Of course, this only happens only under suitable hypotheses,so that the adversary is not able to discrupt just any protocol.For this, we borrow from the computational model the idea to use probability and complexity to constrain the adversary power. We therefore define a probabilistic version of the Dolev-Yao adversary. We then consider two common security properties: the secrecy of a given message and non-injective authentication. Using these properties, we compare the enhanced Dolev-Yao adversary to the standard one.Secondly, the dissertation relaxes another assumption that is the free algebra. Indeed,it turns out that a very broad class of protocols only use the following primitives:encryptions,digital signatures,hashes,pairs.These primitives are directly modeled with the terms below: enc(m,k) or enc(m,pub(k)),sig(w,pri(k)),hash(m),cons(m₁,m₂).Here, m denotes a message, k is a key.Terms pub(k) and pri(k) denote the public and private parts of the asymmetric key. In formal model,the algebra given by the above primitives is usually assumed to be free. In other words,considering only symmetric encryption, we have that enc(m₁,k₁)=enc(m₂, k₂) if and only if m₁=m₂ and k₁=k₂. This freeness property ensures that intended values and their term representation have a direct one-to-one correspondence. In Chapter 3,we deal with the problem of constructing over-approx-mations for set of terms, when we consider them up to an equivalence relation.This equivalence relation is not fixed, but can be expressed through any term rewriting system.Through rewriting rules, we can express the laws for many cryptographic primitives,without having to choose a fixed set of those.So, with this approach,we relax both the free algebra assumption, as well as the reliance on having a limited set of operations.Here we approximate terms up to rewriting through non deterministic finite tree automata.We define a sequence of algorithms to compute sound approximations.Thirdly,using the above techniques for dealing with terms up to equivalence, we study analysis and verification of cryptographic protocols. We define a process calculus for the specification of protocols. We keep the issues of defining the semantics of the calculus separated from those related to the primitives used. We still allow these primitives to be defined through any rewriting system.Then we consider the static analysis of protocols.Based on the control flow analysis, with changes for this approach,we adapt this analysis to our calculus.This analysis statically computes a finite representation for a superset of the message exchanged through the network at run-time. So terms not within this superset are known not to be used in communications.This can be used to prove the secrecy of a selected data.Our adaptation is able to deal with terms up to rewriting.This enables us to statically reason about security properties of protocols.Fourthly, through the research of the syntax and testing equivalence of the Spi calculus, we extend the Spi calculus, and make the extended Spi calculus as the input language of an automatic verification system. We analyze the EKE protocol using the extended Spi calculus, and the results indicate this system achieves good results in analysis of many protocols, and this system is reliable and creditable.The contributions of this dissertation are as following:Firstly, we proposed a process calculus for the cryptographic primitives of protocols. We defined its formal syntax and semantics.Secondly, based on our process calculus, we proposed a probabilistic definition of the standard Dolev-Yao adversary. We adapted the standard Dolev-Yao adversary model so that the adversary can guess the key of decrypting the intercepted message.Thirdly, in our process calculus, we proposed the probabilistic notion of secrecy and authentication. And under the assumptions that the adversary successfully guess a key with a negligible probability and the resources of the adversary are polynomial.Then we provede the enhanced adversary model has the same power as the standard Dolev-Yao adversaryFourthly, the dissertation proposed a approach for computing a finite over-approxmations for set of terms up to rewriting system.We expressed the language through a finite tree automata. Also, approximation is a term automata, and it instantiated rewriting.That is the language of terms include all initial terms and all possible rewriting of these terms. Then we proposed its semantics. We defined a sequence of algorithms to compute sound approximations.Fifthly, for the specification of protocols, we proposed a process calculus.Then we formally defined the syntax, dynamic semantics and static semantics of our calculus.Sixthly, we adapted the control flow analysis to our calculus. So, this analysis statically computes a finite representation for a superset of the message exchanged through the network at run-time. This enables us to statically reason about security properties of protocols.Finally, we extended and improved the Spi calculus, and maked the extend Spi calculus as the input language of an automatic verification system. This system achieved good results in analysis of many protocols. Then we analyzed the EKE protocol, we found the EKE protocol is not secure under parallel session attack.