--- a/src/HOL/Auth/Yahalom.thy Fri Oct 18 11:42:17 1996 +0200
+++ b/src/HOL/Auth/Yahalom.thy Fri Oct 18 11:42:41 1996 +0200
@@ -59,4 +59,12 @@
Says A B {|Agent A, Nonce NA|} : set_of_list evs |]
==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom lost"
+ (*This message models possible leaks of session keys. The Nonces
+ identify the protocol run.*)
+ Revl "[| evs: yahalom lost; A ~= Spy;
+ Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A),
+ X|}
+ : set_of_list evs |]
+ ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : yahalom lost"
+
end