src/HOL/Auth/Shared.thy

--- a/src/HOL/Auth/Shared.thy	Mon Sep 09 17:34:24 1996 +0200
+++ b/src/HOL/Auth/Shared.thy	Mon Sep 09 17:44:20 1996 +0200
@@ -14,6 +14,7 @@
 
 consts
   shrK    :: agent => key  (*symmetric keys*)
+  leaked  :: nat set       (*Friendly agents whose keys have leaked to Enemy*)
 
 rules
   isSym_shrK "isSymKey (shrK A)"
@@ -25,7 +26,8 @@
         (*Server knows all keys; other agents know only their own*)
   initState_Server  "initState Server     = Key `` range shrK"
   initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
-  initState_Enemy   "initState Enemy  = {Key (shrK Enemy)}"
+  initState_Enemy
+    "initState Enemy = insert (Key (shrK Enemy)) (Key``shrK``Friend``leaked)"
 
 datatype  (*Messages, and components of agent stores*)
   event = Says agent agent msg