src/HOL/Auth/Yahalom2.thy
changeset 2284 80ebd1a213fd
parent 2155 dc85854810eb
child 2378 fc103154ad8f
     1.1 --- a/src/HOL/Auth/Yahalom2.thy	Fri Nov 29 17:58:18 1996 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom2.thy	Fri Nov 29 18:03:21 1996 +0100
     1.3 @@ -48,25 +48,25 @@
     1.4                 : set_of_list evs |]
     1.5            ==> Says Server A
     1.6                 {|Nonce NB, 
     1.7 -                 Crypt {|Agent B, Key (newK evs), Nonce NA|} (shrK A),
     1.8 -                 Crypt {|Nonce NB, Key (newK evs), Agent A|} (shrK B)|}
     1.9 +                 Crypt (shrK A) {|Agent B, Key (newK evs), Nonce NA|},
    1.10 +                 Crypt (shrK B) {|Nonce NB, Key (newK evs), Agent A|}|}
    1.11                   # evs : yahalom lost"
    1.12  
    1.13           (*Alice receives the Server's (?) message, checks her Nonce, and
    1.14             uses the new session key to send Bob his Nonce.*)
    1.15      YM4  "[| evs: yahalom lost;  A ~= Server;  A ~= B;  
    1.16 -             Says S A {|Nonce NB, Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
    1.17 +             Says S A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    1.18                          X|}
    1.19                 : set_of_list evs;
    1.20               Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
    1.21 -          ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
    1.22 +          ==> Says A B {|X, Crypt K (Nonce NB)|} # evs : yahalom lost"
    1.23  
    1.24           (*This message models possible leaks of session keys.  The nonces
    1.25             identify the protocol run.  Quoting Server here ensures they are
    1.26             correct. *)
    1.27      Oops "[| evs: yahalom lost;  A ~= Spy;
    1.28               Says Server A {|Nonce NB, 
    1.29 -                             Crypt {|Agent B, Key K, Nonce NA|} (shrK A),
    1.30 +                             Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
    1.31                               X|}  : set_of_list evs |]
    1.32            ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
    1.33