src/HOL/Auth/Shared.thy
changeset 3512 9dcb4daa15e8
parent 3472 fb3c38c88c08
child 3519 ab0a9fbed4c0
     1.1 --- a/src/HOL/Auth/Shared.thy	Wed Jul 09 17:00:34 1997 +0200
     1.2 +++ b/src/HOL/Auth/Shared.thy	Fri Jul 11 13:26:15 1997 +0200
     1.3 @@ -5,10 +5,10 @@
     1.4  
     1.5  Theory of Shared Keys (common to all symmetric-key protocols)
     1.6  
     1.7 -Server keys; initial states of agents; new nonces and keys; function "sees" 
     1.8 +Shared, long-term keys; initial states of agents
     1.9  *)
    1.10  
    1.11 -Shared = Message + List + Finite +
    1.12 +Shared = Event + Finite +
    1.13  
    1.14  consts
    1.15    shrK    :: agent => key  (*symmetric keys*)
    1.16 @@ -17,9 +17,6 @@
    1.17    isSym_keys "isSymKey K"	(*All keys are symmetric*)
    1.18    inj_shrK   "inj shrK"		(*No two agents have the same long-term key*)
    1.19  
    1.20 -consts  (*Initial states of agents -- parameter of the construction*)
    1.21 -  initState :: [agent set, agent] => msg set
    1.22 -
    1.23  primrec initState agent
    1.24          (*Server knows all long-term keys; other agents know only their own*)
    1.25    initState_Server  "initState lost Server     = Key `` range shrK"
    1.26 @@ -27,31 +24,6 @@
    1.27    initState_Spy     "initState lost Spy        = Key``shrK``lost"
    1.28  
    1.29  
    1.30 -datatype  (*Messages, and components of agent stores*)
    1.31 -  event = Says agent agent msg
    1.32 -
    1.33 -consts  
    1.34 -  sees1 :: [agent, event] => msg set
    1.35 -
    1.36 -primrec sees1 event
    1.37 -           (*Spy reads all traffic whether addressed to him or not*)
    1.38 -  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
    1.39 -
    1.40 -consts  
    1.41 -  sees :: [agent set, agent, event list] => msg set
    1.42 -
    1.43 -primrec sees list
    1.44 -  sees_Nil  "sees lost A []       = initState lost A"
    1.45 -  sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
    1.46 -
    1.47 -
    1.48 -constdefs
    1.49 -  (*Set of items that might be visible to somebody: complement of the set
    1.50 -        of fresh items*)
    1.51 -  used :: event list => msg set
    1.52 -    "used evs == parts (UN lost B. sees lost B evs)"
    1.53 -
    1.54 -
    1.55  rules
    1.56    (*Unlike the corresponding property of nonces, this cannot be proved.
    1.57      We have infinitely many agents and there is nothing to stop their