WIXLIB

Prefaceixproperties 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 themodel-checker FDR discussed in Chapter 4.Chapter 6 discusses in more detail some of the CSP modelling that is carried out byCasper, particularly how the hostile environment is modelled to allow efficient analysisby the model-checker.Chapter 7 is concerned with direct verification of CSP models of protocols. Itintroduces the ‘rank function’ approach to proving protocols correct. This allowsproofs to be constructed that verify protocol descriptions of arbitrary size againsttheir requirements. The theorem-proving and bespoke tool support available for thisapproach is also discussed.Chapter 8 addresses the problem of scale. Real-world protocols are very large andtheir analysis is difficult because of the volume of detail contained in their description.This chapter is concerned with ‘simplifying transformations’, which allow extraneousdetail to be abstracted away when checking a protocol against a particular propertyin such a way that verification of the abstract protocol implies correctness of the fullprotocol. The approach is illustrated with the CyberCash main sequence protocol.Chapter 9 discusses the literature on security protocol verification and its historicalcontext. There are a number of different approaches to the problems addressed in thisbook, 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 ongoingresearch, and gives indications of areas for possible further developments and research.One area of current research discussed in this chapter, of particular importance tothe model-checking approach of this book, is the development of techniques basedon ‘data independence’, which allow the results of model-checking to be lifted toprotocol models of arbitrary size.There are three appendices. The first covers some background mathematics andcryptography, introducing the RSA and the ElGamal schemes; the second is an exampleof Casper applied to the Yahalom protocol, containing the input file and the CSP modelproduced by Casper; and the third contains a verification using rank functions of thesimplified 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). Readersare recommended to download the tools and experiment with protocol analysis whilereading the book. The website also provides exercises (and answers!), as well as avariety of other related material.AcknowledgementsThe authors would like to thank DERA (the Defence and Evaluation Research Agency,UK) and the MoD for funding the Strategic Research Project (SRP) ‘Modelling andAnalysis of Security Protocols’ under which the foundations of the approach werelaid down, and the EPRSC (UK Engineering and Physical Sciences Research Council)and ONR (US Office of Naval Research) for funding subsequent developments of

xPrefacethe approach. Thanks are also due to Inmos, ONR, DERA and ESPRIT, for fundingdevelopments to FDR over the years.Peter Ryan would also like to thank the Department of Computer Science, RoyalHolloway, and Microsoft Research, Cambridge, for hospitality during the writing ofthis book.This work has benefited from collaboration with Philippa Broadfoot, Neil Evans,James Heather, Mei Lin Hui, Ranko Lazić and the staff at Formal Systems. It hasalso been influenced by discussions with and comments from Giampaolo Bella, SteveBrackin, Dieter Gollmann, Andy Gordon, Roberto Gorrieri, Joshua Guttman, RichardKemmerer, John McLean, Cathy Meadows, Larry Paulson, Matthias Schunter, PaulSyverson and Paulo Verissimo.Thanks also to Giampaulo Bella, Neil Evans, Dieter Gollmann, Mei Lin Hui,Matthias Schunter and Paulo Verissimo for their careful reading of various parts ofthis book, and for their suggestions for improvement.Finally, special thanks are due to Coby, Helen, and Liz, Kate, and Eleanor for moralsupport.

Chapter 0Introduction0.1Security protocolsAs with any protocol, a security protocol comprises a prescribed sequence ofinteractions between entities designed to achieve a certain end. A diplomatic protocoltypically involves some exchange of memoranda of understanding and so on, intendedto establish agreement between parties with potentially conflicting interests. Acommunications protocol is designed to establish communication between agents, i.e.set up a link, agree syntax, and so on. Even such mundane, everyday activities aswithdrawing money from an ATM or negotiating a roundabout involve protocols.The goals of security protocols, also known as cryptographic protocols, are toprovide various security services across a distributed system. These goals include: theauthentication of agents or nodes, establishing session keys between nodes, ensuringsecrecy, integrity, anonymity, non-repudiation and so on. They involve the exchangeof messages between nodes, often requiring the participation of a trusted third party orsession server. Typically they make liberal use of various cryptographic mechanisms,such as symmetric and asymmetric encryption, hash functions, and digital signatures.In some cases further devices like timestamps are also used. We will explain theseterms more fully shortly.The difficulty of designing and analyzing security protocols has long beenrecognized. This difficulty stems from a number of considerations: The properties they are supposed to ensure are extremely subtle. Even theapparently rather simple notion of authentication turns out to harbour a numberof subtleties and comes in various flavours. The precise meaning, or rathermeanings, of this concept remain hotly debated. These protocols inhabit a complex, hostile environment. To evaluate themproperly we need to be able accurately to describe and model this environmentand this will have to include the capabilities of agents deliberately trying toundermine the protocol. In this book we will refer to such a hostile agent as1

2CHAPTER 0. INTRODUCTIONFigure 1: Setting up a secure channelan intruder; in the literature other terms such as ‘spy’, ‘enemy’, ‘attacker’,‘eavesdropper’ and ‘penetrator’ are also used. Capturing the capabilities of ‘intruders’ is inevitably extremely difficult.Arguably it is impossible, but at least we may hope to make goodapproximations that can be progressively enhanced as new styles of attackcome to light. Besides manipulating messages passing across the network, theycould include cryptanalytic techniques, monitoring tempest emanations, timing,power fluctuations, probabilistic observations and other nefarious activities as‘rubber hose-pipe cryptanalysis’ (non-mathematical techniques for extractingcryptographic variables). By their very nature security protocols involve a high degree of concurrency,which invariably makes analysis more challenging.Security protocols are, in fact, excellent candidates for rigorous analysistechniques: they are critical components of any distributed security architecture, theyare very easy to express, and they are very difficult to evaluate by hand. They aredeceptively simple looking: the literature is full of protocols that appear to be securebut have subsequently been found to fall prey to some subtle attack, sometimes yearslater. In Roger Needham’s remark ‘they are three line programs that people stillmanage to get wrong’.Security protocols have taken on a role for the formal-methods communityanalogous to that of fruit flies to the genetic research community. They are compactand easy to manipulate whilst embodying many of the issues and challenges to thetools and techniques for the analysis and evaluation of security critical systems.To make things rather more concrete let us consider an example: the NeedhamSchroeder Secret-Key (NSSK) protocol. This is one of the earliest such protocols andhas, aside from a rather subtle vulnerability that we will discuss later, stood the test oftime. It forms the basis of the well-known Kerberos authentication and authorizationsystem [65]. It uses purely symmetric encryption algorithms and is designed to enabletwo agents, Anne and Bob say, to set up a secure channel of communication with thehelp of a trusted server, Jeeves. This situation is illustrated in Figure 1.To start with, all the registered agents, including Anne and Bob, share private, longterm keys with Jeeves. These are pair-wise distinct so although each can communicate

0.1. SECURITY PROTOCOLS3securely with Jeeves they are not able to communicate directly with each other. Nowsuppose that Anne wants to start talking privately with Bob. One obvious possibility isfor them to communicate via Jeeves: she sends an encrypted message to Jeeves usingthe key she shares with him; he decrypts this and then encrypts the plaintext using thekey he shares with Bob. This works but rapidly gets very cumbersome: it involves a lotof computation and means that Jeeves becomes a bottleneck and single point of failure.The trick then is just to use Jeeves as and when necessary to establish a new keybetween Anne and Bob so that they can then communicate directly without furtherrecourse to Jeeves. An obvious question is: why not just supply each pair of agentswith a key at the outset? Again this works up to a point but requires roughly N 2distinct keys to be distributed from the start, where N is the number of agents. If Nis large this rapidly becomes impractical, especially as it is likely that most of thesekeys will never be used. It is even worse as we may not know at the outset what theset of users is going to be. Typically, registered users will come and go. Anotherimportant point is that it is desirable to change keys frequently to make the task ofcryptanalysts harder and contain the effect of any compromises. Having a mechanismlike the Needham-Schroeder Secret-Key protocol to set up new keys as required makesthis easier. The long-term keys, ServerKey(a), ServerKey(b) etc., can be stronger andshould less susceptible to cryptanalysis as they tend to carry only a small volume oftraffic.Returning then to the protocol we see that if we start with N users only N keys needbe set up initially and it will be fairly straightforward to supply each new user with anew private key as and when they register.Suppose that Anne shares the key ServerKey(Anne) with Jeeves, whilst Bob sharesServerKey(Bob) with him.The protocol proceeds as follows:Message 1Message 2Message 3Message 4Message 5a JJ aa bb aa b:::::a.b.na{na .b.kab .{kab .a}ServerKey(b) }ServerKey(a){kab .a}ServerKey(b){nb }kab{nb 1}kabThis requires some explanation. First let us explain the notation. Each step of theprotocol is represented by a line in the description. ThusMessage n a b : dataindicates that in the nth step of the protocol agent a dispatches a message data to b.The message in general consists of a number of parts concatenated together. In practiceit is of course possible that this message will not reach b or might reach someone else.For the moment however we are only concerned with presenting the intended progressof the protocol.Terms of the form na denote so-called nonces: freshly generated, unique and(usually) unpredictable numbers. The subscript indicates who generated it, but noticethat this is just a notational convenience; in the real protocol there will typically be

4CHAPTER 0. INTRODUCTIONnothing in the actual value to indicate that it was created by a. We will discuss the roleof nonces more fully shortly.Compound terms can take the forms: {data}k , which denotes the value data encrypted under the key k; m.n, which denotes the text m followed by (concatenated with) the text n.Now we are in a position to walk through this protocol step by step. In the firststep Anne tells Jeeves that she would like to talk to Bob and she supplies the noncena . Jeeves now creates a new key kab and returns the message with nested encryptionindicated in step 2 to Anne. The outer encryption is performed using ServerKey(a)which Anne can strip off. Inside Anne finds the following:na .b.kab .{kab .a}ServerKey(b)The first term is just the value of the nonce she sent to Jeeves in message 1. Sheis expected to check that this value agrees with the value she originally sent out. Wewill return to the significance of this a little later. The second term should be Bob’sname. Again she should check that this agrees with the name in her request of message1. The third term is the new key kab . The last term is encrypted using the key that Bobshares with Jeeves. Anne can’t read this last term but in accordance with the protocol,and assuming that all the other checks have succeeded, she simply forwards it to Bobin the third step. When Bob receives this he is able to strip off the encryption to reveal:kab .a.So he now knows the value of the new key kab and knows that it is intended forcommunication with Anne. He now dreams up a new nonce of his own nb and sends itback to Anne encrypted under kab in message 4. Anne decrypts this to extract nb . Shemodifies this in some standard way – the convention is to subtract 1 – and sends thismodified value back to Bob, again encrypted under kab . Finally Bob decrypts this andchecks that the resulting value agrees with what he expects for nb 1.So, what has all this frantic activity achieved? In informal terms, and assumingthat all has gone smoothly, Anne and Bob end up with shared knowledge of kab . Infact they share this knowledge after message 3 has been received by Bob. So why afurther two messages and yet another of these nonces? Messages 4 and 5 are really justacknowledgement messages to assure each other that the other also knows kab . We seethat by the time Bob receives message 3 he knows that Anne knows kab . Once Annegets message 4 she knows that Bob knows kab and, further, she knows that he knowsthat she knows kab . And so on. We can see that we could go on constructing an infinitechain of acknowledgement messages leading to a tower of states of knowledge aboutknowledge.We should stress though that the conclusions reached by Anne and Bob above arebased on very informal reasoning. On receiving message 3 Bob is reasoning somethingalong the following lines:Apart from me only Jeeves knows ServerKey(b) so only he could havegenerated these terms. Assuming that Jeeves is being honest he wouldonly have generated them in response to a request from Anne and so they

0.1. SECURITY PROTOCOLS5must have been included in a message to Anne encrypted with her longterm key. Hence it could only have reached me if it was forwarded tome by Anne. So Anne received the appropriate message from Jeeves withkab . . .Such chains of reasoning are extremely error prone as we will see in, for example,the analysis of the Needham-Schroeder Public-Key (NSPK) protocol. We will see inthis book how one can reason about protocols in a fully formal and indeed largelyautomated way.The goal of this protocol is authenticated key distribution. In particular it shouldfulfil Anne’s request to provide the means for her to have a private, authenticatedconversation with Bob. What she wants at the end of the protocol run is to be surethat Jeeves has supplied her and Bob, and only her and Bob, with a freshly generatedsession key K that they can now use in further exchanges. As long as this key is onlyknown to her and Bob she can be confident that messages she sends out encrypted withK can only be read by Bob, and furthermore that messages she gets back encryptedwith K must have come from Bob and will also be safe from prying eyes.This protocol illustrates a number of interesting issues that will crop up repeatedlythroughout this book. Ensuring that Anne and Bob are really justified in havingconfidence in the services provided by this protocol is no easy task. First, we needto be sure that intruders can’t undermine this goal by manipulating the messages invarious (non-cryptographic) ways. This depends on the correctness of the protocoldesign, and is the principal concern of this book. It is also possible that poorlydesigned or unsuitable cryptographic primitives might lead to vulnerabilities that canbe exploited. By and large we will not deal with such problems except to discuss tosome extent how features of the crypto algorithms might interact with the protocolitself to give rise to vulnerabilities. We should also note that, from Anne’s point ofview say, she needs to place confidence in certain, remote parts of the system. Shehas to trust Jeeves to act according to the protocol description and to employ a ‘good’key generation scheme. She also needs to trust Bob. If Bob is going to compromisehis key, either deliberately or simply through carelessness (insecure storage of the keymaterial), then all hope of secrecy or authentication is lost. On the other hand sheshould not need to place any great faith in the communications medium. Quite thecontrary: she should typically assume that the medium is entirely open to maliciousagents trying everything in their power to undermine the security goals.Notice that the first message from the initiator, Anne, goes out in the clear. Thereis thus nothing to ensure the secrecy or integrity of this message. We are assuming thatthe intruder learning that Anne wants to talk to Bob is not a problem. We will also seelater that there is no use to the intruder of learning the value of na . Thus lack of secrecyof these values is not a problem unless we are worried about traffic analysis. As tothe integrity, it is certainly the case that there is nothing to prevent the intruder alteringthese values. However the only effect will be for Anne to back out when she finds thatthe values in the reply from Jeeves do not agree with her records. A denial of serviceattack can be launched in this way, but secrecy and authentication are not breached.Another point is that we are assuming that the protocol is using a form of blockcipher (which operates on fixed length blocks of plaintext and ciphertext) rather than

6CHAPTER 0. INTRODUCTIONsay a stream cipher (which converts plaintext to and from ciphertext one characterat a time). We wil

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 .