src/HOL/Auth/Shared.thy
changeset 2032 1bbf1bdcaf56
parent 2012 1b234f1fd9c7
child 2064 5a5e508e2a2b
     1.1 --- a/src/HOL/Auth/Shared.thy	Thu Sep 26 12:47:47 1996 +0200
     1.2 +++ b/src/HOL/Auth/Shared.thy	Thu Sep 26 12:50:48 1996 +0200
     1.3 @@ -12,22 +12,19 @@
     1.4  
     1.5  consts
     1.6    shrK    :: agent => key  (*symmetric keys*)
     1.7 -  leaked  :: nat set       (*Friendly agents whose keys have leaked to Enemy*)
     1.8 -
     1.9 -constdefs     (*Enemy and compromised agents*)
    1.10 -  bad     :: agent set     "bad == insert Enemy (Friend``leaked)"
    1.11  
    1.12  rules
    1.13    isSym_shrK "isSymKey (shrK A)"
    1.14  
    1.15  consts  (*Initial states of agents -- parameter of the construction*)
    1.16 -  initState :: agent => msg set
    1.17 +  initState :: [agent set, agent] => msg set
    1.18  
    1.19  primrec initState agent
    1.20          (*Server knows all keys; other agents know only their own*)
    1.21 -  initState_Server  "initState Server     = Key `` range shrK"
    1.22 -  initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
    1.23 -  initState_Enemy   "initState Enemy      = Key``shrK``bad"
    1.24 +  initState_Server  "initState lost Server     = Key `` range shrK"
    1.25 +  initState_Friend  "initState lost (Friend i) = {Key (shrK (Friend i))}"
    1.26 +  initState_Spy   "initState lost Spy      = Key``shrK``lost"
    1.27 +
    1.28  
    1.29  datatype  (*Messages, and components of agent stores*)
    1.30    event = Says agent agent msg
    1.31 @@ -38,16 +35,16 @@
    1.32  primrec sees1 event
    1.33             (*First agent recalls all that it says, but NOT everything
    1.34               that is sent to it; it must note such things if/when received*)
    1.35 -  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
    1.36 +  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Spy} then {X} else {})"
    1.37            (*part of A's internal state*)
    1.38  
    1.39  consts  
    1.40 -  sees :: [agent, event list] => msg set
    1.41 +  sees :: [agent set, agent, event list] => msg set
    1.42  
    1.43  primrec sees list
    1.44          (*Initial knowledge includes all public keys and own private key*)
    1.45 -  sees_Nil  "sees A []       = initState A"
    1.46 -  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
    1.47 +  sees_Nil  "sees lost A []       = initState lost A"
    1.48 +  sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
    1.49  
    1.50  
    1.51  (*Agents generate "random" nonces.  Different traces always yield
    1.52 @@ -57,13 +54,12 @@
    1.53    newK :: "event list => key"
    1.54  
    1.55  rules
    1.56 -  inj_shrK "inj shrK"
    1.57 +  inj_shrK      "inj shrK"
    1.58 +
    1.59 +  inj_newN      "inj newN"
    1.60  
    1.61 -  inj_newN   "inj newN"
    1.62 -  fresh_newN "Nonce (newN evs) ~: parts (initState B)" 
    1.63 -
    1.64 -  inj_newK   "inj newK"
    1.65 -  fresh_newK "Key (newK evs) ~: parts (initState B)" 
    1.66 -  isSym_newK "isSymKey (newK evs)"
    1.67 +  inj_newK      "inj newK"
    1.68 +  newK_neq_shrK "newK evs ~= shrK A" 
    1.69 +  isSym_newK    "isSymKey (newK evs)"
    1.70  
    1.71  end