src/HOL/Auth/Yahalom.thy
changeset 2110 d01151e66cd4
parent 2032 1bbf1bdcaf56
child 2125 92a08ee6a9cb
     1.1 --- a/src/HOL/Auth/Yahalom.thy	Fri Oct 18 11:42:17 1996 +0200
     1.2 +++ b/src/HOL/Auth/Yahalom.thy	Fri Oct 18 11:42:41 1996 +0200
     1.3 @@ -59,4 +59,12 @@
     1.4               Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
     1.5            ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
     1.6  
     1.7 +         (*This message models possible leaks of session keys.  The Nonces
     1.8 +           identify the protocol run.*)
     1.9 +    Revl "[| evs: yahalom lost;  A ~= Spy;
    1.10 +             Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
    1.11 +                        X|}
    1.12 +               : set_of_list evs |]
    1.13 +          ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
    1.14 +
    1.15  end