Home

Manual - Department of Computer Science

1. From Kb px and Km pxs the intruder is able to deduce Km 6 Kb using the given deduction or in a system with a server using the server as an oracle and hence Kb Encoding oracle properties of an honest agent in this way can sometimes allow that agent to be left out of the system checked but still allow attacks to be found often searching a smaller state space Answer to Exercise 7 The script should be similar to the following Needham Schroeder Shared Key Protocol with key compromise Free variables A B Agent S Server na nb Nonce SKey Agent gt ServerKey 68 B ANSWERS TO THE EXERCISES kab SessionKey InverseKeys SKey SKey kab kab Processes INITIATOR A S na knows SKey A RESPONDER B nb knows SKey B SERVER S kab knows SKey Protocol description 0 gt A B A B 1 A o S A B na 2 S gt A na B kab SKey A 3 S gt B kab A SKey B A Bl 4 B gt A nb kab 5 A gt B nb nb kab Specification Agreement B A Agreement A B L Secret A kab B Secret B kab A Actual variables Alice Bob Ivor Agent Stan Server Na Nb Ni Nonce Kab SessionKey InverseKeys Kab Kab Inline functions symbolic SKey System INITIATOR Alice Stan Na RESPONDER Bob Nb SERVER Stan Kab Intruder Information Intruder Ivor IntruderKnowledge Alice Bob Ivor Stan Ni SKey Ivor Crackable Sess
2. with the message to the right of the turnstile represents the new message that the intruder can deduce and the messages to the left represent the messages needed for this deduction For example forall k1 k2 SessionKey pks ServerPublicKey k1 pks k2 pks k1 k2 Exercise 5 6 The above deduction is relevant to the TMN protocol see Exercise 3 of this section if the intruder knows two distinct session keys both encrypted with the same server s public key then he can replay them at the server and use the server as an oracle to learn the Vernam encryption of the session keys Investigate the effect of modelling the TMN protocol using a system without a server but where the intruder is given the above extra deduction d 5 11 Key compromise Some protocols are subject to key compromise attacks where a key is compromised either through cryptographic techniques or through the key being stolen and then used to lead to a failure of authentication in a sub sequent session All keys of a particular type can be declared to be compromisable by including a line like the following in the Intruder Information section 32 5 CARRYING ON Crackable SessionKey The key will be compromised and passed to the intruder when all agents whose runs overlap in time with any agent using that key have finished their runs Exercise 5 7 Use Casper to model the following slightly simplified version of the Needham Schroeder S
3. 1 A and nth decrypt v pka 2 now and decryptable nth decrypt v pka 3 SK B lt n2 nth decrypt nth decrypt v pka 3 SK B 1 gt 6 B gt 1 B n2 pka PK A In the test following message 5 and the assignment preceding message 0 we have made use of a few functions provided by Casper e The function decryptable takes a message and a key and tests whether the message may be decrypted with the key that is it tests whether the message is encrypted with the inverse of the key e The function decrypt takes a message and a key and decrypts the message with the key it should be applied only when the key is the correct decrypting key 5 8 Detecting type flaws 29 e The function head returns the first field from a message The function nth _ n returns the nth field from a message Thus the test following message 5 checks that message 3 was encrypted with the inverse of the key received in message 5 which B expects to be A s public key that the first field inside the encryption was A s identity and that the second field was encrypted with B s public key The assignment preceding message 6 assigns n2 to the contents of the inner encrypted component The way in which B processes message 3 when he receives the key in message 5 is of a fairly standard form so I intend to introduce a primitive action unpack_and_check representing this processing in a future release of Casper 5 8 Detecting ty
4. Hall 1985 Eldar Kleiner A web services security study using Casper and FDR DPhil Oxford University 2008 Gavin Lowe An attack on the Needham Schroeder public key authentication protocol Information Processing Letters 56 131 133 1995 Gavin Lowe Breaking and fixing the Needham Schroeder public key protocol using FDR In Proceedings of TACAS volume 1055 of Lecture Notes in Computer Science pages 147 166 Springer Verlag 1996 Also in Software Concepts and Tools 17 93 102 1996 Gavin Lowe A hierarchy of authentication specifications In Pro ceedings of 10th IEEE Computer Security Foundations Workshop 1997 Gavin Lowe Towards a completeness result for model checking of security protocols extended abstract In 11th Computer Security Foundations Workshop 1998 Gavin Lowe Analysing protocols subject to guessing attacks In Proceedings of WITS 702 2002 Gavin Lowe and Bill Roscoe Using CSP to detect errors in the TMN protocol JEEE Transactions on Software Engineering 23 10 659 669 1997 Catherine A Meadows Analyzing the Needham Schroeder public key protocol A comparison of two approaches In E Bertino H Kurth G Martella and E Montolivo editors ESORICS 96 LNCS 1146 pages 351 364 1996 Roger Needham and Michael Schroeder Using encryption for au thentication in large networks of computers Communications of the ACM 21 12 993 999 1978 A W Roscoe and P J Broadfoot Proving secur
5. InternalKnown vPublic Nonce InternalKnown vPublic Nonce InternalUnknown Nel Nonce External InverseKeys vSecret vSecret Inline functions symbolic ServerKey HSystem RESPONDER Alice Alice Nel 7 2 Assumptions and Threshold Theorems 43 We now present the thresholds for the authentication specifications Consider specifications of the form NonInjectiveAgreement a b vs Agreement a b vs WeakAgreement a b and Aliveness a b the sys tem should be constructed as follows e For non injective aliveness and weak agreement specifications one ex ternal b should be constructed and for injective specifications two ex ternal b s should be constructed the arguments to the external b s should differ only in data independent values e Two agent identities one honest and one dishonest e Sufficient External values such that external agents do not generate the same values for data independent variables e For every variable v in vs a unique InternalUnknown value vs e A variable p that is of every type and subtype and has status InternalUnknown and InternalKnown As an example we again consider the simplified Yahalom protocol for the specification Agreement a b kab Free variables a b Agent s Server na Nonce NonceNA nb Nonce NonceNB kab SessionKey ServerKey Agent gt ServerKeys InverseKeys kab kab ServerKey ServerKey Processes INITIATOR a na knows ServerKe
6. Intruder Information Intruder Mallory IntruderKnowledge Alice Bob Mallory Sam SKey Mallory Crackable SessionKey 3 This produces the following attack on secrecy 0 Alice Bob 1 Alice Isam Bob 0 Kab skey Alice Time passes 1 LT Alice Sam Bob 0 Kab skey Alice 2 Sam I Bop Alice 1 Kab skey Bob Time passes d I Bob Sam TAlice 1 8 Kab sKey Bob 2 Sam T Alice Bob 2 Kab skey Alice Time passes Kab has been compromised 1 I Alice Sam Bob 2 Kab skey Alice 2 Sam gt I Bob 1 Alice 3 Kab skey Bob Di T sam Bob Alice 9 Kab skey Bob The intruder knows Kab The intruder plays ping pong with Sam keeping the key delivery messages current until he is able to crack the key Answer to Exercise 9 The original protocol can be modelled as follows B 3 Answers to exercises from Section 5 Encrypted Key Exchange Free variables a b Agent na nb Nonce k SessionKey pk PubKey sk SecKey passwd Agent x Agent gt Password InverseKeys passwd passwd pk sk k k Processes INITIATOR a pk sk na knows passwd a b RESPONDER b nb k knows passwd a b Protocol description 0 gt a b 1 a gt b a pk passwd a b 2 b gt a i k pk passwd a b 3 a gt b na k 4 b gt a fna nb k 5 a gt b nb k Specification Secret a passwd a b b Secret a k b Agreement
7. this attack should be regarded as false as providing kab is freshly generated by the server kab would not be known to the intruder To avoid the problems above the following system would be recommended for analysing the simplified Yahalom protocol Actual variables Alice Mallory Agent Alice Server Kabs1 Kabs2 SessionKey InternalUnknown Kabp SessionKey InternalKnown Nil Nonce InternalKnown Nil Nonce InternalUnknown 7 3 System Generation 45 Nel Ne2 Nonce External InverseKeys vSecret vSecret Inline functions symbolic ServerKey HSystem RESPONDER Alice Sam Nel RESPONDER Alice Sam Ne2 Note that the types now share no variables in common and there is no overlap between InternalUnknown and InternalKnown values for kab 7 3 System Generation The task of specifying the actual variables and external agents can be onerous and therefore Casper has the ability to automatically generate the actual vari ables and the external agent definitions To do this the Actual variables section should be left blank aside from the type of the intruder The flag GenerateSystem True should then be specified in the System section An example is show below for the simplified Yahalom protocol above Actual variables Mallory Agent Inline functions symbolic ServerKey HSystem GenerateSystem True Intruder Information Intruder Mallory IntruderKnowledge ServerKey Mallory UnboundPa
8. Alice gt Bob Na Alice PK Bob 2 Bob gt I Alice Na Nb PK Alice 2 I_Mallory gt Alice Na Nb PK Alice 3 Alice gt I Mallory Nb PK Mallory 3 I Alice gt Bob Nb PK Bob The intruder knows Nb Checking assertion AuthenticateINITIATORToRESPONDERAgreement_na_nb T SYSTEM_1 Attack found Top level trace Alice believes she is running the protocol taking role INITIATOR with Mallory using data items Na Nb Bob believes he has completed a run of the protocol taking role RESPONDER with Alice using data items Na Nb System level 0 gt Alice Mallory 1 Alice gt I Mallory Na Alice PK Mallory 1 I Alice gt Bob Na Alice PK Bob 2 Bob gt I Alice Na Nb PK Alice 2 I Mallory gt Alice Na Nb PK Alice 3 Alice gt I Mallory Nb PK Mallory 3 I Alice gt Bob Nb PK Bob Checking assertion AuthenticateRESPONDERToINITIATORAgreement_na_nb T SYSTEM_2 No attack found Done Figure 2 Output from CasperFDR during checking 3 2 Running Casper 13 3 2 Running Casper The compiler is written in the functional programming language Haskell Executing the shell script casper will start up Haskell and load in the Casper files The compiler is then run by typing compile filename where the path for the input file is given by filename sp1 Note that the quotes are necessary The suffix spl stands for Security Protocol Languag
9. Np Nonce InternalKnown Nai Na2 Nonce InternalUnknown NonceNA Nb1 Nb2 Nonce InternalUnknown NonceNB Nei Ne2 Nonce External InverseKeys Kabp Kabp Kabs1 Kabs1 Kabs2 Kabs2 Inline functions symbolic ServerKey System RESPONDER Bob Sam Ne1 RESPONDER Bob Sam Ne2 Intruder Information Intruder Mallory IntruderKnowledge Alice Bob Mallory Sam Np ServerKey Mallory UnboundParallel True A 3 Simplifying transformations input script Free variables A B Agent na nb Nonce PK Agent gt PublicKey SK Agent gt SecretKey kab SessionKey 59 ts TimeStamp InverseKeys PK SK kab kab f HashFunction Processes INITIATOR A na kab knows PK SK A RESPONDER B nb kab knows PK SK B Protocol description 0 gt A 8 1 A gt B 1na A ts PK B 2 B gt A na nb A ts PK A 3 A gt B f na A 2 4 B gt A na A PK A Specification Secret A na B Agreement A B na nb Agreement B A na nb Simplification RemoveFields TimeStamp SwapPairs Nonce Agent RemoveHash f Agent B Answers to the exercises B 1 Answers to exercises from Section 2 Answer to Exercise 1 The only necessary changes to the input file are in the Protocol description section which should be edited to the following Protocol description 0 gt A 8 1 A gt B na PK B 2 B gt A na nb B PK A
10. When FDR is used to check whether initiator Alice is correctly authenti cated it produces an attack which can be rewritten as 0 3 MalloryAtice Bob Nm Alice px Bob a 1 Malloryatice Sam Bob a 2 Sam MallorYAtice PKb Bob sks sam 04 Bob Sam Alice a d Sam Bob PKa Alice sxs sam a b Bob Malloryatice Nm Nb pk Alice 0 3 Malloryn Alice Nm Nb px Alice 6 4 Alice Mallorysan Nb a T Mallory Alice Bob Nb pK Bob In run a Mallory imitates initiator Alice in a run of the protocol with Bob Messages a 1 and a 2 serve only to get the server into the right state to accept a message 4 there is no reason why they have to be out of order as above When Bob sends a nonce challenge in message a 6 Mallory sends the message to Alice as a message 3 which Alice interprets as coming from an agent Nb Alice therefore requests Nb s key in message 3 4 but this allows Mallory to learn the value of Nb and so answer Bob s nonce challenge This attack was described by Meadows in Mea96 Answer to Exercise 5 The input script should look something like A protocol to illustrate the use of algebra Free variables 66 a b Agent kab SessionKey PK Agent gt PublicKey SK Agent gt SecretKey InverseKeys PK SK Processes INITIATOR a kab knows PK SK a RESPONDER b knows PK SK b Protocol description B ANSWERS TO THE EXERCISES 0 gt
11. a message along with a list of the variables that should be bound Some example events include a sends message 2 containing na nb A sends message 2 to b containing Na for na nb A receives message 2 from B containing Na for Na Nb for Nb Note that the sender and receiver of a message and any variable in the containing clause may be either an actual variable or a free variable Whilst most of the time free variables will be preferable it can result in checks taking too long if this is the case it is recommended that the user instead substitutes some free variables for actual variables The list of bound variables in the events allows the user to force messages to contain the same data item in particular any data items in the same scope are required to match For example in the specification if a receives message 2 from b containing na then previously b sends message 1 containing na a the na and a are required to be the same However in the specification if a receives message 3 from b containing na then previously b sends message 1 containing na nb a and previously a sends message 2 containing nb the nb is not required to be the same The scope of the variables can be defined as follows e Any free variable on the left hand side of an implication is in scope on the right hand side Ina formula such as p A oq any free variable in p is in scope within q An example input file is shown below for the Needham Schroeder Pu
12. abort the run TimeStamp 0 O MaxRunTime 0 The function SKey which returns the key an agent shares with the server is defined by Functions SKey Alice SKey Bob SKey Mallory Kms 18 4 CASE STUDY THE WIDE MOUTHED FROG PROTOCOL VVe assume that the intruder initially knovvs all the agents identities and his own key Intruder Information Intruder Mallory IntruderKnowledge Alice Bob Mallory Sam SKey Mallory When the above file is compiled using Casper and then checked using FDR FDR fails to find any attack upon this small system 4 3 Second system We now consider a slightly different system where the agent Alice can run the protocol once as initiator and once as responder possibly concurrently We suppose that Bob is absent so doesn t run the protocol S5ystem INITIATOR Alice Sam Kab RESPONDER Alice SERVER Sam Note that this change to the system involves changing precisely one line of the input file When we check this system FDR discovers that the protocol does not correctly authenticate the initiator Bob to responder Alice By exploring the debug tree and using interpret we can discover that the attack takes the following form a l Alice gt Sam Bob 0 Kab skey Alice 2 Msam Alice Bob 0 Kab sKey Alice The intruder simply replays Alice s first message back at her which she interprets as being message 2 of a run initiated by Bob 4 4 Third s
13. an agent s identity 5 9 Algebraic equivalences Many cryptographic functions have interesting algebraic properties These are defined in a separate section under the Equivalences heading As an example the lines Equivalences forall k1 k2 m m k1 k2 m k2 k1 would express the property that the encryption property used is commuta tive written mathematically as Vk1 k2 me m ri he lm y hk Within such lines bound variables for which no type is given each of 1 k2 and m in this case are interpreted as ranging over all messages If such an 5 10 Intruder deductions 31 equivalence only applies for some of the variables being of a particular type then such variables should be typed within the quantification for example forall k1 k2 SomeKeyType m m ki k2 m k2 k1 Exercise 5 5 Investigate the following protocol 1 a b a kab px SK a 2 b a b kab px a sK 0 where PK and SK return an agent s public and secret key respectively and where the intention is to establish a shared session key kab in a setting where the encryption used is commutative d 5 10 Intruder deductions It is sometimes useful to be able to define additional ways in which the intruder can deduce new messages Each deduction defines a way in which the intruder can deduce some message from some collection of other messages that he knows Each deduction is defined around a turnstile 1
14. arb a b 1 a gt b Ha kab PK b SK a a b 2 b gt a 446 kab PK a SK b Specification Secret b kab Tal Actual variables A B M Agent K1 K2 SessionKey Functions symbolic PK SK System INITIATOR A K1 RESPONDER B Intruder Information Intruder M IntruderKnovledge A B M PK K2 SK M Equivalences This is the interesting bit encryption is commutative forall ki k2 m The following specifies that the m ki k2 m k2 k1 B 3 Answers to exercises from Section 5 67 The following attack can be discovered 0 A M 1 4A M HA K sk A bPK M 1 14 o B K pk B SK A B believes K1 is a secret shared with A The intruder knows K1 The first message 1 is somewhat surprising as it doesn t seem to match the protocol description However it is equivalent under the algebraic equiva lence to 1 A M A KI bk M sk a which does match the protocol description From the message in its first form the intruder is able to derive A K1 5x 4 and hence LA K1 sx a pK a which is equivalent to the fakes message 1 in the attack Answer to Exercise 6 Taking the input script from Exercise 3 removing the server and adding the given deduction will allow the following attack to be found 2 Isam Bob Alice Bob believes Kb is a secret shared with Sam Alice 3 Bob Isam Alice Kb prs The intruder knows Kb
15. et pes ee y AAA E ES 5 4 Protocol specifications a 5 5 Splitting large messages sy bs ab all m x Ba eS 5 6 Agents withdrawing heck Gace Sa Be 5 7 Delaying decryption di a dee ie as Ohare wok Se 5 6 Detecting type flaws lt a al ee bs ow RAS s 5 9 Algebraic equivalences 5 10 Intruder deductions 0000004 10 10 13 13 15 15 17 18 18 19 20 ii 8 9 CONTENTS 5 11 Key compromise Ca b a ne 5 12 Password guessing attacks Secure channels 6 1 Old style secure channels 6 2 Nevv style secure channels Using data independence techniques 7 1 How to use data independence techniques 7 2 Assumptions and Threshold Theorems 7 3 System Generation 4 246 6 ee Aaa d TA Repeat Sections s ine ara za a Sat ri 7 5 Minimising state space explosion 7 6 Current limitations tera So ola A de Specifying Properties using Temporal Logic Simplifying transformations 10 Conclusion A Example input scripts A 1 A standard input script di 25 4 a 6 A 2 An input script using data independence techniques Simplifying transformations input script Ansvvers to the exercises B 1 Answers to exercises from Section2 B 2 Answers to exercises from Section3 B 3 Ans
16. generated For example within the script of Appendix A 2 this section is as follows Processes INITIATOR A knows SKey A generates na RESPONDER B S knows SKey B generates nb SERVER S knows SKey generates kab The values na nb and kab are of data independent types and so are freshly generated for each run By contrast if this protocol was being modelled without the use of data independence techniques then this section would be defined as follows INITIATOR A na knows SKey A RESPONDER B nb knows SKey B SERVER S kab knows SKey Use of data independence techniques also affects the Free variables section Each free variable can now be specified with a subtype if this is done then internal agents will only use actual variables that have the same subtype for that free variable The Actual variables section is also altered with each data independent variable not only receiving a subtype but also a status that is one of the following InternalKnown The variable should be used by internalised agents when communicating with an agent they think is dishonest i e Known as in known to the intruder InternalUnknown The variable should be used by internalised agents when communicating with an agent they think is honest External The variable should be used by external agents only For example the nonces in the Needham Schroeder Public Key protocol could be declared as follows Free variables na Nonce NonceNA nb No
17. implementation the agents would not be able to tell whether the message they receive is of the expected form We therefore allow the agents to accept an arbitrary message of the expected type or a special value Garbage representing a random sequence of bits invented by the intruder The notation can be used not only for the case where a message is simply forwarded without decryption but also more generally where the sender and receiver treat the message differently For example consider the following version of the 7 message Needham Schroeder Public Key Protocol a gt 8 ib 5 gt 6 16 PK b sskts a b na a px 5 2 gt 5 s b fa PK a ssk a b a b a na nb b pkta a b a b nb py ID ON so do The purpose of message 2 is for a to obtain b s public key However writing PK b in the protocol description is rather misleading a should be willing to accept any key call it pkb in this message and then use that key pkb for the rest of the protocol We hope that the form of message 2 ensures that the key that a receives really is PK b but this is something we need to check indeed in Exercise 2 we will see an example where this is not the case The following Casper protocol description treats PX b and PK a as required Protocol description 0 gt a b 1 2 gt 8 b 2 s a ib PK b pkb SSK s 3 a 0 na a pkb PK b 4 b m s a 5 s gt b a P
18. kab nb ras 2 Tn the original version of the protocol the ticket included a timestamp which we omit here for simplicity tickb 24 5 CARRYING ON Exercise 5 2 Adapt the script for the seven message adapted Needham Schroeder Public Key Protocol to remove the identities from within the en crypted components of the key delivery messages messages 3 and 6 1 a s 0 2 5 gt 6 PK b ssK 5 3 a b ina a pK 4 b s a gt b PK a ssx a 6 b a b a na nb b pk a 7 a ob a b nb PKO Analyse this protocol using Casper and FDR amp 5 2 Vernam encryption The notation m m represents the bit wise exclusive or also known as Vernam encryption of m and m The receiver of a message containing a Vernam encryption should be able to create at least one of m and m so as to obtain the other Exercise 5 3 Consider the TMN protocol from TMN90 1 A S B ka oks 225 3 B S A kb ots 4 9 kae kb where pks is the public key of server s ka and kb are session keys and the intention is to establish a new session key kb shared between A and B Use Casper and FDR to analyse this protocol you should discover an attack Suggest how to adapt the protocol to prevent this attack and then investigate whether the adapted protocol is secure d 5 3 Hash functions Hash functions used in a Casper script should be declared as having the type HashFunct
19. msg channel spec msg channel prop session channel spec C THE CASPER SYNTAX IntruderProcesses process name process name StaleKnowledge True False Crackable crackable type crackable type type name C time Guessable type name 17 type name section Channels old channel spec channel spec authenticated 21 secret direct 2 msg channel spec session chanmel spec line no msg channel prop c NF NRA NRA I NR NR Session Stream injective symmetric line no line no C 13 Simplifying transformations script simplifying script n free vars section processes section prot desc section spec section simplifying section C 14 Simplifications section simpl section Simplifications simpl C 14 Simplifications section 79 simpl encrypt type hash type type RemoveFields type name type name qe RemoveHashedFields hash type RemoveEncryption encrypt type RemoveHash hash type SwapPairs C type name type name 97 1 Coalesce C type name type name RemovePlainAndEnc type YU type name y identifier C type type name encrypt type hash
20. protocol The two parts are themselves further subdivided by section headers these are lines beginning with Comments may be added to the file by begin ning the relevant lines with Any logical line may be split across two or more physical lines by preceding any non logical linebreak by a backslash CQ 2 2 The protocol definition The first part of the input file defines the generic operation of the protocol 2 2 1 Protocol description The main part of the definition of the protocol is the definition of the sequence of messages in the protocol This appears under the heading Protocol description The notation used is similar to the standard method of describing pro tocols as in Figure 1 However we have to adopt the notation slightly to make the definition fully formal In order to represent the protocol in ascii we use the notation m k for message m encrypted with key k denoted by m in Figure 1 Thus the three messages can be represented by 1 A gt B na A PK B B gt A na nb PK A 3 A B nb PK B Casper adds extra fields to each message representing the apparent sender and intended receiver so there is no need to include these explicitly in the normal case where the intruder can be expected to know all the agents identities but see Section 5 8 for a discussion of this point We also need some way of starting the protocol run off How does A know that he should run the
21. protocol with B We assume that the run is initiated by A receiving some message from a user or the environment including B s identity We represent this by an extra message in the protocol description 2 2 The protocol definition 5 0 gt A A B The absence of a sender field in the above line represents that this message is sent by the environment We assume that such messages cannot be overheard by the intruder neither can they be faked The complete protocol description then takes the form Protocol description 0 gt 4 8 A gt B na A PK B B gt A na nb PK A A gt B nb PK B Ne 2 2 2 Free variables The types of the variables and functions that are used in the protocol defini tion are defined under the heading Free variables this definition takes the following form Free variables A B Agent na nb Nonce PK Agent gt PublicKey SK Agent gt SecretKey For example in the protocol description the variables na and nb should be taken to be of type Nonce This information is used in defining the types of valid messages in the system The functions PK and SK return an agent s public key and secret key respectively these functions will be defined later We term these free variables because they will be instantiated with actual values when we consider an actual system running the protocol Under the same heading is a definition of which keys are inverse
22. suitable for checking using FDR This version of the manual assumes some familiarity with FDR at least to the level covered by the first three parts of the FDR2 manual For97 In the next section we give a gentle introduction to the Casper syntax by informally explaining an example input file In Section 3 we describe how to use Casper to compile the CSP code from the input file how to run the 2 2 AN EXAMPLE INPUT FILE code using FDR and how to interpret the output In Section 4 we present a case study of the Wide Mouthed Frog protocol In Section 5 we describe how to model some more features that often crop up in security protocols In Section 9 we describe an extension to Casper that supports the simplifying transformations of HL99 We sum up in Section 10 2 An example input file An example input file is given in Appendix A and is included in the file NS3 spl in the standard Casper distribution and in the Casper example li brary Cas98 This file gives a definition of the 3 message version of the Needham Schroeder Public Key Protocol NST8 This protocol would nor mally be described as in Figure 1 where PX A represents A s public key and m represents message m encrypted with key k 1 A B na Ajex p 2 3 4 B A na nb pray 3 4 gt 5 A B nb ps Figure 1 The Needham Schroeder Public Key Protocol In the protocol A seeks to establish a connection with B and to achieve mutual authentic
23. to further security failures 33 Exercise 5 9 The Encrypted Key Exchange Protocol EKE seeks to achieve key establishment and mutual authentication using a poorly chosen password a b a pk passwd a b eb ELE Pastel a b na b a na nb a b nb X wow Here passwd a b is a potentially poorly chosen password shared between a and b pk is an asymmetric key created by a and k is a symmetric key created by b Model and analyse this protocol Then adapt the protocol so that pk is replaced by a symmetric key you should find an attack d 6 Secure channels Some security protocols are designed to be layered on top of a secure trans port protocol such as TLS which provides additional security services acting as some kind of secure channel over which the messages are passed There are two distinct way to specify the services provided by such secure channels each within a Channels section 6 1 Old style secure channels The original style of designating the properties of channels allowed the fol lowing two properties to be specified secret the intruder cannot learn the contents of a message sent over the channel authenticated if agent 5 receives messages on the channel apparently from a then a really did send the messages intended for b and b receives a prefix of the messages sent by a For example Channels authenticated secret 34 6 SECURE CHANNELS All chann
24. type type type
25. 3 A o B nb PK B Ansvver to Exercise 2 Predictable nonces may be modelled by including those nonces within the intruder s initial knowledge With the Needham Schroeder protocol the nonces Na and Nb may be made predictable by editing the Intruder Information section to 60 B ANSWERS TO THE EXERCISES Intruder Information Intruder Mallory IntruderKnowledge Alice Bob Mallory Na Nb Nm PK SK Mallory Answer to Exercise 3 Having a line of the form INITIATOR Alice Na PKb in the System section would have the effect that Alice would use Bob s public key PKb in every run of the protocol including those runs with an agent other than Bob This clearly isn t what we want In general none of the parameters of a process should depend upon the identity of the other agent taking part in the protocol run B 2 Answers to exercises from Section 3 Answer to Exercise 1 When FDR is used to test the assertion dealing with secrecy the test should fail The attack can be interpreted as follows 0 Alice 5 Bob 1 Alice I Bob Va pK Bob 1 Mallor Bob Na Pk Bos Bob believes he is running the protocol taking role RESPONDER with Mallory using data items Na Nb 2 Bob Mallory Na Nb Bob px Mallory 2 Ino Alice Na Na Bob pk Alice Alice believes Na is a secret shared with Bob The intruder knows Na Alice tries running the protocol with Bob but Mallory intercepts the first
26. A B 1 A gt B na 2 B gt S nb A na SKey B S gt A nb B kab na SKey A 3b S gt A A kab nb SKey B enc 5 6 Agents withdrawing 27 da A gt B enc 7 A kab nb SKey B 4b A gt B nb kab Here we have split message 3 into two messages now numbered 3a and 3b and we have split message 4 into two messages now numbered 4a and 4b A few moments thought should convince you that this approach will identify the same attacks The above protocol is included in the Casper example library 98 The one proviso to this approach is that if an agent learns a key in one part of the original message that he then uses to decrypt another part of the message then when the message is split the parts must be ordered appropriately in the above example message 4a must precede message 4b because B learns kab from message 4a which he needs in order to decrypt message 4b It is also worth mentioning that splitting messages too much will in crease the time taken by a check because it will increase the number of ways in which simultaneous runs can be interleaved It would probably be counter productive to split message 2 above it is arguable whether splitting message 3a further would be useful As a rule of thumb I tend to split mes sages if they have more than about 100 200 possible forms although more experience on this question would be useful 5 6 Agents withdrawing Sometimes it
27. Casper A Compiler for the Analysis of Security Protocols User Manual and Tutorial Gavin Lowe Philippa Broadfoot Christopher Dilloway Mei Lin Hui Version 1 12 September 28 2009 Oxford University Computing Laboratory Wolfson Building Parks Road Oxford OX1 3QD UK CONTENTS Contents 1 Introduction 2 An example input file 2 1 Overview of input fle v4 2a As 2 2 The protocol definition 2 2 1 Protocol description Deal ae eae eae 2 2 2 Free variables m z A pk Me kop sl 22 Processes Teira 5 end Real s Fok WR pod 2 2 4 Specifications ede n k l oe R 2 3 The system definition ae ee x add a 2 3 1 Type definitions n A eee 00663 220 Finctions us S XA 2 3 3 System definition x a 2 3 4 The intruder lt ce m i sb a 3 Using Casper srl Usa Casper a arpa how EPO 3 2 Running da 3 3 Running the output file vviihFDR 4 Case study The VVide mouthed frog Protocol 4 1 Modelling the protocol hake ke See SO pa 4 2 First system m AD aa r m a am 4 3 Second system a an m des Anke tea Sd a d 4 4 Third system x x A n oh ce ALG Fo rth Systeni ea set Bac aie am BS ney s EE dea 4 6 Timestamp Details 5 Carrying on o A 5 2 Vernam encryption Fey ie a a 547 Hash functi6nss s La e ce
28. K a pka SSK s 6 b gt a na nb b pka 7 PK a 7 a 5 b nb pkb PK b The notation can also be used to model protocols that make use of either key certificates or tickets For example the Kehne Langendorfer Scoenwalder protocol has two phases 5 1 The notation 23 e An initial exchange between A and B which establishes a ticket of the form A kab private Where kab is a session key and Private B is a key known only to Bt e A re authentication phase where the ticket is re used to re establish authentication We can model the second phase as follows Protocol description 0 gt A B Shared A B 7 kab A Shared A B Private B A gt B na tickb A kab Private B B gt A nb na kab A gt B nb kab w Ne A receives three things in message 0 The identity of the agent B with whom A will run the protocol as normal e The key kab to be used in the exchange which we model as the result of a function application Shared A B e A ticket of the form A Shared A B private p Which A stores in the variable tickb One can think of an environmental message such as this as representing an agent retrieving information from wherever it is stored Exercise 5 1 Produce a Casper script to model the Yahalom BAN proto col 1 a b na 2 0 gt 5 nb a Nna Server Key 6 9 nb 16 kab T ServerKey a La kab nb ServerKey b 4 La
29. PK IdProvider gt PublicKey SK IdProvider gt SecretKey InverseKeys PK SK Protocol description 0 gt u sp idp Request for a resource I am u I want to access sp 1 u gt idp u sp lt AuthnResponse gt idp gt u a idp sp u u gt sp a sp idp u sp gt idp a u sp idp idp gt sp sp idp nidp SK idp sp gt u m WN 36 6 SECURE CHANNELS Processes USER u knows PK SERVICEPROVIDER sp m knows PK IDPROVIDER idp a nidp knows PK SK idp Channels NF NRA NR NF NRA NR NR NF NRA NR NF NRA NR NF NRA NR O OC QO O Specification Secret sp m u Secret u m sp Agreement sp idp lu al Agreement idp sp a nidpl Agreement sp u m idp Agreement u sp 160 Agreement idp u sp Agreement u idp sp Actual variables Alice Mallory User Dustin Mallory ServiceProvider Sam IdProvider M M Mm Message A A Am Artifact Nidp Nidp Nm Nonce Functions symbolic PK SK System USER Alice USER Alice SERVICEPROVIDER Dustin M SERVICEPROVIDER Dustin M IDPROVIDER Sam A Nidp IDPROVIDER Sam A Nidp Intruder Information Intruder Mallory 6 2 Nevv style secure channels 37 IntruderKnowledge Alice Dustin Mallory Sam Am Nm Mm PK Some secure transport protocols link messages togeth
30. a then temporal formula 211 fact Casper doesn t parse such expressions itself but simply copies them directly into the output file for FDR to subsequently parse 76 C THE CASPER SYNTAX temporal formula temporal formula and temporal formula temporal formula or temporal formula C temporal formula previously temporal formula temporal event temporal event identifier sends receives message line no from to identifier 53 containing substitution 17 substitution identifier identifier for identifier substitution C 7 Algebraic equivalences section equivalences section Equivalences 1 equiv dec equiv dec x forall quants msg msg quants x quant quant quant identifier identifier type name C 8 Actual variables section act var section Actual variables 21 act dec act dec act var dec timestamp def maxruntime def act inv keys dec act var dec identifier identifier type name di tagl subtype expr subtype expr PI identifier identifier di tag External InternalKnown InternalUnknown timestamp def x TimeStamp time time maxruntime def MaxRunTime time lt act inv keys dec act inv key pair act inv key pai
31. ace above the following is printed 14 3 USING CASPER Alice believes Na is a secret shared vith Mallory Bob believes Nb is a secret shared vith Alice The intruder knovs Nb This is the same error as described above The CSP definition of the system hides most of the details at the top level However moving down two levels in the debug tree to the process SYSTEM gives the following trace env Alice Env0 Mallory lt gt intercept Alice Mallory Msg1 Encrypt PK_ Mallory lt Na Alice gt lt gt fake Alice Bob Msg1 Encrypt PK_ Bob lt Na Alice gt lt gt intercept Bob Alice Msg2 Encrypt PK_ Alice lt Na Nb gt lt gt fake Mallory Alice Msg2 Encrypt PK_ Alice lt Na Nb gt lt gt intercept Alice Mallory Msg3 Encrypt PK_ Mallory lt Nb gt lt Na gt fake Alice Bob Msg3 Encrypt PK_ Bob lt Nb gt lt Na gt leak Nb We can use interpret to interpret this trace 0 gt Alice Mallory 1 Alice gt I Mallory Na Alice PK_ Mallory 1 I_Alice gt Bob Na Alice PK_ Bob 2 Bob gt I Alice Na Nb PK_ Alice 2 I Mallory gt Alice Na Nb PK_ Alice 3 Alice gt I Mallory Nb PK_ Mallory 3 I Alice gt Bob Nb PK_ Bob The intruder knows Nb Again this is the same attack as described above The other assertions can be checked and any attacks interpreted in the same way The Casper package also includes a function linterpret that pro
32. ages of the protocol We describe each simplification in turn RemoveFields This simplification takes a list of types and remove all fields of those types from the protocol description For example the simplifi cation RemoveFields Nonce TimeStamp will remove every instance of a nonce or timestamp RemoveHashedFields This simplification removes some hashed messages from the protocol description For example RemoveHashedFields f Nonce Agent will remove all messages of the form f N A for N Nonce A Agent RemoveEncryption This simplification strips off encryptions leaving just the body of a message For example RemoveEncryption Nonce Agent PublicKey will simplify any message of the form N A x for N Nonce A Agent K PublicKey replacing it by N A RemoveHash This simplification strips off applications of hash functions leaving just the body The example RemoveHash f Nonce Nonce TimeStamp will simplify any message of the form f N1 N2 for N1 N2 Nonce T Timestamp replacing it by N1 N2 T Coalesce This simplification takes a pair of types as an argument and co alesces pairs of adjacent atoms of those types replacing them by just the first element For example Coalesce Nonce Nonce will coa lesce adjacent pairs of nonces replacing them by the first element of the pair This simplification should only be used if the results of HL99 are to be applied if the field removed is eit
33. ain the expected values for example in message 2 above A will accept any value for nb but will only accept the value for na that matches the value in his current knowledge that is the same value that A sent in message 1 and will only accept a message that is encrypted with PK A his public key 2 2 4 Specifications The requirements of the protocol are specified under the Specification heading as below Specification Secret A na B Secret B nb A Agreement A B na nb Agreement B A na nb The lines starting Secret specify that certain data items should be secret The first secret specification above may be paraphrased as A thinks that na is a secret that can be known to only himself and B Of course if B happens to be the intruder then there is nothing to prevent him passing the secret on to others However this line will cause a CSP specification to be generated with the meaning if A runs the protocol ap parently with B and B is not the intruder then the intruder will never learn the value of na The lines starting Agreement are authentication specifications The first specifies that A is correctly authenticated to B and the two agents agree on the data values na and nb More formally it specifies 8 2 AN EXAMPLE INPUT FILE If responder B completes a protocol run apparently with A using the data values na and nb then the same agent A has previously been running the protocol ap pare
34. as run ning the protocol with someone other than B The specification TimedAgreement A B t vi Vn isa timed version of Agreement A B vi Vn where in addition A s run was within the previous time units of B completing his run by con trast the Agreement specification macro places no constraints on the amount of time between the runs Similarly TimedNonInjectiveAgreement A B t v1 Vn TimedWeakAgreement A B t and TimedAliveness A B t are timed versions of NonInjectiveAgreement A B vi vnl WeakAgreement A B and Aliveness A B The different authentication specifications are discussed in more detail in Low97 5 5 Splitting large messages If a protocol involves a particularly large message then the resulting message space that FDR has to produce will be extremely large In these circum stances it is a good idea to split such large messages For example consider the Yahalom protocol which could be written using the Casper notation as Protocol description gt A B A gt B na B gt S nb na SKey B S gt A nb B kab na SKey A A kab nb SKey B 7 enc A gt B enc A kab nb SKey B nb kab Hs UNEO If we consider a small system with 3 agents 3 shared keys 3 nonces and 2 session keys then message 3 can take 8910 32 2 32 2 1 different forms It is better to write the protocol as Protocol description 0 gt
35. as to describe the following protocol 1 4 gt A 3 na 2 A B A na nb B Pk A 3 A B nb prey 10 3 USING CASPER Exercise 2 2 n some protocols nonces are considered to be predictable that is an intruder may be able to predict which nonces other agents are about to use How may we model predictable nonces within Casper de Exercise 2 3 In the above description of the Needham Schroeder Public Key Protocol B s public key PK B was not included in the parameters of the process INITIATOR under the Processes heading instead A was assumed to know the function PK and calculated PK B to send message 1 What would be the effect of including pkb as a parameter of INITIATOR under the Processes heading and then instantiating this with PKb PK Bob under the System heading de Answers to the exercises appear in Appendix B 3 Using Casper There are two ways of using Casper making use of the graphical front end CasperFDR to interface with FDR or as a stand alone Haskell script 3 1 Using CasperFDR CasperFDR is started by executing the shell script CasperFDR A filename without the sp1 suffix may be provided on the command line if a filename is not provided then a file selection window will appear CasperFDR takes a few seconds to initialise The main CasperFDR window has three buttons The compile button compiles the script into CSP producing input similar to the follow
36. at they personally share with the server i e SKey A and SKey B respectively The exchange of messages can then be defined by Protocol description 0 gt A B 1 A gt S AB ts kab SKey A ts now or ts 1 now 2 S gt B A ts kab SKey B ts now or ts 1 now The lines within square brackets represent tests that are performed by the agent who receives the message on the previous line if the test fails the agent aborts the run Within tests the distinguished variable now represents the current time When S receives message 1 he checks that the timestamp is recent either the current time or the previous time if the test fails then S refuses to accept this message and aborts the run B makes a similar check when he receives message 2 When an agent sends a timestamped message as with messages 1 and 2 above the value of the timestamp will be set to the current time We consider now the specification for the protocol It would seem that if a responder B completes a run of the protocol apparently with A then A should have been running the protocol within the previous two time units the tests performed on the timestamps allow for a delay of one time unit per message this assumes that there is negligible delay between S checking mes sage 1 and sending message 2 we formalize this assumption below Further the two agents should agree on the value of kab Our specification is a timed version of the A
37. ation both agents should become sure as to the identity of the other agent The protocol begins with A selecting a nonce na and sending it along with its identity to B message 1 encrypted using B s public key When B receives this message it decrypts the message to obtain the nonce na It then returns the nonce na along with a new nonce nb to A encrypted with A s key message 2 When A receives this message he should be assured that he is talking to B since only B should be able to decrypt message 1 to obtain na A then returns the nonce nb to B encrypted with B s key When B receives this message it would seem that he should be assured that he is talking to A since only A should be able to decrypt message 2 to obtain nb We consider a protocol description in standard notation to be a tem plate parameterized by the free variables appearing within it these variables are instantiated with actual values in runs normally different values in dif ferent runs We adopt the following conventions in this paper free variables representing agents identities will be represented by a single capital letter while free variables representing other data items will be represented by small letters when we instantiate these free variables with actual values we will 2 1 Overview of input file represent agents identities by proper names while other data items will have names beginning with a capital letter In defining the Casp
38. ators and responders similarly FDR can only deal with systems where the underlying atomic datatypes for example the types of nonces or keys are themselves finite It is my experience that most attacks upon protocols can be found by considering a fairly small system The question of proving the security of an arbitrarily sized system from the security of a particular system is the topic of current research see Lovv96 Low98 for approaches to this problem Because of the above observations the Casper input file must define not only the operation of the protocol but also the system to be checked There fore the input file contains two distinct parts e A definition of the way in which the protocol operates describing the messages passed between the agents the tests performed by the agents the types of the data items used the initial knowledge of the agents a specification of what the protocol is supposed to achieve and a defini tion of any algebraic equivalences over the types used 4 2 AN EXAMPLE INPUT FILE e A definition of the actual system to be checked defining the agents taking part in the actual system and the roles they play the actual datatypes to be used and the intruder s abilities The first part can be thought of as a function that returns a model of a system running the protocol the second part can then be thought of as defining a particular image of that function by instantiating the parameters of the
39. b a na Actual variables Alice Bob Mallory Agent Nal Nbi Nm Nonce K1 Km SessionKey PK1 PKm PubKey SK1 SKm SecKey InverseKeys PK1 SK1 PKm SKm K1 K1 Km Km Functions symbolic passwd System INITIATOR Alice PK1 SK1 Nal RESPONDER Bob Nb1 K1 71 72 C THE CASPER SYNTAX Intruder Information Intruder Mallory IntruderKnowledge Alice Bob Mallory Nm PKm SKm passwd Mallory Alice passwd Mallory Bob passwd Alice Mallory passwd Bob Mallory Guessable Password This produces no attacks If the protocol is adapted so that pk and sk are replaced by a single symmetric key then FDR discovers an attack where the intruder observes a run between A and B up to message 4 guesses the value passwd A B and then verifies the guess using verifier Na Exploring the debug tree one can find out that the intruder decrypts the second message with passwd A B to obtain K px decrypts the first message with passwd A B to obtain PK decrypts K px with PK to obtain K this step is not possible if PK is an asymmetric key decrypts the third message to obtain Na and decrypts the fourth message to obtain Na again the fact that he obtains the same value Na from both these decryptions verifies the guess It is also possible to verify the guess by decrypting the fourth and fifth messages to obtain Nb in two different ways C The Casper syntax In this section we pr
40. blic Key protocol containing some temporal logic specifications Needham Schroeder Public Key Protocol 3 message version Free variables 50 8 SPECIFYING PROPERTIES USING TEMPORAL LOGIC a b Agent na nb Nonce PK Agent gt PublicKey SK Agent gt SecretKey InverseKeys PK SK Processes INITIATOR a na knows PK SK a RESPONDER b nb knows PK SK b Protocol description 0 gt a db 1 a b fna a PK b 2 b gt a nb PK a 3 a b nb PK b Specification PASS if B receives message 3 from A containing Nb for nb then previously A receives message 2 containing Nb for nb and previously A sends message 3 containing Nb for nb PASS if A receives message 2 from B containing Na for na Nb for nb then previously B sends message 2 to A containing Na for na Nb for nb A for a and previously A receives message 0 containing B for b Actual variables A B I Agent Na Nb Nm Nonce Functions symbolic PK SK System l INITIATOR A Na RESPONDER B Nb Intruder Information Intruder I IntruderKnowledge A B I Nm PK SK I Temporal logic specifications may be used either with the normal models or in conjunction with the data independent models Note that when using it with the data independent models the normal threshold theorems do not apply and therefore the GenerateSystem flag may not be used The external agent should be pic
41. ced in the repeat section Therefore as the internal agents simulate an unbounded number of runs this simulates an unbounded number of repeat sessions 7 5 Minimising state space explosion When applying these techniques one runs into problems with the size of the state space of the protocol model We describe now several techniques for managing this state space explosion within data independence scripts Authentication specifications that test for agreement on many variables can be very slow and demanding on memory to test To speed up the checks a specification such as Agreement a b vs can be split up into two different specifications Agreement a b vs1 and Agreement a b vs2 where vs vsit vs2 Also the use of notation should be avoided as much as possible as the use of it dramatically increases the amount of memory that is required Testing protocols that contain timed specifications such as TimedAgreement a b t vs can be very slow especially if t is greater than 2 It is recommended that this specification is instead split up into two different checks Agreement a b vs and TimedAgreement a b t 11 The Agreement specification can then be split up further as mentioned above Close inspection of the threshold theorems should show that as the num ber of authentication specifications in a single file rises so to does the number of values that are required to show the protocol is secure Since increasing the number of values in the
42. col OpenID authentication protocol Free variables u User rp RelyingParty op OpenID m Message nk Nonce k HashKey h HashFunction k1 NullKey PK OpenID gt NullKey SK OpenID gt NullKey 38 InverseKeys PK SK Protocol description 0 gt u rp 1 u gt op rp 2 op gt u rp nk h k u 7 hash 3 u gt op nk hash h k u hashrp 4 10 gt 1 u 5 u gt op 6 rp gt op u nk hashrp h k u 7 op rp u 8 rp ou m Processes USER u op RELYINGPARTY m OPENID op nk k Channels Session symmetric 1 2 Session symmetric 3 8 Session symmetric 6 7 Session 4 5 C NF NRA NR C NF NRA NR C NR C NR NF NRA NF NRA 0 1 e Specification Agreement u Agreement rp u m op nk Agreement u op rp nk Agreement op u rp nk Agreement op lu nk Agreement rp op lu nk op Actual variables Alice Mallory User Richard Mallory RelyingParty 6 SECURE CHANNELS 39 Olive Mallory OpenID M1 M2 Mm Message NK1 NK2 Nm Nonce K1 K2 Km HashKey Functions symbolic PK SK System USER Alice Olive USER Alice Olive RELYINGPARTY Richard M1 RELYINGPARTY Richard M2 OPENID Olive NK1 K1 OPENID Olive NK2 K2 Intruder Information Intruder Mallory IntruderKnowledge Alice Richard Olive Mallory Nm Mm Km The
43. ded for Alice as in the first message 2 This attack can be re written as follows labelling the two runs a and 6 writing for example 3 2 for message 2 of run 5 a l Alice Mallory 1Na Alice pk Mallory 0 1 Tan Bob Na Alice pK Bob B 2 Bob I ntice Na Nb px Alice a 2 Mallory Alice Na Nb pk Alice a 3 Alice Mallory Nb px aallory LAuce gt Bob Nb PK Bos This is the attack from Low95 The second assertion checked concerns authentication of the initiator to the responder This also fails Bob believes that he has successfully com pleted a run of the protocol with Alice using nonces Na and Nb but Alice does not believe that she has been running the protocol with Bob The attack is essentially the same as the previous Checking the final assertion concerning authentication of the responder to the initiator fails to find an attack The file menu in the CasperFDR window allows the user to select a new file open an FDR status window to see output from FDR during checking or quit 12 3 USING CASPER Starting FDR Checking auto users gavinl Security Casper Manual NS3 csp Checking assertion SECRET_SPEC T SYSTEM_S Attack found Top level trace Alice believes Na is a secret shared with Mallory Bob believes Nb is a secret shared with Alice The intruder knows Nb System level 0 gt Alice Mallory 1 Alice gt I Mallory Na Alice PK Mallory l 1 I
44. described by Anderson and Needham in AN95 4 6 Timestamp Details Timestamps are implemented internally within Casper using the concept of agestamps where each timestamp actually specifies how long ago it was cre ated This allows for a more accurate simulation of an infinite time domain than using absolute timestamps would allow To implement this it was as sumed that no time elapses between an agent receiving a message and sending a response This means that time can only pass whilst the message is being held by the intruder In order to test protocols that use timestamps correctly the following rules of thumb should be obeyed The maximum run time should be set to one and all checks of the form ts now should allow a timestamp to either be now or now 1 The time domain should then be chosen to be one greater than this so typically the time bound should be specified as MinTime 0 MazTime 2 21 Since agestamps are used rather than timestamps Casper vvill report timestamps with negative values in counterexample traces This indicates how old the message is so an agestamp of value indicates that one time unit has passed since the timestamp was created 5 Carrying on In this section we explain how to handle a few features that often crop up in protocols 5 1 The notation It will often be the case that the sender and receiver of a message treat that message differently For example in many protocols an agent rec
45. description 0 gt 1 A gt 2 B gt A B B na A PK B A na nb PK A A 2 An input script using data independence techniques 57 3 A o B nb PK B Specification Secret A na B Secret 5 nb A Agreement A B lna nbl Agreement B A na nb Actual variables Alice Bob Mallory Agent Na Nb Nm Nonce Functions symbolic PK SK System INITIATOR Alice Na RESPONDER Bob Nb Intruder Information Intruder Mallory IntruderKnowledge Alice Bob Mallory Nm PK SK Mallory A 2 An input script using data independence tech niques Simplified version of Yahalom Free variables a b Agent s Server na Nonce NonceNA nb Nonce NonceNB kab SessionKey ServerKey Agent gt ServerKeys InverseKeys kab kab ServerKey ServerKey Processes INITIATOR a na knows ServerKey a generates na RESPONDER b s nb knows ServerKey b generates nb SERVER s kab knows ServerKey generates kab Protocol description 0 ma b 58 A EXAMPLE INPUT SCRIPTS 1 a gt b na 2 b gt s fa na nb ServerKey b Sa s gt a ib kab na nb ServerKey a l 30 s gt b kab ServerKey b 4 a b nb kab Specification Secret b kab a s Agreement a b na nb Agreement a b kab Actual variables Alice Bob Mallory Agent Sam Server Kabp SessionKey InternalKnown Kabs1 Kabs2 SessionKey InternalUnknown
46. duces an interpretation of the attack as ETPX source suitable for use with the package protdesc sty which is included in the distribution Exercise 3 1 Run CasperFDR on your answer to Exercise 1 of Section 2 You should detect an attack try to understand it Alternatively run Casper on the script run FDR on the output file produced and use the debugger and the interpret function to understand the attack d 15 4 Case study The VVide mouthed frog Pro tocol In this section we describe how to deal with some more protocol features and illustrate some of the issues involved in modelling protocols by considering the example of the Wide mouthed frog Protocol of BAN89 The protocol can be described as follows 1 1 gt 1151 B kab skey A 2 8 B 11s2 A kab skey B Here the server shares keys SKey A and SKey B with A and B respec tively the protocol aims to establish a session key kab and to authenticate A to B A invents a session key and sends it to S along with a timestamp 151 S then forwards the key to B along with a new timestamp 152 As explained in Section 2 FDR cannot be used to consider the most general system running the protocol Instead we have to consider particular systems We will consider four different systems running the protocol FDR finds that there is no attack upon the first system but finds three different attacks on the other systems Part of the skill in using Casper is to know what
47. e This creates an output file in filename csp For example running the compiler on the example of the 3 message Needham Schroeder Public Key Protocol gives the following output compile NS3 Parsing Type checking Compiling Writing output Output written to NS3 csp Alternatively the function vcompile may be used in the same way vcompile additionally writes a copy of the CSP code on the screen 3 3 Running the output file with FDR The output file can be loaded into FDR in the normal way This produces the same three assertions as described in Section 3 1 Each can be checked using FDR If FDR finds an attack then the FDR debugger can be used to find the corresponding CSP trace In the running example testing the first assertion concerning secrecy finds that the refinement fails The debugger shows that the right hand side will perform the following trace with taus not shown signal Claim_Secret Alice Na Mallory signal Claim_Secret Bob Nb Alice leak Nb The Casper package includes a function interpret which can be used to interpret the output from FDR This function is used by typing interpret at the Casper prompt followed by return pasting in the trace from the FDR debugger and then typing a blank line this might require you to hit return twice once to end the last line from the debugger and once for the blank line A description of the attack will then appear on the screen For the tr
48. ec identifier identifier type expr subtype expr P identifier identifier 4 type name type name x type name type name T4 C THE CASPER SYNTAX inv keys dec InverseKeys inv key pair inv key pair 1 inv key pair x C identifier identifier Each inv key pair should be either a pair of variable names or a pair of function names C 4 Processes section Processes 1 process def processes section process def process name C identifier identifier knows statement generates statement 2 2 knows statement knows atom atom generates statement generates identifier identifier The first parameter of each process should represent agent identities used in the protocol description C 5 Protocol description section prot desc section x Protocol description I prot msg env msg send env msg rec prot msg assignment line line no identifier gt identifier msg test line assignment line x assignment assignment gt asssignment identifier fdr expression test line 2 4 test 1 test x fdr expression env msg rec x line no gt identifier msg test line 1 env msg send assignment line line no identifier gt msg line no x letter digit let
49. eives an encrypted message that it does not decrypt but instead simply forwards it to a third party This is the case in the standard Yahalom protocol 1 a b na 2 b s na nb A des 10 kab na ta kab serverKey b 4 La kab serverKey b nb kab a does not decrypt the second component of message 3 but simply forwards it to b in message 4 Casper expects agents receiving messages to be able to decrypt them this helps to trap many user errors hence we need some way of indicating to Casper that certain messages really aren t intended to be decrypted this is the role of the notation We write m v where m is a message and v is a variable to denote that the recipient of the message should not attempt to decrypt the message m but instead store it in the variable v Similarly we write v m to indicate that the sender should send the message stored in the variable v but the recipient should expect a message of the form given by m For example we would model the standard Yahalom protocol using a script with a Protocol description section as follows Protocol description 0 ma b 1 a gt b na 2 b gt s a na nb ServerKey b 3 s gt a b kab na nb ServerKey a la kab ServerKey b 7 v 4 a gt bi v kab ServerKey b nb kab 22 CARRYING ON a stores the second component of message 3 in the variable v and forwards it to b in message 4 In an
50. els in the system are given these properties See BL03 for more details of these properties Under this style is is also possible to use the following designator direct messsages may be sent directly between hoenst agents rather than having to pass via the intruder this gives shorter clearer counter example traces in some cases but leads to a larger state space 6 2 New style secure channels The more recent style of designating secure channels allows each message to be designated as being over a secure channel that provides one or more of the following services Confidentiality C The contents of the message are kept confidential from the intruder No faking NF The intruder cannot fake messages on this channel No redirecting NR The intruder cannot redirect a message so that it is received by an agent other than that for whom it was originally intended No honest redirecting VR The intruder cannot redirect messages except when the message was originally intended for him No reascribing NRA The intruder cannot reascribe a message so that it appears to come from an agent other than the original sender No honest reascribing NRA The intruder cannot reascribe a mes sage other than so that it appears to come from himself See Dil08 DLOS for further description of these properties For each message in the protocol the user should list the properties of the channel that the message is carried on F
51. er input format we have had to make various design decisions Our philosophy has been to try to make the syntax as close as pos sible to the standard way of describing protocols with as few special cases as possible We have tried to define a set of default actions made precise below that are as close as possible to what would be expected by some body familiar with security protocols for example when an agent receives a message containing a variable that he has seen in an earlier message he should check that the value he receives matches the value he saw earlier the protocol tester should not have to make this test explicit On the other hand we have not tried to cover cases where the actions to be taken by the agents are not obvious to do so would be to run the risk of having the agents perform actions different from those expected by the protocol tester In such cases the actions should be made explicit failure to do so should cause Casper to raise an error message 2 1 Overview of input file FDR operates by explicitly enumerating and then exploring the state space of the system in question Hence it can only deal with finite state systems typically up to a few million states and so this method can only be used to check a particular typically fairly small system running the protocol for example with a single initiator and a single responder rather than being able to check an arbitrary system with an arbitrary number of initi
52. er into sessions so that the intruder cannot combine messages sent in different sessions so that they are received in the same session In some cases the relationship be tween sessions is injective each session of one agent corresponds to a single session of another Further some secure transport protocols provide sym metric sessions if messages sent by A in session are received by B in session sg then messages sent by B in session sg are receives by A in ses sion s Finally some secure transport protocols ensure that messages are received in the same order in which they are sent for example by including an authenticated message number we call this the stream property Again see Dil08 DL08 for more details In order to use the session and stream properties the user should use the keywords Session and Stream optionally followed by one of the key words injective or symmetric followed by a list of the message numbers that should be joined into a single session When two agents communicate on session channels even on non symmetric session channels it is not nec essary to create different sessions for each agent the list of all messages sent by both agents should be included in the session For example the following session description specifies that messages 1 2 and 3 are sent in a single injective session channel Session injective 1 2 3 The script below illustrates the use of session channels within the OpenID proto
53. esent the formal syntax for Casper scripts We use EBNF writing literals in teletype font within quotes terms within curly brackets may be repeated zero or more times terms within square brackets are op tional linebreaks are significant within Casper scripts and are represented by 1 Logical lines may be split across two or more lines by ending lines with A or by indenting the following line Lines beginning with are comments C 1 Basic definitions identifier letter letter digit atom identifier fn app fn app identifier C identifier identifier O C 2 Syntax summary 73 msg x identifier identifier C msg Y 2 msg msg msg H atom Y msg msg msg identifier identifier msg C msg y type name identifier process name identifier The bit wise exclusive or operator binds tighter than the operator which binds tighter than the sequencing operator 6022 There are two distinguised type names in Casper TimeStamp and HashFunction C 2 Syntax summary script free vars section processes section prot desc section spec section equivalences section act var section functions section system section intruder section channels C 3 Free variables free vars section var dec subtype expr x type expr section section Free variables var dec inv keys d
54. greement specification of Section 2 Specification TimedAgreement A B 2 kab 4 2 First system 17 The above specification can be paraphrased as If responder B completes a protocol run apparently with A then the same agent A has been running the protocol with B within the last 2 time units and both agents agreed as to which roles they took and upon the value of kab and further each such run of A corresponds to a unique run of B 4 2 First system It is normally a good idea to start off by checking a small system because more often than not this will uncover any attacks We therefore consider a system with a single initiator Alice and a single responder Bob each of whom can run the protocol once System INITIATOR Alice Sam Kab RESPONDER Bob SERVER Sam The actual variables in the system are defined by Actual variables Alice Bob Mallory Agent Sam Server Kas Kbs Kms ServerKey Kab SessionKey The time domain to be considered is also defined under the Actual variables heading it should be defined to be a contiguous subsequence of the integers as below In this case we choose a very small one point time domain so as to make checking as fast as possible It is also necessary to make an implementation assumption about how long any particular run should last this is defined by the variable MaxRunTime if any run lasts for longer than this time then the agent involved should timeout and
55. hared Key Protocol 1 S A B na 2 na B kab skeyta 3 kab A skeytB 4 BoA nb Kab 5 ASB nb nD kab Specify that session key such as kab are crackable You should find an attack upon this protocol amp In protocols using timestamps it is convenient to specify that keys are compromised after a particular period of time This can be done using a line such as Crackable SessionKey 3 which specifies that the key is compromised after 3 time units Exercise 5 8 Adapt the TMN Protocol script from Section 4 5 to specify that session keys can be compromised after three time units You should find an attack upon the protocol d 5 12 Passvvord guessing attacks Some protocols make use of poorly chosen secrets such as passwords which might be guessed by an intruder who is then able to verify that guess For example such a verification might be by the intruder using the guessed value to decrypt a message to find a value that he has already seen See Low02 for a description of other ways in which such guesses can be verified Values of certain types can be specified to be guessable by including a line like the following in the Intruder Information section Guessable Password When dealing with guessable types Casper produces an extra refinement assertion to find whether the intruder can guess a value and then verify his guess In most protocols such a correct guess will also lead
56. her in the intruder s initial knowledge or equal to the value removed it is up to the user to check this condition SwapPairs This simplification takes a pair of types as an argument and swaps pairs of adjacent atoms of those types For example SwapPairs Nonce Agent swaps adjacent pairs of nonces and atoms RemovePlainAndEnc This simplification will simplify signed messages of the form m m x for k a signature key replacing them by just m It is up to the user to ensure that all messages of this form are encrypted with signature keys 53 A full sample input file can be found in Appendix A 3 When Casper has been loaded the command simplify filename will apply the simplifications defined in the file filename spl and print the new protocol description on the screen 10 Conclusion The Casper compiler has revolutionized our approach to analyzing protocols Previously when we produced the CSP by hand it would take about a day to code up a protocol now it takes only a few minutes In particular making small changes to the protocol or the system to be checked typically requires changes to only a couple of lines of the input file when editing the CSP code by hand the changes necessary were spread throughout the file and it was hard to know whether you had remembered them all Also it was easy to make mistakes when producing the CSP by hand and these mistakes were hard to spot When using Casper errors are less commo
57. icated Removing the specification Secret B kb A S from the Casper script will lead to the following attack being discovered 0 Alice Bob 1 Alice gt Sam Bob Ka px 2 Sam Igo Alice 3 Igo Sam Alice Km ks 4 Sam Alice Km 0 Ka Alice believes Ka is a secret shared with Bob Sam The intruder knows Ka which exploits the fact that message 3 is not authenticated These attacks can be prevented by replacing the public key encryptions in messages 1 and 3 by encryptions using keys shared between the sender and the server However there are still attacks upon the resulting protocol We leave it up to the reader to investigate and then prevent these attacks Answer to Exercise 4 To ensure that the key server accepts only genuine agents identities we will define a function realAgent which tests whether its argument really does represent an agent s identity the server should apply this test to the identities it receives in messages 1 and 4 We also want to restrict ourselves to searching for attacks where the user requests a connection with a genuine agent rather than a random number that B happens to then choose as his nonce so this test is applied to the value received in message 0 note that this should be thought of more as a restriction on the environment than a test that A should actually perform The protocol and system definition is then straightforward Needham Schroeder Public Key Pro
58. ication being tested We first consider secrecy specifications such as Secret b v as for which the following are required One external instance of b e Two agent identities one honest and one dishonest Two actual variables S and P that are InternalUnknown and InternalKnown respectively S should be of the type and subtype of v P should be of every type and subtype that is not the type or subtype of v e Sufficient External values such that external agents do not generate the same values for data independent variables 42 7 USING DATA INDEPENDENCE TECHNIQUES We illustrate the minimum number of required variables by considering the simplified Yahalom protocol as presented below 1 a b na 2 b a na nd serverKey b Jara b kab na nb serverKey a 30 5 0 10 kab serverKey b 4 nb kab Below is the the system setup and minimum number of variables as dictated by the above thresholds for the specification Secret b kab a s Free variables a b Agent s Server na Nonce NonceNA nb Nonce NonceNB kab SessionKey ServerKey Agent gt ServerKeys InverseKeys kab kab ServerKey ServerKey Processes INITIATOR a na knows ServerKey a generates na RESPONDER b s nb knows ServerKey b generates nb SERVER s kab knows ServerKey generates kab Actual variables Alice Mallory Agent Alice Server vSecret SessionKey InternalUnknown vPublic SessionKey
59. ing Casper version 1 5 Parsing Type checking Consistency checking Compiling Writing output Output written to NS3 csp Done Compiling creates refinement assertions corresponding to the specifica tions from the input file For example three refinement assertions are created for the file from Section 2 3 1 Using CasperFDR 11 SECRET_SPEC T SYSTEM_S AuthenticateINITIATORToRESPONDERAgreement_na_nb T SYSTEM_1 AuthenticateRESPONDERToINITIATORAgreement_na_nb T SYSTEM_2 The first assertion corresponds to the secrecy specifications the second as sertion corresponds to the specification concerning authentication of the ini tiator to the responder the third assertion corresponds to the specification concerning authentication of the responder to the initiator The check button invokes FDR to check all the assertions The output for the example file is given in Figure 2 The first check concerning secrecy fails Two descriptions of the attack appear on the screen The former description describes the attack at a high level talking about the beliefs and knowledge of the agents in this case the error is that Mallory learns Nb which Bob thought should have been kept secret The latter description describes the individual messages that are sent during the attack The notation I_Alice represents the intruder taking Alice s identity either to fake a message as in the second message 1 or to intercept a message inten
60. ion in the Free variables section Then f m represents the application of f to message m In such cases both the sender and the recipient should be able to create f m the recipient will only accept a value for this message if the value received matches the value he calculates for himself It is assumed that all hash functions are known to all agents 5 4 Protocol specifications 25 5 4 Protocol specifications Casper supports a number of different forms of specification for protocols as follows Secret A s B B specifies that in any completed run A can expect the value of the variable s to be a secret B Bn are the variables representing the roles with whom the secret is shared More precisely this specification fails if A can complete a run where none of the roles B By is legitimately taken by the intruder but the intruder learns the value A gives to s StrongSecret A s B B is similar to Secret A s B4 Bn except it also includes incomplete runs Thus this specifi cation fails if A can take part in a run complete or not where none of the roles B Bn is taken by the intruder but the intruder learns the value A gives to s It is arguable whether one should consider a failure of secrecy on an incomplete run to be an attack because A will probably not do anything with the value of s if the run is incomplete however we should probably be aware of such behaviours Our main
61. ionKey B 3 Answers to exercises from Section 5 69 Checking the resulting secrecy specification reveals the following attack 1 ane gt Stan Alice Bob Ni 2 Stan gt tice Ni Bob Kab skey Alice 3 Stan IBob Kab Alice skey Bob Stan withdraws from this run as SERVER Kab has been compromised 8 I stan Bob Kab Alice skey Bob 4 Bob I Alice Nb kab 5 Tatice gt Bob Nb Nb kab The intruder knows Kab Answer to Exercise 8 The script should look something like the follow ing Wide Mouthed Frog Protocol with key compromise Free variables A B Agent S Server kab SessionKey ts ts TimeStamp SKey Agent gt ServerKey InverseKeys SKey SKey kab kab Processes INITIATOR A S kab knows SKey A RESPONDER B knows SKey B SERVER S knows SKey Protocol description 0 gt A 8 1 A gt S AB ts kab SKey A 1 ts now or ts 1 n0w and A B 2 S gt B A ts kab SKey B ts now or ts 1 now and A B Specification TimedAgreement A B 2 kab Secret A kab B Secret B kab Actual variables T B ANSWERS TO THE EXERCISES Alice Bob Mallory Agent Sam Server Kab SessionKey TimeStamp 0 3 MaxRunTime 0 InverseKeys Kab Kab Functions symbolic SKey S5ystem INITIATOR Alice Sam Kab RESPONDER Bob SERVER Sam SERVER Sam SERVER Sam WithdrawOption True
62. is desirable to model the situation where agents can abort a run part way through and then start a new run where the agent is defined by a sequential composition within the System section This is done by putting the line WithdrawOption True within the System section The default is Nithdrav ption False i e that agents do not abort runs part way through 28 5 CARRYING ON 5 7 Delaying decryption Consider the following simplified version of the SPLICE protocol of YOM90 1 4 9 B ni 2 8 A 19 A n1 PK B lskts 8 4A B 14 1 2 pk B SK A 4 B 8 A n3 6 4 B n2 pKa In messages 1 and 2 A obtains B s public key from the key server S In message 3 A sends a message to B signed with his secret key B then obtains A s public key in messages 4 and 5 and so can check message 3 Finally B returns a message to A The important point to note here is that B cannot immediately decrypt message 3 he does not obtain A s public key until message 5 We model this within Casper by having B store the value of message 3 in a variable enc using the notation B decrypting this message and performing the ap propriate checks only after receiving message 5 0 gt 1 8 1 A S B nil 2 S gt A S A n1 PK B 7 pkb SSK S 3 A gt B A ts n2 pkb PK B SK A 2 v 4 B gt 5 A n3 5 6 gt B 48 B n3 PK A pka SSK S pbable v pka and nth decrypt v pka
63. ity protocols with model checkers by data independence techniques Journal of Computer Security 7 2 3 147 190 1999 56 Ros94 Ros95 Ros98 TMN90 YOM90 A EXAMPLE INPUT SCRIPTS A W Roscoe Model checking CSP In A Classical Mind Essays in Honour of C A R Hoare Prentice Hall 1994 A W Roscoe Modelling and verifying key exchange protocols using CSP and FDR In 8th IEEE Computer Security Foundations Workshop 1995 A W Roscoe Proving security protocols with model checkers by data independence techniques In Proceedings of 11th IEEE Computer Security Foundations Workshop pages 84 95 1998 Makoto Tatebayashi Natsume Matsuzaki and David B Newman Jr Key distribution protocol for digital mobile communication systems In Advances in Cryptology Proceedings of Crypto 789 volume 435 of Lecture Notes in Computer Science pages 324 333 Springer Verlag 1990 S Yamaguchi K Okayama and H Miyahara Design and im plementation of an authentication system in WIDE Internet en vironment In Proc 10th IEEE Region Conf on Computer and Communication Systems 1990 A Example input scripts A 1 A standard input script Needham Schroeder Public Key Protocol 3 message version Free variables A B Agent na nb Nonce PK Agent gt PublicKey SK Agent gt SecretKey InverseKeys PK SK Processes INITIATOR A na knows PK SK A RESPONDER B nb knows PK SK B Protocol
64. ked to be the agent who sends or receives the event on the left hand side of the if that is not contained within any previously statement 9 Simplifying transformations Casper has been extended to implement the simplifying transformations de scribed in HL99 These transformations can be used to simplify a protocol to make it easier to analyze They have the property that if there is an at tack upon the original protocol then there is also an attack on the simplified version We will assume some familiarity with the material in HL99 in this section The simplifying transformation extension to Casper can be used to define a sequence of simplifications which are then applied automatically to the pro tocol The input script contains the first four sections of a standard Casper script together with an additional section Simplifications containing a list of the simplifications to be performed An example Simplifications section is below which illustrates the seven types of simplifying transforma tion currently supported HSimplifications RemoveFields Nonce TimeStampl RemoveHashedFields f Nonce Agent RemoveEncryption Nonce Agent PublicKey RemoveHash f Nonce Nonce TimeStamp SwapPairs Nonce Agent Coalese Nonce Nonce RemovePlainAndEnc 52 9 SIMPLIFYING TRANSFORMATIONS All the simplifications are defined in terms of the type of the messages to be simplified Each simplification is applied uniformly to all the mess
65. l three times System INITIATOR Alice Sam Kab RESPONDER Bob SERVER Sam SERVER Sam SERVER Sam When this system is checked FDR finds that initiator Alice is not au thenticated according to the above timed specification Using the debugger and interpret produces the following result Alice believes she is running the protocol taking role INITIATOR with Bob using data items Kab Time passes 20 4 CASE STUDY THE VVIDE MOUTHED FROG PROTOCOL Time passes Time passes Bob believes he has completed a run of the protocol taking role RESPONDER with Alice using data items Kab Each time passes represents one unit of time passing Bob completes his protocol run three time units after Alice was running the protocol Exploring the debug tree we can find that the attack takes the following form a l Alice Sam Bob 0 Kab grey Atice a 2 Sam Mo Alice 0 Kab skey Bob tock 0 1 Mego o Sam Alice 0 Kab sxey Bos 6 2 Sam Malice Bob 1 Kab skey Alice tock 7 1 Mane gt Sam Bob 1 Kab skey Alice 7 2 Sam Mg Alice 2 Kab skey Bob tock 6 1 Msam Bob Alice 2 Kab sxey Bob The intruder plays ping pong with the server continually replaying messages so that the timestamp is updated each time It should be obvious how the intruder could continue such an exchange for longer so as to break a timed specification with a weaker time constraint This attack was
66. ld find no attacks against the protocol However there exists an injective authentication attack against the repeated authentication section as shown below 1 Alice gt Sam Bob Ma a 2a Sam Alice Ma 0 Bob Kab uKey Atice a 2b Sam Alice Ma 0 Kab Alice skey Bob a 4 Alice Bob Ma 0 Kab Alice skey Bob a 5 Bob Alice Nb1 Ma Alice ras a 6 Alice Bob Bob Nb1 tras 9 Alice IBob Ma 0 Kab Alice skey Bob 68 5 Igo Alice Nb1 Ma Alice kab B 6 Alice IBob Bob ko Hence Agreement s u kab does not hold in this protocol Casper can detect this attack if GenerateSystemForRepeatSection 4 to 6 is specified instead of GenerateSystem True When this flag is specified the system construction is altered rather than ensuring that all data independent arguments to external processes are disjoint it instead does the following If a data independent argument to the external process is first 7 5 Minimising state space explosion 47 used in the non repeat section then an InternalUnknown value is picked and the same value is picked for all external instances otherwise an external value is picked as before By forcing the external processes to use InternalUnknown values for vari ables introduced outside of the repeat section we ensure that the internal agents are capable of performing the same repeat section with variables dif fering only when they are introdu
67. le to change the identity on the public key requesting message so that the key server delivers the wrong public key namely the intruder s Answer to Exercise 3 Your input script should look something like the following TMN protocol Free variables A B Agent S Server pks PublicKey sks SecretKey ka kb SessionKey InverseKeys pks sks Processes 62 B ANSVVERS TO THE EXERCISES INITIATOR A S pks ka RESPONDER B S pks kb SERVER S sks Protocol description 0 5 A B A B 1 A gt S B ka pks A B 2 S gt B A A B 3 B gt S A kb pks 4 S gt A kb ka Specification Secret A ka B S Secret A kb B S Secret B kb 4 Actual variables Alice Bob Mallory Agent Sam Server PKs PublicKey SKs SecretKey Ka Kb Km SessionKey InverseKeys PKs SKs System INITIATOR Alice Sam PKs Ka RESPONDER Bob Sam PKs Kb SERVER Sam SKs Intruder Information Intruder Mallory IntruderKnowledge Alice Bob Mallory Sam PKs Km B 3 Answers to exercises from Section 5 63 This should detect an attack which can be interpreted as follows 1 ance gt Sam Bob Km pps 2 Bob Alice Bob believes Kb is a secret shared with Sam Alice 3 Bob Sam Alice Kb pgs 4 Sam Km Kb The intruder knows Kb This attack exploits the fact that message 1 is not authent
68. message 1 Mallory then forwards the encrypted component from the first message to Bob but under his own identity second message 1 Bob sees nothing wrong with this message so he responds with a message 2 from which Mallory can learn the value of Na Finally Mallory completes the protocol run by faking a message 2 back to Alice When FDR is used to test the assertion dealing with authentication of the responder Bob the test should fail giving an attack very similar to the one above B 3 Answers to exercises from Section 5 B 3 Answers to exercises from Section 5 61 Answer to Exercise 1 The protocol decription should be changed to the following Protocol description 0 gt a b 1 a gt b na 2 b gt s nb fa na ServerKey b 3 s gt a nb fb kab na ServerKey a la kab nb ServerKey b 4 b v kab nb ServerKey b nb kab Analyzing this protocol gives the folloving attack 0 Alice Bob 1 Alice Igo Nal 1 B Alice Nal 2 Alice gt Isam Na2 Bob Nal serverKey Alice 2 Tan Sam Na1 1Bob Nal serverKey Alice 3 Sam gt Igo Nal Alice Kab Nal serverKey Bob Bob Kab Nal ServerKeyAlice 3 Isam Alice Nal Bob Kab Nal serverKeyAlice Bob Kab Nal ServerKey Alice 4 4 Alice I Bob Bob Kab Nal ServerKey Alice Nal Kab Answer to Exercise 2 You should find that in each case the intruder is ab
69. n most get caught by the compiler and those errors that do get through are easier to spot because the file is so much shorter I anticipate that the Casper compiler will continue to evolve in the future In particular the following features are anticipated e Key compromise will be modelled e Non atomic keys will be supported e A richer set of agent actions will be supported I would be interested to receive requests for further features Acknowledgements Much of the code of Casper was written by Philippa Broadfoot The simpli fying transformations code was written by Mei Lin Hui I would also like to thank Bill Roscoe Peter Ryan Irfan Zakiuddan Steve Schneider Joshua Guttman Paul Gardiner Michael Goldsmith Bryan Scattergood Simon Ambler Mark Reilly Paul Norris and Ben Donovan for useful comments and discussions about Casper This work was partially funded by the US Office of Naval Research the UK Defence Evaluation and Research Agency and the UK EPSRC 54 REFERENCES References AN95 Ross Anderson and Roger Needham Programming Satan s com BAN89 BL03 BLR00 Cas98 Dil08 DLO8 For97 HL99 puter In J van Leeuwen editor Computer Science Today volume 1000 of Lecture Notes in Computer Science Springer Verlag 1995 Michael Burrows Mart n Abadi and Roger Needham A logic of authentication Proceedings of the Royal Society of London A 426 233 271 1989 A preliminary version a
70. n agent s secret key to be symbolic this means that Casper produces its own values to represent the results of function ap plications 2 3 3 System definition The most important part of the system definition covers which agents should be present in the system to be checked This is done by listing the agents with the parameters suitable instantiated as follows HSystem INITIATOR Alice Na RESPONDER Bob Nb Thus we consider a system with a single initiator Alice taking the role of A in the protocol description and a single responder Bob who can each run the protocol once they use nonces Na and Nb The types of the parameters of the processes should match the types of the parameters of the corresponding processes defined under the Processes heading Section 2 2 3 2 3 4 The intruder Finally the operation of the intruder is specified by giving his identity and the set of data values that he knows initially Intruder Information Intruder Mallory IntruderKnowledge Alice Bob Mallory Nm PK SK Mallory The above defines the intruder s identity to be Mallory and defines that the intruder initially knows all the agents identities a single nonce Nm the public key function PK and his own secret key SKm The inclusion of the function PK in the intruder s knowledge means that he can immediately calculate PK Alice PK Bob and PK Mallory Exercise 2 1 Copy the input file NS3 spl and then edit it so
71. nce NonceNB 7 2 Assumptions and Threshold Theorems 41 Actual variables Np Nonce InternalKnown Nal Na2 Nonce InternalUnknown NonceNA Nb1 Nb2 Nonce InternalUnknown NonceNB Nel Ne2 Nonce External Note that if a variable either actual or free has no subtype then it is assumed that it is a member of every subtype For details of how many variables of each type are required see Section 7 2 The last required alteration that is required is to add the flag UnboundParallel True to the Intruder information section of the in put script 7 2 Assumptions and Threshold Theorems In this section we detail the assumptions that the data independent model makes and the minimum number of actual variables required to prove a protocol is correct In particular if no attacks are found against a system that satisfies these assumptions and has sufficient actual variables then no attack exists on a system that contains an unbounded number of agents running this protocol using infinite types The data independent model makes one assumption in addition to the Dolev Yao assumptions namely that there exist no inequality tests in the protocol For example it is frequently assumed that an agent will not open a session with itself and thus tests such as a b are included However in the data independent model a test of this sort is prohibited The minimum number of actual variables that are required depends on the type of specif
72. ntly with B with A taking the role of initiator using the same nonces and further each such run of B corresponds to a unique run of A This is a particular form of authentication we discuss various other forms in Section 5 4 2 3 The system definition The second part of the input file deals with the actual system to be checked 2 3 1 Type definitions The types of variables to be used in the actual system to be checked are defined in a similar way to the types of the free variables Actual variables Alice Bob Mallory Agent Na Nb Nm Nonce Thus we will be dealing with a system with three agents Mallory will be the intruder and three nonces the public and secret keys of these agents are defined in the Functions section below I normally use the convention that free variables representing agents are denoted by a single capital letter A B etc while actual variables repre senting agents are denoted by real names Alice Bob etc Similarly free variables representing other data items are denoted by small letters e g na while the corresponding actual values are denoted by identifiers starting with a capital letter e g Na 2 3 2 Functions Any functions used by the agents in the protocol description have to be defined under the Functions heading Functions symbolic PK SK 2 3 The system definition 9 The above defines the functions PK which returns an agent s public key and SK which returns a
73. old style designation of secret is equivalent to C NRA NR the old style designation of authenticated is equivalent to NF NRA NR and Stream 7 Using data independence techniques m Ros98 Roscoe showed how techniques borrowed from data independence and related fields can be used to achieve the illusion that agents can call upon an infinite supply of different nonces keys etc even though the actual types used for these values remain finite It is thus possible to create models of protocols in which agents do not have to stop after a small number of sequential runs m Kle08 Kleiner used data independence methods to extend the work of Roscoe to allow an unbounded number of parallel sessions with the same agent to occur Informally the idea is that agents in the system are inter nalised into the intruder these agents are referred to as internal agents This effectively means that the intruder is given an oracle of the behaviour of the internal agents In this section we describe how these techniques can be used from within Casper 7 1 How to use data independence techniques A complete input script using data independence techniques is given in Ap pendix A 2 We describe below the essential data independence features 40 7 USING DATA INDEPENDENCE TECHNIQUES The first change comes within the Processes section Variables of data independent types are indicated using the generates keyword values for such variables will be freshly
74. or example the following channels section specifies the use of C A NR on the channel for message 2 and NF A NRA on the channel for messages 1 and 3 Channels 1 NF NRA 2 NR 3 NF NRA 6 2 New style secure channels 35 The channel properties must be listed for each message individually and must be listed in the order C NF NRA NR The script below illustrates the technique on a version of the SAML Sin gle Sign On protocol note that this is not a realistic model of the protocol A user wants to authenticate herself to a service provider with the help of an identity provider The user and identity provider have pre existing shared secrets so are able to establish confidential authenticated channels that sat isfy C A NF A NRA A NR in each direction e g bilateral TLS the service provider and identity provider each has some means of authenticat ing himself e g a public key certificate so are likewise able to establish confidential authenticated channels in each direction the service provider has some means of authenticating himself e g a public key certificate so is able to establish a one way authenticated channel that satisfies C A NR e g unilateral TLS to the user but the user cannot directly authenticate herself to the service provider SAML Single Sign On 550 protocol Free variables u User sp ServiceProvider idp IdProvider m Message nidp Nonce a Artifact
75. pe flaws Up until now we have been assuming that the different data types within a system were disjoint That is we have been considering systems where the atomic data items carried typing information so that an agent receiving a data item could tell whether it was for example a nonce an agent s identity or a key However some protocol implementations do not achieve this and as a result the protocols are open to attack Within Casper it is possible to define that a particular data item can be interpreted as being of more than one type by including the name of that data item within more than one type definition line in the Actual variables section For example we can define that Bob s identity could be interpreted as being either an agent s identity or a nonce via the lines Actual variables Alice Bob Mallory Agent Nb Nb Bob Nonce Exercise 5 4 Consider the seven message version of the Needham Schroeder Public Key Protocol a gt s S gt 0 16 PK b sskts 2x275 5 155 5 b gt 8 4 s b La PK a ssk a b a b a na 5 PK a a b imi pet WA lo 30 5 CARRYING ON Code up this protocol using a system where two agents Alice and Bob can both run the protocol once as responder but not as initiator and the key server can run the protocol once Also allow Bob s nonce to be interpreted as an agent s identity It is reasonable to assume that the key ser
76. ppeared as Digital Equipment Corporation Systems Research Center report No 39 1989 Philippa Broadfoot and Gavin Lowe On distributed security trans actions that use secure transport protocols In Proceedings of the 16th IEEE Computer Security Foundations Workshop pages 141 151 2003 Philippa Broadfoot Gavin Lowe and Bill Roscoe Automating data independence In Proceedings of ESORICS 2000 pages 175 190 2000 Casper example library 1998 Available via URL http www comlab ox ac uk people gavin lowe Security Casper library tar gz Christopher Dillovvay On the Specification and Analy sis of Secure Transport Layers DPhil Oxford University 2008 http veb comlab ox ac uk activities security papers dilloway_thesis pdf Christopher Dilloway and Gavin Lowe Specifying secure trans port layers In 21st IEEE Computer Security Foundations Sym posium CSF 21 2008 http www comlab ox ac uk files 116 channels pdf Formal Systems Europe Ltd Failures Divergence Refinement FDR 2 User Manual 1997 Available via URL http www formal demon co uk FDR2 html Mei Lin Hui and Gavin Lowe Safe simplifying transformations for security protocols In Proceedings of the 12th IEEE Computer Security Foundations Workshop 1999 REFERENCES 59 85 Kle08 Low95 Low96 Low97 Low98 Low02 LR97 Mea96 NS78 RB99 C A R Hoare Communicating Sequential Processes Prentice
77. r act inv key pair C identifier identifier 2 C 9 Functions section 77 C 9 Functions section functions section Functions 1 functions line functions line erplicit function line symbolic line explicit function line x fn def lhs identifier 22 fn def lhs identifier C fn def arg fn def arg fn def arg identifier symbolic line symbolic identifier identifier C 10 System section system section System agent dec withdraw dec generate system agent dec instance dec instance dec 21 instance dec process name C identifier identifier withdraw dec WithdrawOption True False 41 generate system GenerateSystem True GenerateSystemForRepeatSection C 11 Intruder section intruder section deduction line no to line no Intruder Information 21 Intruder identifier IntruderKnowledge P atom atom Y all internal proc dec stale knowledge dec crackable dec guessable dec UnboundParallel True deduction forall quants 42 msg 1 msg 1 msg x 78 internal proc dec stale knowledge dec crackable dec crackable type guessable dec C 12 Secure channels channels section old channel spec channel spec
78. rallel True Note that if multiple specifications are in the same file then they all must require the same agent to be external Hence all specifications must be of the form Agreement _ b _ or Secret for some b The system that is generated is designed in such a way to avoid any type flaw attacks as mentioned above However it does not by default eliminate 46 7 USING DATA INDEPENDENCE TECHNIQUES false attacks that occur as a result of an overlap between InternalUnknown and InternalKnown values To eliminate false attacks due to a variable v that overlaps place a secrecy specification of the form Secret a v as for appro priate a and as in the same file This will cause the resulting generated sys tem to have no overlap between the InternalUnknown and InternalKnown values 7 4 Repeat Sections A repeat section within a protocol is a section that is repeated a potentially unbounded number of times For example consider the following modified version of the KSL protocol u is a user as is the authentication server and s is a server that u wishes to be authenticated to 1 q as s ma 20 as ima ts 8 kab UKeytu 20 as ma ts kab U SKey s 4 Urs ma ts kab u sKey s 5 s u nb ma ul ra 6 s nblkm Messages 4 6 are intended to be performed repeatedly until the ticket expires If you were to analyse the protocol using the standard data independence methods you wou
79. re are some properties that cannot For example the specification if Bob receives a message 3 then previously Alice sends a message 2 or Sam sends a message 2 is not testable because of the disjunction Furthermore the authentication properties apply only to complete runs of the protocol which is not true of the temporal specifications since any message may be specified partial runs of the protocol are also considered Casper therefore allows specifications to be entered in a restricted temporal logic consisting of just one temporal operator previously written as o below along with conjunction disjunction and implication Here we provide a brief description of the semantics for the full details of the input syntax see Section C 6 A temporal logic specification is a formula of the form p q where p is any formula built from A V and such that p is not a disjunction for specifications such as p V q gt r the specification should be split into two specifications p gt r and q gt r e q is any formula built from A V and o 49 Also in the model that we consider the sending and receiving of messages is considered atomic and therefore no more than one atomic event can occur at any given time unit Therefore specifications such as o p A q are not allowed instead users can write op A oq Lastly o binds weakest of all meaning that op V q is equal to o p V q The atomic events that we allow are the sending or receiving of
80. reason for including this specification form is that it is the form of secrecy considered in Low98 Agreement A B vi Vn specifies that A is correctly authen ticated to B and the agents agree upon Un more precisely if B thinks he has successfully completed a run of the protocol with A then A has previously been running the protocol apparently with B and both agents agreed as to which roles they took and both agents agreed as to the values of the variables v Un and there is a one one relationship between the runs of B and the runs of A The specification NonInjectiveAgreement A B v1 Vn means that if B thinks he has successfully completed a run of the protocol with A then A has previously been running the protocol apparently with B and both agents agreed as to which roles they took and both agents agreed as to the values of the variables Un Note that several runs of B may correspond to the same run of A e The specification WeakAgreement A B means that if B thinks he has successfully completed a run of the protocol with A then A has previously been running the protocol apparently with B Note that A and B may disagree as to which role each was taking 26 5 CARRYING ON e The specification Aliveness A B means that if B thinks he has suc cessfully completed a run of the protocol with A then A has previously been running the protocol Note that A may have thought he w
81. s information is used to check that the protocol definition is feasible in the sense that agents only send messages that they could be expected to create and only receive messages that they could be expected to decrypt e Later under the System heading below we will instantiate the pa rameters with actual values so as to define a system and define the data values that each agent should use in their runs For example suppose we define a system with a particular initiator Alice that is we instantiate the variable A with the value Alice Then we would expect that in each run Alice would use a different nonce in each run that is na would be instantiated with different values in each run On the other hand the data items PK and SK A do not appear as parame ters because we would expect the same values to be used in every run SK A depending upon the identity A 2 2 The protocol definition 7 Whenever an agent sends a message it should be the case that the agent possesses all the components necessary to produce it for example B is able to send message 2 because he knows na learnt from message 1 nb from his parameter list and PK A from his knowledge of PK and A Similarly if it is the intention that an agent should decrypt an encrypted component that he receives then he should possess the decrypting key An agent will accept a message it receives if all fields represented by variables already in the agent s knowledge cont
82. s of which others InverseKeys PK SK The above line means that the functions PK and SK when applied to the same identity return keys that are inverses of each other so for every agent A PK A A s public key and SK A A s secret key are inverses of one another 6 2 AN EXAMPLE INPUT FILE 2 2 3 Processes Bach agent running in the system will be represented by a CSP process The names of the CSP processes representing the agents are defined as below Processes INITIATOR A na knows PK SK A RESPONDER B nb knows PK SK B These lines have several tasks e They give names to the roles played by the different agents here INITIATOR and RESPONDER These names are also used as the names of the CSP processes that represent the agents For example the agent represented by A in the protocol description will be repre sented by a CSP process INITIATOR parameterized by the arguments A and na e The parameters and the variables following the keyword knows de fine the knowledge that the agent in question is expected to have at the beginning of the protocol run For example the initiator A is expected to know his own identity A the nonce na the public key function PK i e he can look up public keys in some table and his own secret key SK A The first parameter should be the string that represents the agent in the protocol description section 2 2 1 and will be instantiated with the agent s identity Thi
83. system can cause the checking time to rise greatly it can help to split specifications into several input files that can be run independently Lastly whilst the GenerateSystem flag is extremely useful and makes using the data independent model substantially easier it does not produce the minimum number of variables It may be possible to reduce the number of variables required by collapsing some of the types which must be done by hand It is recommended that the user starts off with the minimum number of values as dictated by the above threshold theorems and then adds variables as necessary to remove the false attacks 48 8 SPECIFYING PROPERTIES USING TEMPORAL LOGIC 7 6 Current limitations The current limitations upon the models using the data independence tech niques are as follows e No algebraic equivalences can be defined e Secure channels cannot be used e Guessing attacks cannot be modelled e Crackables are not allowed Note also that the counterexamples given by casperFDR are not very informative because any interaction with an internal agent will appear as I Agent Therefore if a protocol is found to be insecure then it is recom mended that the user attempts to build a small system using the standard model that exhibits the problem S Specifying Properties using Temporal Logic Whilst most secrecy and authentication properties of security protocols can be captured using Casper s Secret and Agreement specifications the
84. systems to try checking Larger systems require considerably more time to check the rate of increase varies from protocol to protocol so a pragmatic approach is to start with a small system and work up which is what we do here The systems we check below have admittedly been tailored slightly to discovering certain attacks however the first three systems are among the first few I would try if coming at this protocol blind 4 1 Modelling the protocol Most of the modelling of the protocol is straight forward below we concen trate on the parts that require techniques not discussed above The free variables are declared as follows Free variables A B Agent S Server SKey Agent gt ServerKey kab SessionKey ts ts TimeStamp InverseKeys SKey SKey As explained in Section 2 most type names can be chosen by the user one exception to this rule concerns timestamps which must be represented by the 16 4 CASE STUDY THE VVIDE MOUTHED FROG PROTOCOL type TimeStamp Note that the InverseKeys line declares that keys returned by the SKey function are self inverse i e symmetric The agents taking part in the protocol can be defined as follovvs Processes INITIATOR A S kab knows SKey A RESPONDER B knows SKey B SERVER S knows SKey Note that the server is assumed to know all the keys he shares with other agents so we specify that he knows all of the SKey function However A and B only know the key th
85. ter digit C 6 Specification section 75 The sender and receiver fields for each message i e the fields preceding and following the gt should both be declared as identities of agents in the Processes section The type fdr expression represents all expressions accepted by FDR the syntax is basically that of a simple functional language see For97 for details C 6 Specification spec section spec agents fields time temporal spec section Specification 21 spec temporal spec Secret C identifier atom agents 97 1 StrongSecret C identifier atom agents 97 22 Agreement C identifier identifier fields 1 NonInjectiveAgreement identifier identifier fields 91 1 WeakAgreement C identifier identifier Aliveness C identifier identifier Y 1 TimedAgreement C identifier identifier time fields Y 1 TimedNonInjectiveAgreement C identifier identifier time fields 97 1 TimedWeakAgreement identifier identifier time Y 23 TimedAliveness C identifier identifier time 22 P identifier identifier 1 P identifier identifier Y N if temporal formul
86. tocol 7 message version with type flaw Free variables 64 B ANSVVERS TO THE EXERCISES A B Agent na nb Nonce pka pkb PublicKey PK Agent gt PublicKey SK Agent gt SecretKey PKS Server gt ServerPublicKey SKS Server gt ServerSecretKey realAgent Agent gt Bool S Server InverseKeys PK SK PKS SKS Processes INITIATOR A na S knows SK A PKS RESPONDER B nb S knows SK B PKS SERVER S knows PK SKS S Protocol description 0 gt A 2B realAgent B 1 A gt S B realAgent B 2 S gt A B PK B pkb SKS S 3 A gt B na A pkb PK B 4 B gt S A realAgent A 1 5 S gt B A PK A 7 pka SKS S 6 B gt A na nb pka PK A 7 A gt B nb pkb PK B Specification Secret A na B Secret B nb A Agreement A B na nb Agreement B A na nb Actual variables Alice Bob Mallory Nb Agent Na Nb Nm Nonce Sam Server Functions symbolic PK SK PKS SKS realAgent Alice true B 3 Answers to exercises from Section 5 65 realAgent Bob true realAgent Mallory true realAgent _ false System RESPONDER Alice Na Sam RESPONDER Bob Nb Sam SERVER Sam Intruder Information Intruder Mallory IntruderKnovledge Alice Bob Mallory Nm Sam PK PKS SK Mallory Note that we have defined Nb so that it can be interpreted as either a nonce or an agent s identity
87. ver knows the identities of all genuine agents so would not accept Bob s nonce as being an agent s identity how can we model this FDR should find an attack upon the resulting system amp Note that the attack found in the above exercise would not work if mes sage 3 included the sender s identity as plaintext the intruder would not be able to create message 6 3 because he does not know the identity of the apparent sender Nb When not considering type flaws it is normal to omit plaintext sender and receiver fields because it is normal to assume that the intruder knows all the agents identities however when considering type flaws it can be important to include these identities Note that giving data items multiple types can greatly increase the state space to be checked so this technique should be used with some caution More than a little guess work is required in deciding which data items should be given multiple types in order to have a good chance of finding an attack This question certainly requires more research but a good rule of thumb would be to try and spot whether part of a message may be inter preted as coming from a different message when a data item is interpreted as being of a different type For example in the attack on the Needham Schroeder Public Key Protocol discussed in question 4 a message 6 of the form Nm Nb pk a was interpreted as being part of a message 3 when the nonce Nb was interpreted as being
88. wers to exercises from Section 5 The Casper syntax Cul Basic denies dk ee AAA Ce Syntax a ea to Sew Be ee eS eee x A C 3 Free variables section scott Se do 9 C4 Processes section x we hse amp Be C 5 Protocol description section n da e A C 6 Specification section rro s C 7 Algebraic equivalences section C 8 Actual variables section C 9 Functions section s oe be PAS bp oe LA C 10 System section eco 33 33 34 39 39 Al 45 46 AT 48 48 51 53 56 56 57 58 59 59 60 60 CONTENTS ii C 11 Intruder section TT C 12 Secure channels section 78 C 13 Simplifying transformations script 78 C 14 Simplifications section eS 78 CONTENTS 1 Introduction Many security protocols have appeared in the academic literature with var ious goals such as establishing a cryptographic key or achieving authentica tion where an agent becomes sure of the identity of the other agent taking part in the protocol These protocols are supposed to succeed even in the presence of a malicious agent called an intruder this intruder is assumed to have complete control over the communications network and so can inter cept messages and introduce new messages into the system using information from messages he has previously seen Unfortunatel
89. y a large proportion of the protocols that have been suggested do not succeed in their stated goals Over the last few years a method for analyzing security protocols using the process algebra CSP Hoa85 and its model checker FDR Ros94 has been developed Ros95 Low96 LR97 Briefly e Each agent taking part in the protocol is modelled as a CSP process e The most general intruder who can interact with the protocol is also modelled as a CSP process e The resulting system is tested against specifications representing de sired security properties such as correctly achieves authentication or ensures secrecy FDR searches the state space to investigate whether any insecure traces i e sequences of messages can occur e If FDR finds that the specification is not met then it returns a trace of the system that does not satisfy the specification this trace corresponds to an attack upon the protocol This method has proved remarkably successful and has been applied to find attacks upon a number of protocols Low96 LR97 However the task of producing the CSP description of the system is very time consuming and only possible for people well practiced in CSP and even the experts will often make mistakes that prove hard to spot Casper simplifies this process The user specifies the protocol using a more abstract notation similar to the notation appearing in the academic literature and Casper compiles this into CSP code
90. y a generates na RESPONDER b s nb knows ServerKey b generates nb SERVER s kab knows ServerKey generates kab Actual variables Alice Mallory Agent Alice Server vSecret SessionKey InternalUnknown vPublic SessionKey InternalUnknown vPublic SessionKey InternalKnown 44 7 USING DATA INDEPENDENCE TECHNIQUES vPublic Nonce InternalKnown vPublic Nonce InternalUnknown k Nel Ne2 Nonce External InverseKeys vSecret vSecret Inline functions symbolic ServerKey HSystem RESPONDER Alice Sam Nel RESPONDER Alice Sam Ne2 Lines that have been changed or added compared to the secrecy specification above have been marked with a x Whilst the above represents the minimum number of variables required it is recommended that more values are provided in order to avoid type flaw and certain secrecy attacks For example in the above vPublic is both a session key and a nonce and therefore some false attacks may be introduced Also above there is an overlap between InternalUnknown and InternalKnown session keys This can lead to false attacks on protocols such as the one below 1 a b na 2 b s fa na nb serverKey b s a nb b kab na gerverKey a 3b 8 b kab serverKey b 4 a b nb kab Since nb is not transmitted encrypted if kab were an InternalKnown value the intruder could generate message 4 thus leading to a non injective au thentication attack However
91. ystem We will now consider a slightly different system where the responder Bob can run the protocol twice sequentially System INITIATOR Alice Sam Kab RESPONDER Bob RESPONDER Bob SERVER Sam 4 5 Fourth system 19 When we check this system FDR tells us that Alice is not correctly authenticated Using the debugger and interpret gives the following Alice believes she is running the protocol taking role INITIATOR with Bob using data items Kab Bob believes he has completed a run of the protocol taking role RESPONDER with Alice using data items Kab Bob believes he has completed a run of the protocol taking role RESPONDER with Alice using data items Kab Clearly the problem is that Bob thinks he has completed two runs of the protocol while Alice only wanted to perform a single run Exploring the debug tree further we can find that the attack takes the following form a l Alice Sam Bob 0 Kab skey Alice 2 Sam Bob Alice 0 Kab skey Bov B 2 Msam Bob TAlice 0 Kab skey Bob A The intruder simply replays the message from Sam to Bob so that Bob thinks that Alice is trying to establish a second session 4 5 Fourth system We now seek an attack that breaks the 2 time unit limit To do this we should consider a larger time domain TimeStamp 0 3 We will consider a system where initiator Alice and responder Bob each run the protocol once but where the server can run the protoco

Manual - Department of Computer Science

Contents

Download Pdf Manuals

Related Search

Related Contents