src/HOL/Auth/Yahalom.thy
changeset 1985 84cf16192e03
child 1995 c80e58e78d9c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/Yahalom.thy	Thu Sep 12 10:40:05 1996 +0200
     1.3 @@ -0,0 +1,73 @@
     1.4 +(*  Title:      HOL/Auth/OtwayRees
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Inductive relation "yahalom" for the Yahalom protocol.
    1.10 +
    1.11 +From page 257 of
    1.12 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    1.13 +  Proc. Royal Soc. 426 (1989)
    1.14 +*)
    1.15 +
    1.16 +OtwayRees = Shared + 
    1.17 +
    1.18 +consts  yahalom   :: "event list set"
    1.19 +inductive yahalom
    1.20 +  intrs 
    1.21 +         (*Initial trace is empty*)
    1.22 +    Nil  "[]: yahalom"
    1.23 +
    1.24 +         (*The enemy MAY say anything he CAN say.  We do not expect him to
    1.25 +           invent new nonces here, but he can also use NS1.  Common to
    1.26 +           all similar protocols.*)
    1.27 +    Fake "[| evs: yahalom;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
    1.28 +          ==> Says Enemy B X  # evs : yahalom"
    1.29 +
    1.30 +         (*Alice initiates a protocol run*)
    1.31 +    YM1  "[| evs: yahalom;  A ~= B |]
    1.32 +          ==> Says A B {|Nonce (newN evs), Agent A |} # evs : yahalom"
    1.33 +
    1.34 +         (*Bob's response to Alice's message.  Bob doesn't know who 
    1.35 +	   the sender is, hence the A' in the sender field.
    1.36 +           We modify the published protocol by NOT encrypting NB.*)
    1.37 +    YM2  "[| evs: yahalom;  B ~= Server;
    1.38 +             Says A' B {|Nonce NA, Agent A|} : set_of_list evs |]
    1.39 +          ==> Says B Server 
    1.40 +                  {|Agent B, 
    1.41 +                    Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|}
    1.42 +                 # evs : yahalom"
    1.43 +
    1.44 +         (*The Server receives Bob's message.  He responds by sending a
    1.45 +            new session key to Alice, with a packet for forwarding to Bob.*)
    1.46 +    YM3  "[| evs: yahalom;  B ~= Server;
    1.47 +             Says B' Server 
    1.48 +                  {|Nonce NA, Agent A, Agent B, 
    1.49 +                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
    1.50 +                    Nonce NB, 
    1.51 +                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    1.52 +               : set_of_list evs |]
    1.53 +          ==> Says Server B 
    1.54 +                  {|Nonce NA, 
    1.55 +                    Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
    1.56 +                    Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
    1.57 +                 # evs : yahalom"
    1.58 +
    1.59 +         (*Bob receives the Server's (?) message and compares the Nonces with
    1.60 +	   those in the message he previously sent the Server.*)
    1.61 +    YM4  "[| evs: yahalom;  A ~= B;  
    1.62 +             Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    1.63 +               : set_of_list evs;
    1.64 +             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    1.65 +               : set_of_list evs |]
    1.66 +          ==> (Says B A {|Nonce NA, X|}) # evs : yahalom"
    1.67 +
    1.68 +         (*Alice checks her Nonce, then sends a dummy message to Bob,
    1.69 +           using the new session key.*)
    1.70 +    YM5  "[| evs: yahalom;  
    1.71 +             Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    1.72 +               : set_of_list evs;
    1.73 +             Says A  B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    1.74 +          ==> Says A B (Crypt (Agent A) K)  # evs : yahalom"
    1.75 +
    1.76 +end