Modelling & Analysis of Security Protocols

About

Features



Description

• Copyright 2001
• Dimensions: 7-3/8x9-1/4
• Pages: 320
• Edition: 1st

• Book
• ISBN-10: 0-201-67471-8
• ISBN-13: 978-0-201-67471-2

Security protocols are one of the most critical elements in enabling the secure communication and processing of information, ensuring its confidentiality, integrity, authenticity and availability. These protocols are vulnerable to a host of subtle attacks, so designing protocols to be impervious to such attacks has proved to be extremely challenging and error prone.   This book provides a thorough and detailed understanding of one of the most effective approaches to the design and evaluation of security critical systems, describing the role of security protocols in distributed secure systems and the vulnerabilities to which they are prey.  The authors introduce security protocols, the role they play and the cryptographic mechanisms they employ, and detail their role in security architectures, e-commerce, e-cash etc. Precise characterizations of key concepts in information security, such as confidentiality, authentication and integrity are introduced and a range of tools and techniques are described which will ensure that a protocol guarantees certain security services under appropriate assumptions.  Modeling and Analysis of Security Protocols provides:

• An in-depth discussion of the nature and role of security protocols and their vulnerabilities.
  
• A rigorous framework in which security protocols and properties can be defined in detail.
  
• An understanding of the tools and techniques used to design and evaluate security protocols.



Sample Content

Online Sample Chapter

Expressing Security Protocol Goals

Table of Contents

Table of Contents

0. Introduction.
Security protocols.
Security properties.
Cryptography.
Public-key certificates and infrastructures.
Encryption modes.
Cryptographic hash functions.
Digital signatures.
Security protocol vulnerabilities.
The CSP approach.
Casper: the user-friendly interface of FDR.
Limits of formal analysis.
Summary.

1. An introduction to CSP.
Basic building blocks.
Parallel operators.
Hiding and renaming.
Further operators.
Process behaviour.
Discrete time.

2. Modelling security protocols in CSP.
Trustworthy processes.
Data types for protocol models.
Modelling an intruder.
Putting the network together.

3. Expressing protocol goals.
The Yahalom protocol.
Secrecy.
Authentication.
Non-repudiation.
Anonymity.
Summary.

4. Overview of FDR.
Comparing processes.
Labelled Transition Systems.
Exploiting compositional structure.
Counterexamples.

5. Casper.
An example input file.
The %-notation.
Case study: the Wide-Mouthed-Frog protocol.
Protocol specifications.
Hash functions and Vernam encryption.
Summary.

6. Encoding protocols and intruders for FDR.
CSP from Casper.
Modelling the intruder: the perfect spy.
Wiring the network together.
Example deduction system.
Algebraic equivalences.
Specifying desired properties.

7. Theorem proving.
Rank functions.
Secrecy of the shared key: a rank function.
Secrecy on nB.
Authentication.
Machine assistance.
Summary.

8. Simplifying transformations.
Simplifying transformations for protocols.
Transformations on protocols.
Examples of safe simplifying transformations.
Structural transformations.
Case study: The CyberCash Main Sequence protocol.
Summary.

9. Other approaches.
Introduction.
The Dolev-Yao model.
BAN logic and derivatives.
FDM and InaJo.
NRL Analyser.
The B-method approach.
The non-interference approach.
Strand spaces.
The inductive approach.
Spi calculus.
Provable security.

10. Prospects and wider issues.
Introduction.
Abstraction of cryptographic primitives.
The refinement problem.
Combining formal and cryptographic styles of analysis.
Dependence on infrastructure assumptions.
Conference and group keying.
Quantum cryptography.
Data independence.

Appendix A. Background cryptography.
The RSA algorithm.
The ElGamal public key system.
Complexity theory.

Appendix B. The Yahalom protocol in Casper.
The Casper input file.
Casper output.

Appendix C. CyberCash rank function analysis.
Secrecy.
Authentication.

Bibliography.
Notation.
Index.

Preface

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



Updates

Submit Errata

