diff -r 6ff9bd353121 -r 4d68fbe6378b src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/Shared.thy	Fri Jan 17 12:49:31 1997 +0100
@@ -8,13 +8,14 @@
 Server keys; initial states of agents; new nonces and keys; function "sees" 
 *)
 
-Shared = Message + List + 
+Shared = Message + List + Finite +
 
 consts
   shrK    :: agent => key  (*symmetric keys*)
 
 rules
-  isSym_shrK "isSymKey (shrK A)"
+  (*ALL keys are symmetric*)
+  isSym_keys "isSymKey K"
 
 consts  (*Initial states of agents -- parameter of the construction*)
   initState :: [agent set, agent] => msg set
@@ -44,6 +45,23 @@
   sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
 
 
+constdefs
+  (*Set of items that might be visible to somebody: complement of the set
+        of fresh items*)
+  used :: event list => msg set
+    "used evs == parts (UN lost B. sees lost B evs)"
+
+
+rules
+  (*Unlike the corresponding property of nonces, this cannot be proved.
+    We have infinitely many agents and there is nothing to stop their
+    long-term keys from exhausting all the natural numbers.  The axiom
+    assumes that their keys are dispersed so as to leave room for infinitely
+    many fresh session keys.  We could, alternatively, restrict agents to
+    an unspecified finite number.*)
+  Key_supply_ax  "KK: Fin UNIV ==> EX K. K ~: KK & Key K ~: used evs"
+
+
 (*Agents generate random (symmetric) keys and nonces.
   The numeric argument is typically the length of the current trace.
   An injective pairing function allows multiple keys/nonces to be generated
@@ -63,6 +81,5 @@
   inj_newK        "inj newK"
 
   newK_neq_shrK   "newK i ~= shrK A" 
-  isSym_newK      "isSymKey (newK i)"
 
 end