Ebook: Formal Models and Techniques for Analyzing Security Protocols

Security protocols are small distributed programs which aim to achieve security properties such as confidentiality, authentication, anonymity, etc. Nowadays, security protocols are omnipresent in our daily lives: home-banking, electronic commerce, mobile phones, etc. However, because these protocols are generally implemented on potentially insecure networks (e.g. the Internet) they are extremely difficult to devise. Using Roger Needham's words “Security protocols are three line programs that people still manage to get wrong”. Based on the seminal work of Dolev and Yao, symbolic methods for analyzing such protocols have been in development for about 25 years. The main components of these models are the perfect cryptography assumption and an unbounded non-deterministic adversary that has complete control of the network.

The field of symbolic analysis of security protocols has seen significant advances during the last few years. We now have a better understanding of decidability and complexity questions and models with solid theoretical foundations have been developed together with proof techniques. Automated tools have also been designed and successfully applied to numerous protocols, including industrial protocols, for the provision of security or the discovery of attacks, and models have been extended with algebraic properties in order to weaken the perfect cryptography assumption. Recently, even computational soundness results towards cryptographic models have been achieved.

However, the field was still missing a book which summarized the state-of-the-art of these advances. While we certainly do not pretend to give a complete overview of the field, which would be impossible in a single book, nevertheless, we believe that we have covered a representative sample of the ongoing work in this field, which is still very active. This book contains an introduction and 10 tutorial-like chapters on selected topics, each written by a leading expert in the field of formal analysis of security protocols. We are extremely grateful to all the authors for their hard work and effort in preparing these chapters.

January 2011

Véronique Cortier and Steve Kremer

We investigate the complexity of the protocol insecurity problem for a finite number of sessions (fixed number of interleaved runs). We show that this problem is NP-complete with respect to a Dolev-Yao model of intruders. The result does not assume a limit on the size of messages and supports asymetric and non-atomic symmetric encryption keys. We also prove that in order to build an attack with a fixed number of sessions the intruder needs only to forge messages of linear size, provided that they are represented as DAGs.

Derivability constraints represent in a symbolic way the infinite set of possible executions of a finite protocol, in presence of an arbitrary active attacker. Solving a derivability constraint consists in computing a simplified representation of such executions, which is amenable to the verification of any (trace) security property. Our goal is to explain this method on a non-trivial combination of primitives.

In this chapter we explain how to model the protocol executions using derivability constraints, and how such constraints are interpreted, depending on the cryptographic primitives and the assumed attacker capabilities. Such capabilities are represented as a deduction system that has some specific properties. We choose as an example the combination of exclusive-or, symmetric encryption/decryption and pairing/unpairing. We explain the properties of the deduction system in this case and give a complete and terminating set of rules that solves derivability constraints. A similar set of rules has been already published for the classical Dolev-Yao attacker, but it is a new result for the combination of primitives that we consider. This allows to decide trace security properties for this combination of primitives and arbitrary finite protocols.

In this chapter we describe an approach to analysing security protocols using the process algebra CSP and the model checker FDR. The basic approach is to build a CSP model of a small system running the protocol, together with the most general intruder who can interact with the protocol. We then use the model checker FDR to explore the state space, looking for insecure states. In the second half of the chapter, we extend this approach so as to be able to analyse an arbitrary system running the protocol.

This chapter presents a method for verifying security protocols based on an abstract representation of protocols by Horn clauses. This method is the foundation of the protocol verifier ProVerif. It is fully automatic, efficient, and can handle an unbounded number of sessions and an unbounded message space. It supports various cryptographic primitives defined by rewrite rules or equations. Even if we focus on secrecy in this chapter, this method can also prove other security properties, including authentication and process equivalences.

The applied pi calculus is a language for modelling security protocols. It is an extension of the pi calculus, a language for studying concurrency and process interaction. This chapter presents the applied pi calculus in a tutorial style. It describes reachability, correspondence, and observational equivalence properties, with examples showing how to model secrecy, authentication, and privacy aspects of protocols.

We revise existing type-based analyses of security protocols by devising a core type system for secrecy, integrity and authentication in the setting of spi-calculus processes. These fundamental security properties are usually studied independently. Our exercise of considering all of them in a uniform framework is interesting under different perspectives: (i) it provides a general overview of how type theory can be applied to reason on security protocols; (ii) it illustrates and compares the main results and techniques in literature; (iii) perhaps more importantly, it shows that by combining techniques deployed for different properties, existing type-systems can be significantly simplified.

Protocol Composition Logic (PCL) is a logic for proving authentication and secrecy properties of network protocols. This chapter presents the central concepts of PCL, including a protocol programming language, the semantics of protocol execution in the presence of a network attacker, the syntax and semantics of PCL assertions, and axioms and proof rules for proving authentication properties. The presentation draws on a logical framework enhanced with subtyping, setting the stage for mechanizing PCL proofs. and gives a new presentation of PCL semantics involving honest and unconstrained principals. Other papers on PCL provide additional axioms, proof rules, and case studies of standardized protocols in common use.

Given a cryptographic protocol, and some assumptions, can we present everything that can happen, subject to these assumptions? The assumptions may include: (i) some behavior assumed to have occurred, (ii) some keys assumed to be uncompromised, and (iii) some values assumed to have been freshly chosen. An object representing these types of information is called a skeleton.

The shapes for a skeleton A are the minimal, essentially different executions that are compatible with the assumptions in A. The set of shapes for an A is frequently but not always finite. Given a finite set of shapes for A, it is evident whether a security goal such as authentication or confidentiality holds for A.

In this paper, we describe a search that finds the shapes, starting from a protocol and a skeleton A. The search is driven by the challenge-response patterns formalized in the strand space authentication tests.

Communicating Sequential Processes (CSP) is an abstract language for describing processes and reasoning about their interactions within concurrent systems. It is appropriate for investigating the overall behaviour that emerges. It has a mature theory, and powerful tool support [For03] and can be considered as an off-the-shelf framework which can be customised for particular domains through additional domain-specific constructions and theory. This chapter introduces the application of CSP to the analysis of security protocols. For the purposes of this chapter, we will introduce only those parts of CSP that we use in protocol analysis. Fuller descriptions of the language and theory can be found in [Hoa85,Ros97,Sch99].

Symbolic models for security are built around axioms that reflect appealing intuition regarding the security of basic primitives. The resulting adversaries however often seem unrealistically strong in some of their abilities and not sufficiently powerful in others. An interesting research direction pioneered by Abadi and Rogaway is to show that despite these apparent limitations symbolic models can be used to obtain results that are meaningful with respect to the more detailed and realistic models used in computational cryptography. This line of research is now known as computational soundness. This chapter describes in detail a computational soundness result that extends the original work of Abadi and Rogaway. We show that it is possible to reason about computational indistinguishability of distributions obtained by using symmetric encryption and exponentiation in finite groups with entirely symbolic methods. The result relies on standard notions of security for the encryption scheme and on a powerful generalization of the Diffie-Hellman assumption.