src/HOL/Auth/Yahalom.thy
changeset 2156 9c361df93bd5
parent 2125 92a08ee6a9cb
child 2284 80ebd1a213fd
     1.1 --- a/src/HOL/Auth/Yahalom.thy	Fri Nov 01 18:28:19 1996 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom.thy	Fri Nov 01 18:34:34 1996 +0100
     1.3 @@ -59,7 +59,8 @@
     1.4            ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
     1.5  
     1.6           (*This message models possible leaks of session keys.  The Nonces
     1.7 -           identify the protocol run.*)
     1.8 +           identify the protocol run.  Quoting Server here ensures they are
     1.9 +           correct.*)
    1.10      Oops "[| evs: yahalom lost;  A ~= Spy;
    1.11               Says Server A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} 
    1.12                                     (shrK A),