src/HOL/Auth/Yahalom2.thy
changeset 3659 eddedfe2f3f8
parent 3519 ab0a9fbed4c0
child 3683 aafe719dff14
     1.1 --- a/src/HOL/Auth/Yahalom2.thy	Thu Sep 04 17:57:56 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Fri Sep 05 12:24:13 1997 +0200
     1.3 @@ -29,45 +29,45 @@
     1.4            ==> Says Spy B X  # evs : yahalom"
     1.5  
     1.6           (*Alice initiates a protocol run*)
     1.7 -    YM1  "[| evs: yahalom;  A ~= B;  Nonce NA ~: used evs |]
     1.8 -          ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom"
     1.9 +    YM1  "[| evs1: yahalom;  A ~= B;  Nonce NA ~: used evs1 |]
    1.10 +          ==> Says A B {|Agent A, Nonce NA|} # evs1 : yahalom"
    1.11  
    1.12           (*Bob's response to Alice's message.  Bob doesn't know who 
    1.13  	   the sender is, hence the A' in the sender field.*)
    1.14 -    YM2  "[| evs: yahalom;  B ~= Server;  Nonce NB ~: used evs;
    1.15 -             Says A' B {|Agent A, Nonce NA|} : set evs |]
    1.16 +    YM2  "[| evs2: yahalom;  B ~= Server;  Nonce NB ~: used evs2;
    1.17 +             Says A' B {|Agent A, Nonce NA|} : set evs2 |]
    1.18            ==> Says B Server 
    1.19                    {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
    1.20 -                # evs : yahalom"
    1.21 +                # evs2 : yahalom"
    1.22  
    1.23           (*The Server receives Bob's message.  He responds by sending a
    1.24 -           new session key to Alice, with a packet for forwarding to Bob.
    1.25 -           !! Fields are reversed in the 2nd packet to prevent attacks!! *)
    1.26 -    YM3  "[| evs: yahalom;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
    1.27 +           new session key to Alice, with a certificate for forwarding to Bob.
    1.28 +           Fields are reversed in the 2nd certificate to prevent attacks!! *)
    1.29 +    YM3  "[| evs3: yahalom;  A ~= B;  A ~= Server;  Key KAB ~: used evs3;
    1.30               Says B' Server {|Agent B, Nonce NB,
    1.31  			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
    1.32 -               : set evs |]
    1.33 +               : set evs3 |]
    1.34            ==> Says Server A
    1.35                 {|Nonce NB, 
    1.36                   Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
    1.37                   Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|}
    1.38 -                 # evs : yahalom"
    1.39 +                 # evs3 : yahalom"
    1.40  
    1.41           (*Alice receives the Server's (?) message, checks her Nonce, and
    1.42             uses the new session key to send Bob his Nonce.*)
    1.43 -    YM4  "[| evs: yahalom;  A ~= Server;  
    1.44 +    YM4  "[| evs4: yahalom;  A ~= Server;  
    1.45               Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    1.46 -                        X|}  : set evs;
    1.47 -             Says A B {|Agent A, Nonce NA|} : set evs |]
    1.48 -          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom"
    1.49 +                        X|}  : set evs4;
    1.50 +             Says A B {|Agent A, Nonce NA|} : set evs4 |]
    1.51 +          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom"
    1.52  
    1.53           (*This message models possible leaks of session keys.  The nonces
    1.54             identify the protocol run.  Quoting Server here ensures they are
    1.55             correct. *)
    1.56 -    Oops "[| evs: yahalom;  A ~= Spy;
    1.57 +    Oops "[| evso: yahalom;  A ~= Spy;
    1.58               Says Server A {|Nonce NB, 
    1.59                               Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    1.60 -                             X|}  : set evs |]
    1.61 -          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom"
    1.62 +                             X|}  : set evso |]
    1.63 +          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
    1.64  
    1.65  end