# HG changeset patch
# User paulson
# Date 850470178 -3600
# Node ID f5c61fd9b9b6faa83569bbffc4ae049527c333b6
# Parent  14539397fc04d64d86df735d4535bfaf58902b22
Temporary additions (random) for the nested Otway-Rees protocol
They will need to be rationalized

diff -r 14539397fc04 -r f5c61fd9b9b6 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Fri Dec 13 10:20:55 1996 +0100
+++ b/src/HOL/Auth/Shared.ML	Fri Dec 13 10:42:58 1996 +0100
@@ -26,19 +26,52 @@
 
 (*** Basic properties of shrK and newK ***)
 
+goalw thy [newN_def] "!!evs. newN evs = newN evt ==> length evs = length evt";
+by (fast_tac (!claset addSDs [inj_random RS injD]) 1);
+qed "newN_length";
+
+goalw thy [newK_def] "!!evs. newK evs = newK evt ==> length evs = length evt";
+by (fast_tac (!claset addSDs [inj_random RS injD]) 1);
+qed "newK_length";
+
+goalw thy [newK_def] "newK evs ~= shrK A";
+by (rtac random_neq_shrK 1);
+qed "newK_neq_shrK";
+
+goalw thy [newK_def] "isSymKey (newK evs)";
+by (rtac isSym_random 1);
+qed "isSym_newK";
+
 (* invKey (shrK A) = shrK A *)
 bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK);
 
+(* invKey (random x) = random x *)
+bind_thm ("invKey_random", rewrite_rule [isSymKey_def] isSym_random);
+
 (* invKey (newK evs) = newK evs *)
 bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
-Addsimps [invKey_shrK, invKey_newK];
+Addsimps [invKey_shrK, invKey_random, invKey_newK];
+
+goal thy "!!K. random x = invKey K ==> random x = K";
+by (rtac (invKey_eq RS iffD1) 1);
+by (Simp_tac 1);
+val random_invKey = result();
 
+AddSDs [random_invKey, sym RS random_invKey];
+
+goal thy "!!K. newK evs = invKey K ==> newK evs = K";
+by (rtac (invKey_eq RS iffD1) 1);
+by (Simp_tac 1);
+val newK_invKey = result();
+
+AddSDs [newK_invKey, sym RS newK_invKey];
 
 (*Injectiveness and freshness of new keys and nonces*)
-AddIffs [inj_shrK RS inj_eq];
+AddIffs [inj_shrK RS inj_eq, inj_random RS inj_eq];
 AddSDs  [newN_length, newK_length];
 
-Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
+Addsimps [random_neq_shrK, random_neq_shrK RS not_sym,
+	  newK_neq_shrK, newK_neq_shrK RS not_sym];
 
 (** Rewrites should not refer to  initState(Friend i) 
     -- not in normal form! **)
@@ -72,6 +105,12 @@
 qed "shrK_notin_image_newK";
 Addsimps [shrK_notin_image_newK];
 
+goal thy "shrK A ~: random``E";
+by (agent.induct_tac "A" 1);
+by (Auto_tac ());
+qed "shrK_notin_image_random";
+Addsimps [shrK_notin_image_random];
+
 
 (*** Function "sees" ***)
 
@@ -221,14 +260,6 @@
 (*Push newK applications in, allowing other keys to be pulled out*)
 val pushKey_newK = insComm thy "Key (newK ?evs)"  "Key (shrK ?C)";
 
-goal thy "!!K. newK evs = invKey K ==> newK evs = K";
-by (rtac (invKey_eq RS iffD1) 1);
-by (Simp_tac 1);
-val newK_invKey = result();
-
-AddSDs [newK_invKey];
-AddSDs [sym RS newK_invKey];
-
 Delsimps [image_insert];
 Addsimps [image_insert RS sym];
 
diff -r 14539397fc04 -r f5c61fd9b9b6 src/HOL/Auth/Shared.thy
--- 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