src/HOL/Auth/Shared.thy
changeset 2032 1bbf1bdcaf56
parent 2012 1b234f1fd9c7
child 2064 5a5e508e2a2b
--- a/src/HOL/Auth/Shared.thy	Thu Sep 26 12:47:47 1996 +0200
+++ b/src/HOL/Auth/Shared.thy	Thu Sep 26 12:50:48 1996 +0200
@@ -12,22 +12,19 @@
 
 consts
   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)"
 
 consts  (*Initial states of agents -- parameter of the construction*)
-  initState :: agent => msg set
+  initState :: [agent set, agent] => msg set
 
 primrec initState agent
         (*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``bad"
+  initState_Server  "initState lost Server     = Key `` range shrK"
+  initState_Friend  "initState lost (Friend i) = {Key (shrK (Friend i))}"
+  initState_Spy   "initState lost Spy      = Key``shrK``lost"
+
 
 datatype  (*Messages, and components of agent stores*)
   event = Says agent agent msg
@@ -38,16 +35,16 @@
 primrec sees1 event
            (*First agent recalls all that it says, but NOT everything
              that is sent to it; it must note such things if/when received*)
-  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
+  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Spy} then {X} else {})"
           (*part of A's internal state*)
 
 consts  
-  sees :: [agent, event list] => msg set
+  sees :: [agent set, agent, event list] => msg set
 
 primrec sees list
         (*Initial knowledge includes all public keys and own private key*)
-  sees_Nil  "sees A []       = initState A"
-  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
+  sees_Nil  "sees lost A []       = initState lost A"
+  sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
 
 
 (*Agents generate "random" nonces.  Different traces always yield
@@ -57,13 +54,12 @@
   newK :: "event list => key"
 
 rules
-  inj_shrK "inj shrK"
+  inj_shrK      "inj shrK"
+
+  inj_newN      "inj newN"
 
-  inj_newN   "inj newN"
-  fresh_newN "Nonce (newN evs) ~: parts (initState B)" 
-
-  inj_newK   "inj newK"
-  fresh_newK "Key (newK evs) ~: parts (initState B)" 
-  isSym_newK "isSymKey (newK evs)"
+  inj_newK      "inj newK"
+  newK_neq_shrK "newK evs ~= shrK A" 
+  isSym_newK    "isSymKey (newK evs)"
 
 end