--- a/src/HOL/Auth/Shared.thy Mon Sep 09 18:53:41 1996 +0200
+++ b/src/HOL/Auth/Shared.thy Mon Sep 09 18:58:02 1996 +0200
@@ -16,6 +16,9 @@
shrK :: agent => key (*symmetric keys*)
leaked :: nat set (*Friendly agents whose keys have leaked to Enemy*)
+constdefs (*Enemy and compromised agents*)
+ bad :: agent set "bad == insert Enemy (Friend``leaked)"
+
rules
isSym_shrK "isSymKey (shrK A)"
@@ -26,8 +29,7 @@
(*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 = insert (Key (shrK Enemy)) (Key``shrK``Friend``leaked)"
+ initState_Enemy "initState Enemy = Key``shrK``bad"
datatype (*Messages, and components of agent stores*)
event = Says agent agent msg