1.1 --- a/src/HOL/Auth/Yahalom2.thy	Fri Jan 17 11:50:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Fri Jan 17 12:49:31 1997 +0100
     1.3 @@ -30,26 +30,26 @@
     1.4            ==> Says Spy B X  # evs : yahalom lost"
     1.5  
     1.6           (*Alice initiates a protocol run*)
     1.7 -    YM1  "[| evs: yahalom lost;  A ~= B |]
     1.8 -          ==> Says A B {|Agent A, Nonce (newN(length evs))|} # evs : yahalom lost"
     1.9 +    YM1  "[| evs: yahalom lost;  A ~= B;  Nonce NA ~: used evs |]
    1.10 +          ==> Says A B {|Agent A, Nonce NA|} # evs : yahalom lost"
    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 lost;  B ~= Server;
    1.15 +    YM2  "[| evs: yahalom lost;  B ~= Server;  Nonce NB ~: used evs;
    1.16               Says A' B {|Agent A, Nonce NA|} : set_of_list evs |]
    1.17 -          ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce (newN(length evs))|}
    1.18 -                 # evs : yahalom lost"
    1.19 +          ==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} # evs
    1.20 +                : yahalom lost"
    1.21  
    1.22           (*The Server receives Bob's message.  He responds by sending a
    1.23             new session key to Alice, with a packet for forwarding to Bob.
    1.24             Fields are reversed in the 2nd packet to prevent attacks.*)
    1.25 -    YM3  "[| evs: yahalom lost;  A ~= B;  A ~= Server;
    1.26 +    YM3  "[| evs: yahalom lost;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
    1.27               Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    1.28                 : set_of_list evs |]
    1.29            ==> Says Server A
    1.30                 {|Nonce NB, 
    1.31 -                 Crypt (shrK A) {|Agent B, Key (newK(length evs)), Nonce NA|},
    1.32 -                 Crypt (shrK B) {|Nonce NB, Key (newK(length evs)), Agent A|}|}
    1.33 +                 Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
    1.34 +                 Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|}
    1.35                   # evs : yahalom lost"
    1.36  
    1.37           (*Alice receives the Server's (?) message, checks her Nonce, and