The value of information and the power that it can convey has long been recognized. Now, more than ever, information is a driver of society and its integrity, confidentiality and authenticity must be ensured. Security protocols are a critical element of the infrastructures needed for
the secure communication and processing of information. They are, of course,
not the only components needed to ensure such security properties: for example,
good cryptographic algorithms and systems security measures to protect key material
are also needed. Protocols can however be thought of as the keystones of a secure
architecture: they allow agents to authenticate each other, to establish fresh
session keys to communicate confidentially, to ensure the authenticity of data
and services, and so on.
Aims of the book
This book is about the role of security protocols, how they work, the security
properties they are designed to ensure and how to design and analyze them.
It was recognized very early on, almost as soon as they were conceived, that
the design and analysis of security protocols was going to be a very delicate
and error-prone process. Security protocols are deceptively simple-looking objects
that harbour surprising subtleties and flaws. Attempts to develop frameworks
and tools to reason about their properties goes back over 20 years, but the
topic remains a highly active and fruitful one in the security research community.
An overview of the historical background can be found in Chapter 9.
In this book we present the particular approach to security protocol verification
that has been developed by the authors. It was the first to apply process algebra
and model-checking to the problem. The process algebra in question is CSP (Communicating
Sequential Processes).
There is a widespread misconception that pouring liberal libations of cryptographic
algorithms over an architecture will render it secure. Certainly, good cryptographic
algorithms are important but, as we will see, it is quite possible to have an
architecture employing high grade algorithms that is still wide open to exploitation
due to poor protocol design.
We hope that our readers will come away with a good understanding of the role
of security protocols, how they work and the kinds of vulnerabilities to which
they are prey. In particular we hope that they will better appreciate the subtleties
in making precise the security goals that such protocols are intended to ensure
and the importance of making these goals - as well as the assumptions about
the underlying mechanisms and environment - precise.
Ideally we hope that the reader will gain sufficient understanding (and enthusiasm!)
to apply the tools and techniques presented here to their own protocols, real
or imaginary. Perhaps also some readers will be sufficiently intrigued to go
on to pursue research into some of the open problems that remain in this challenging
and fascinating area.
Structure of the book
This book is concerned with the particular approach to analysis and verification
of security protocols based around the process algebra CSP. There are a number
of facets to this approach, and the book uses a running example, the Yahalom
protocol, to link the material.
The Introduction introduces the general topic of security protocols. It covers
the issues that arise in their design, the cryptographic mechanisms that are
used in their construction, the properties that they are expected to have, and
the kinds of attacks that can be mounted to subvert them. It also discusses
the CSP approach and the tool support. The chapter introduces the Yahalom protocol
and several other protocol examples.
Chapter 1 provides a general introduction to the main aspects of CSP relevant
to the approach. CSP consists of a language and underlying theory for modelling
systems consisting of interacting components, and for supporting a formal analysis
of such models. This chapter introduces the building blocks of the language
which enable individual components to be described, and discusses how components
are combined into systems. Specification and verification through refinement,
and with respect to property-oriented specifications, is also covered. The chapter
finishes with a brief discussion of how discrete time can be modelled.
Chapter 2 shows how to use CSP to construct models of security protocols,
which consist of a number of communicating components and are thus well suited
to analysis in CSP. The variety of possible attacks on protocols must also be
built into the model, and the chapter shows how to incorporate the Dolev-Yao
approach to modelling a hostile environment and produce a system description
which is suitable for analysis.
Chapter 3 covers the kinds of properties that security protocols are expected
to provide, and how they can be expressed formally within the CSP framework.
Secrecy and authentication are the main concern of the approaches in this book,
and various forms are covered. The properties of non-repudiation and anonymity
are also discussed.
Chapter 4 introduces the model-checking tool support available for CSP, the
Failures-Divergences Refinement checker (FDR). It discusses how this tool works,
and the nature of refinement checking.
Chapter 5 is concerned with the Casper tool. This is a compiler for security
protocols, which transforms a high-level description of a security protocol,
and the properties required of it, into a CSP model of the protocol as described
in Chapter 2, and a number of assertions to be checked. This model can then
be analyzed using the model-checker FDR discussed in Chapter 4.
Chapter 6 discusses in more detail some of the CSP modelling that is carried
out by Casper, particularly how the hostile environment is modelled to allow
efficient analysis by the model-checker.
Chapter 7 is concerned with direct verification of CSP models of protocols.
It introduces the 'rank function' approach to proving protocols corrrect. This
allows proofs to b constructed that verify protocol descriptions of arbitrary
size against their requirements. The theorem-proving and bespoke tool support
available for this approach is also discussed.
Chapter 8 addresses the problem of scale. Real-world protocols are very large
and their analysis is difficult because of the volume of detail contained in
their description. This chapter is concerned with 'simplifying transformations',
which allow extraneous detail to be abstracted away when checking a protocol
against a particular property in such a way that verification of the abstract
protocol implies correctness of the full protocol. The approach is illustrated
with the CyberCash main sequence protocol.
Chapter 9 discusses the literature on security protocol verification and its
historical context. There are a number of different approaches to the problems
addressed in this book, and this chapter covers many of those that have been
most influential in the field.
Chapter 10 discusses the broader issues, open problems and areas of ongoing
research, and gives indications of areas for possible further developments and
research. One area of current research discussed in this chapter, of particular
importance to the model-checking approach of this book, is the development of
techniques based on 'data independence', which allow the results of model-checking
to be lifted to protocol models of arbitrary size.
There are three appendices. The first covers some background mathematics and
cryptography, introducing the RSA and the ElGamal schemes; the second is an
example of Casper applied to the Yahalom protocol, containing the input file
and the CSP model produced by Casper; and the third contains a verification
using rank functions of the simplified CyberCash protocol descriptions produced
in Chapter 8.
The book has an associated website: cs.rhbnc.ac.uk/books/secprot/This website
provides access to all of the tools discussed in this book, and to the protocol
examples that are used throughout (as well as others). Readers are recommended
to download the tools and experiment with protocol analysis while reading the
book. The website also provides exercises (and answers!), as well as a variety
of other related material.
Acknowledgements
The authors would like to thank DERA (the Defence and Evaluation Research
Agency, UK) and the MoD for funding the Strategic Research Project (SRP) 'Modelling
and Analysis of Security Protocols' under which the foundations of the approach
were laid down, and the EPRSC (UK Engineering and Physical Sciences Research
Council) and ONR (US Office of Naval Research) for funding subsequent developments
of the approach. Thanks are also due to Inmos, ONR, DERA and ESPRIT, for funding
developments to FDR over the years.
Peter Ryan would also like to thank the Department of Computer Science, Royal
Holloway, and Microsoft Research, Cambridge, for hospitality during the writing
of this book.
This work has benefited from collaboration with Philippa Broadfoot, Neil Evans,
James Heather, Mei Lin Hui, Ranko Lazi´ c and the staff at Formal Systems.
It has also been influenced by discussions with and comments from Giampaolo
Bella, Steve Brackin, Dieter Gollmann, Andy Gordon, Roberto Gorrieri, Joshua
Guttman, Richard Kemmerer, John McLean, Cathy Meadows, Larry Paulson, Matthias
Schunter, Paul Syverson and Paulo Verissimo.
Finally, special thanks are due to Coby, Helen and Liz, Kate and Eleanor for
moral support. 0201674718P04062001
About the Author
Peter Ryan has over 15 years' experience in cryptography and mathematical modelling, computer security and formal methods, gained at GCHQ, CESG, DERA and SRI Cambridge. He is an IMA Fellow and Chair of the Steering Committee of ESORICS. In 1999 he was awarded the title of DERA Fellow.
Steve Schneider is a Senior Lecturer in the Department of Computer Science, Royal Holloway, University of London UK, has published a large number of journal and conference papers in the areas of concurrency theory and security.
Michael Goldsmith is Managing Director of Formal Systems (Europe) Ltd, the company which developed the FDR tool and devised the techniques described in the book in collaboration with DERA and the University of Oxford. He is a Senior Research Fellow of Worcester College, Oxford.
Gavin Lowe is a Lecturer in Computer Science at the University of Oxford. He was responsible for discovering the attack on the Needham-Schroeder Public-Key protocol, which established the power of the current approach.
Bill Roscoe is Professor of Computing Science at the University of Oxford. He is one of the principal developers of CSP and of its application to cryptoprotocols and other aspects of computer security.
0201674718AB04062001
Excerpt. © Reprinted by permission. All rights reserved.
The value of information and the power that it can convey has long been recognized. Now, more than ever, information is a driver of society and its integrity, confidentiality and authenticity must be ensured. Security protocols are a critical element of the infrastructures needed for the secure communication and processing of information. They are, of course, not the only components needed to ensure such security properties: for example, good cryptographic algorithms and systems security measures to protect key material are also needed. Protocols can however be thought of as the keystones of a secure architecture: they allow agents to authenticate each other, to establish fresh session keys to communicate confidentially, to ensure the authenticity of data and services, and so on.
Aims of the book
This book is about the role of security protocols, how they work, the security properties they are designed to ensure and how to design and analyze them.
It was recognized very early on, almost as soon as they were conceived, that the design and analysis of security protocols was going to be a very delicate and error-prone process. Security protocols are deceptively simple-looking objects that harbour surprising subtleties and flaws. Attempts to develop frameworks and tools to reason about their properties goes back over 20 years, but the topic remains a highly active and fruitful one in the security research community. An overview of the historical background can be found in Chapter 9.
In this book we present the particular approach to security protocol verification that has been developed by the authors. It was the first to apply process algebra and model-checking to the problem. The process algebra in question is CSP (Communicating Sequential Processes).
There is a widespread misconception that pouring liberal libations of cryptographic algorithms over an architecture will render it secure. Certainly, good cryptographic algorithms are important but, as we will see, it is quite possible to have an architecture employing high grade algorithms that is still wide open to exploitation due to poor protocol design.
We hope that our readers will come away with a good understanding of the role of security protocols, how they work and the kinds of vulnerabilities to which they are prey. In particular we hope that they will better appreciate the subtleties in making precise the security goals that such protocols are intended to ensure and the importance of making these goals - as well as the assumptions about the underlying mechanisms and environment - precise.
Ideally we hope that the reader will gain sufficient understanding (and enthusiasm!) to apply the tools and techniques presented here to their own protocols, real or imaginary. Perhaps also some readers will be sufficiently intrigued to go on to pursue research into some of the open problems that remain in this challenging and fascinating area.
Structure of the book
This book is concerned with the particular approach to analysis and verification of security protocols based around the process algebra CSP. There are a number of facets to this approach, and the book uses a running example, the Yahalom protocol, to link the material.
The Introduction introduces the general topic of security protocols. It covers the issues that arise in their design, the cryptographic mechanisms that are used in their construction, the properties that they are expected to have, and the kinds of attacks that can be mounted to subvert them. It also discusses the CSP approach and the tool support. The chapter introduces the Yahalom protocol and several other protocol examples.
Chapter 1 provides a general introduction to the main aspects of CSP relevant to the approach. CSP consists of a language and underlying theory for modelling systems consisting of interacting components, and for supporting a formal analysis of such models. This chapter introduces the building blocks of the language which enable individual components to be described, and discusses how components are combined into systems. Specification and verification through refinement, and with respect to property-oriented specifications, is also covered. The chapter finishes with a brief discussion of how discrete time can be modelled.
Chapter 2 shows how to use CSP to construct models of security protocols, which consist of a number of communicating components and are thus well suited to analysis in CSP. The variety of possible attacks on protocols must also be built into the model, and the chapter shows how to incorporate the Dolev-Yao approach to modelling a hostile environment and produce a system description which is suitable for analysis.
Chapter 3 covers the kinds of properties that security protocols are expected to provide, and how they can be expressed formally within the CSP framework. Secrecy and authentication are the main concern of the approaches in this book, and various forms are covered. The properties of non-repudiation and anonymity are also discussed.
Chapter 4 introduces the model-checking tool support available for CSP, the Failures-Divergences Refinement checker (FDR). It discusses how this tool works, and the nature of refinement checking.
Chapter 5 is concerned with the Casper tool. This is a compiler for security protocols, which transforms a high-level description of a security protocol, and the properties required of it, into a CSP model of the protocol as described in Chapter 2, and a number of assertions to be checked. This model can then be analyzed using the model-checker FDR discussed in Chapter 4.
Chapter 6 discusses in more detail some of the CSP modelling that is carried out by Casper, particularly how the hostile environment is modelled to allow efficient analysis by the model-checker.
Chapter 7 is concerned with direct verification of CSP models of protocols. It introduces the 'rank function' approach to proving protocols corrrect. This allows proofs to b constructed that verify protocol descriptions of arbitrary size against their requirements. The theorem-proving and bespoke tool support available for this approach is also discussed.
Chapter 8 addresses the problem of scale. Real-world protocols are very large and their analysis is difficult because of the volume of detail contained in their description. This chapter is concerned with 'simplifying transformations', which allow extraneous detail to be abstracted away when checking a protocol against a particular property in such a way that verification of the abstract protocol implies correctness of the full protocol. The approach is illustrated with the CyberCash main sequence protocol.
Chapter 9 discusses the literature on security protocol verification and its historical context. There are a number of different approaches to the problems addressed in this book, and this chapter covers many of those that have been most influential in the field.
Chapter 10 discusses the broader issues, open problems and areas of ongoing research, and gives indications of areas for possible further developments and research. One area of current research discussed in this chapter, of particular importance to the model-checking approach of this book, is the development of techniques based on 'data independence', which allow the results of model-checking to be lifted to protocol models of arbitrary size.
There are three appendices. The first covers some background mathematics and cryptography, introducing the RSA and the ElGamal schemes; the second is an example of Casper applied to the Yahalom protocol, containing the input file and the CSP model produced by Casper; and the third contains a verification using rank functions of the simplified CyberCash protocol descriptions produced in Chapter 8.
The book has an associated website: www.cs.rhbnc.ac.uk/books/secprot/This website provides access to all of the tools discussed in this book, and to the protocol examples that are used throughout (as well as others). Readers are recommended to download the tools and experiment with protocol analysis while reading the book. The website also provides exercises (and answers!), as well as a variety of other related material.
Acknowledgements
The authors would like to thank DERA (the Defence and Evaluation Research Agency, UK) and the MoD for funding the Strategic Research Project (SRP) 'Modelling and Analysis of Security Protocols' under which the foundations of the approach were laid down, and the EPRSC (UK Engineering and Physical Sciences Research Council) and ONR (US Office of Naval Research) for funding subsequent developments of the approach. Thanks are also due to Inmos, ONR, DERA and ESPRIT, for funding developments to FDR over the years.
Peter Ryan would also like to thank the Department of Computer Science, Royal Holloway, and Microsoft Research, Cambridge, for hospitality during the writing of this book.
This work has benefited from collaboration with Philippa Broadfoot, Neil Evans, James Heather, Mei Lin Hui, Ranko Lazi´ c and the staff at Formal Systems. It has also been influenced by discussions with and comments from Giampaolo Bella, Steve Brackin, Dieter Gollmann, Andy Gordon, Roberto Gorrieri, Joshua Guttman, Richard Kemmerer, John McLean, Cathy Meadows, Larry Paulson, Matthias Schunter, Paul Syverson and Paulo Verissimo.
Finally, special thanks are due to Coby, Helen and Liz, Kate and Eleanor for moral support.
0201674718P04062001 
