src/HOL/Auth/Yahalom2.thy
changeset 3432 04412cfe6861
parent 2516 4d68fbe6378b
child 3445 96fcfbfa4fb5
     1.1 --- a/src/HOL/Auth/Yahalom2.thy	Mon Jun 09 10:21:05 1997 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Mon Jun 09 10:21:38 1997 +0200
     1.3 @@ -6,8 +6,7 @@
     1.4  Inductive relation "yahalom" for the Yahalom protocol, Variant 2.
     1.5  
     1.6  This version trades encryption of NB for additional explicitness in YM3.
     1.7 -It also omits encryption in YM2.  The resulting protocol no longer guarantees
     1.8 -that the other agent is present.
     1.9 +Also in YM3, care is taken to make the two certificates distinct.
    1.10  
    1.11  From page 259 of
    1.12    Burrows, Abadi and Needham.  A Logic of Authentication.
    1.13 @@ -37,14 +36,16 @@
    1.14  	   the sender is, hence the A' in the sender field.*)
    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 NB|} # evs
    1.18 -                : yahalom lost"
    1.19 +          ==> Says B Server 
    1.20 +                  {|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
    1.21 +                # evs : yahalom lost"
    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 +           !! Fields are reversed in the 2nd packet to prevent attacks!! *)
    1.27      YM3  "[| evs: yahalom lost;  A ~= B;  A ~= Server;  Key KAB ~: used evs;
    1.28 -             Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
    1.29 +             Says B' Server {|Agent B, Nonce NB,
    1.30 +			      Crypt (shrK B) {|Agent A, Nonce NA|}|}
    1.31                 : set_of_list evs |]
    1.32            ==> Says Server A
    1.33                 {|Nonce NB,