src/HOL/Auth/Yahalom2.thy
changeset 5066 30271d90644f
parent 4537 4e835bd9fada
child 5359 bd539b72d484
     1.1 --- a/src/HOL/Auth/Yahalom2.thy	Mon Jun 22 15:50:59 1998 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Mon Jun 22 15:53:24 1998 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  
     1.5           (*The Server receives Bob's message.  He responds by sending a
     1.6             new session key to Alice, with a certificate for forwarding to Bob.
     1.7 -           Fields are reversed in the 2nd certificate to prevent attacks!! *)
     1.8 +           Both agents are quoted in the 2nd certificate to prevent attacks!*)
     1.9      YM3  "[| evs3: yahalom;  A ~= B;  A ~= Server;  Key KAB ~: used evs3;
    1.10               Says B' Server {|Agent B, Nonce NB,
    1.11  			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
    1.12 @@ -50,7 +50,7 @@
    1.13            ==> Says Server A
    1.14                 {|Nonce NB, 
    1.15                   Crypt (shrK A) {|Agent B, Key KAB, Nonce NA|},
    1.16 -                 Crypt (shrK B) {|Nonce NB, Key KAB, Agent A|}|}
    1.17 +                 Crypt (shrK B) {|Agent A, Agent B, Key KAB, Nonce NB|}|}
    1.18                   # evs3 : yahalom"
    1.19  
    1.20           (*Alice receives the Server's (?) message, checks her Nonce, and