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.6  
     1.7 -Shared = Message + List + 
     1.8 +Shared = Message + List + Finite +
     1.9  
    1.10  consts
    1.11    shrK    :: agent => key  (*symmetric keys*)
    1.12  
    1.13  rules
    1.14 -  isSym_shrK "isSymKey (shrK A)"
    1.15 +  (*ALL keys are symmetric*)
    1.16 +  isSym_keys "isSymKey K"
    1.17  
    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.22  
    1.23  
    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.46  
    1.47    newK_neq_shrK   "newK i ~= shrK A" 
    1.48 -  isSym_newK      "isSymKey (newK i)"
    1.49  
    1.50  end