src/HOL/Auth/Shared.thy
 changeset 2516 4d68fbe6378b parent 2451 ce85a2aafc7a child 3414 804c8a178a7f
1.1 --- a/src/HOL/Auth/Shared.thy	Fri Jan 17 11:50:09 1997 +0100
1.2 +++ b/src/HOL/Auth/Shared.thy	Fri Jan 17 12:49:31 1997 +0100
1.3 @@ -8,13 +8,14 @@
1.4  Server keys; initial states of agents; new nonces and keys; function "sees"
1.5  *)
1.7 -Shared = Message + List +
1.8 +Shared = Message + List + Finite +
1.10  consts
1.11    shrK    :: agent => key  (*symmetric keys*)
1.13  rules
1.14 -  isSym_shrK "isSymKey (shrK A)"
1.15 +  (*ALL keys are symmetric*)
1.16 +  isSym_keys "isSymKey K"
1.18  consts  (*Initial states of agents -- parameter of the construction*)
1.19    initState :: [agent set, agent] => msg set
1.20 @@ -44,6 +45,23 @@
1.21    sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
1.24 +constdefs
1.25 +  (*Set of items that might be visible to somebody: complement of the set
1.26 +        of fresh items*)
1.27 +  used :: event list => msg set
1.28 +    "used evs == parts (UN lost B. sees lost B evs)"
1.29 +
1.30 +
1.31 +rules
1.32 +  (*Unlike the corresponding property of nonces, this cannot be proved.
1.33 +    We have infinitely many agents and there is nothing to stop their
1.34 +    long-term keys from exhausting all the natural numbers.  The axiom
1.35 +    assumes that their keys are dispersed so as to leave room for infinitely
1.36 +    many fresh session keys.  We could, alternatively, restrict agents to
1.37 +    an unspecified finite number.*)
1.38 +  Key_supply_ax  "KK: Fin UNIV ==> EX K. K ~: KK & Key K ~: used evs"
1.39 +
1.40 +
1.41  (*Agents generate random (symmetric) keys and nonces.
1.42    The numeric argument is typically the length of the current trace.
1.43    An injective pairing function allows multiple keys/nonces to be generated
1.44 @@ -63,6 +81,5 @@
1.45    inj_newK        "inj newK"
1.47    newK_neq_shrK   "newK i ~= shrK A"
1.48 -  isSym_newK      "isSymKey (newK i)"
1.50  end