src/HOL/Auth/Shared.thy
changeset 2376 f5c61fd9b9b6
parent 2319 95f0d5243c85
child 2451 ce85a2aafc7a
--- a/src/HOL/Auth/Shared.thy	Fri Dec 13 10:20:55 1996 +0100
+++ b/src/HOL/Auth/Shared.thy	Fri Dec 13 10:42:58 1996 +0100
@@ -44,19 +44,24 @@
   sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
 
 
-(*Agents generate "random" nonces and keys.  These are uniquely determined by
-  the length of their argument, a trace.*)
+(*Agents generate "random" numbers for use as symmetric keys, as well as
+  nonces.*)
+
 consts
-  newN :: "event list => nat"
-  newK :: "event list => key"
+  random :: "nat*nat => nat"
+
+constdefs
+  newN   :: event list => nat
+  "newN evs == random (length evs, 0)"
+
+  newK   :: event list => nat
+  "newK evs == random (length evs, 1)"
 
 rules
-  inj_shrK      "inj shrK"
+  inj_shrK        "inj shrK"
+  inj_random      "inj random"
 
-  newN_length   "(newN evs = newN evt) ==> (length evs = length evt)"
-  newK_length   "(newK evs = newK evt) ==> (length evs = length evt)"
-
-  newK_neq_shrK "newK evs ~= shrK A" 
-  isSym_newK    "isSymKey (newK evs)"
+  random_neq_shrK "random ij ~= shrK A" 
+  isSym_random    "isSymKey (random ij)"
 
 end