src/HOL/Auth/Shared.thy
changeset 2451 ce85a2aafc7a
parent 2376 f5c61fd9b9b6
child 2516 4d68fbe6378b
--- a/src/HOL/Auth/Shared.thy	Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/Shared.thy	Thu Dec 19 11:58:39 1996 +0100
@@ -44,24 +44,25 @@
   sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
 
 
-(*Agents generate "random" numbers for use as symmetric keys, as well as
-  nonces.*)
+(*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
+	in one protocol round.  A typical candidate for npair(i,j) is
+	2^j(2i+1)
+*)
 
 consts
-  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)"
+  nPair :: "nat*nat => nat"
+  newN  :: "nat => nat"
+  newK  :: "nat => key"
 
 rules
   inj_shrK        "inj shrK"
-  inj_random      "inj random"
+  inj_nPair       "inj nPair"
+  inj_newN        "inj newN"
+  inj_newK        "inj newK"
 
-  random_neq_shrK "random ij ~= shrK A" 
-  isSym_random    "isSymKey (random ij)"
+  newK_neq_shrK   "newK i ~= shrK A" 
+  isSym_newK      "isSymKey (newK i)"
 
 end