src/HOL/Auth/Yahalom.thy
changeset 3659 eddedfe2f3f8
parent 3519 ab0a9fbed4c0
child 3683 aafe719dff14
     1.1 --- a/src/HOL/Auth/Yahalom.thy	Thu Sep 04 17:57:56 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.thy	Fri Sep 05 12:24:13 1997 +0200
     1.3 @@ -26,44 +26,44 @@
     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, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
    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 -    YM3  "[| evs: yahalom;  A ~= Server;  Key KAB ~: used evs;
    1.26 +    YM3  "[| evs3: yahalom;  A ~= Server;  Key KAB ~: used evs3;
    1.27               Says B' Server 
    1.28                    {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}
    1.29 -               : set evs |]
    1.30 +               : set evs3 |]
    1.31            ==> Says Server A
    1.32                     {|Crypt (shrK A) {|Agent B, Key KAB, Nonce NA, Nonce NB|},
    1.33                       Crypt (shrK B) {|Agent A, Key KAB|}|}
    1.34 -                # evs : yahalom"
    1.35 +                # evs3 : yahalom"
    1.36  
    1.37           (*Alice receives the Server's (?) message, checks her Nonce, and
    1.38             uses the new session key to send Bob his Nonce.*)
    1.39 -    YM4  "[| evs: yahalom;  A ~= Server;  
    1.40 +    YM4  "[| evs4: yahalom;  A ~= Server;  
    1.41               Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
    1.42 -                        X|}  : set evs;
    1.43 -             Says A B {|Agent A, Nonce NA|} : set evs |]
    1.44 -          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom"
    1.45 +                        X|}  : set evs4;
    1.46 +             Says A B {|Agent A, Nonce NA|} : set evs4 |]
    1.47 +          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs4 : yahalom"
    1.48  
    1.49           (*This message models possible leaks of session keys.  The Nonces
    1.50             identify the protocol run.  Quoting Server here ensures they are
    1.51             correct.*)
    1.52 -    Oops "[| evs: yahalom;  A ~= Spy;
    1.53 +    Oops "[| evso: yahalom;  A ~= Spy;
    1.54               Says Server A {|Crypt (shrK A)
    1.55                                     {|Agent B, Key K, Nonce NA, Nonce NB|},
    1.56 -                             X|}  : set evs |]
    1.57 -          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom"
    1.58 +                             X|}  : set evso |]
    1.59 +          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evso : yahalom"
    1.60  
    1.61  
    1.62  constdefs