# HG changeset patch
# User paulson
# Date 867746368 -7200
# Node ID fb3c38c88c08a1fe5b6c12cc22f3f1c10825a7ef
# Parent  cd37ec057028d5bc15015360b65df8d4a3623393
Deleted the obsolete operators newK, newN and nPair

diff -r cd37ec057028 -r fb3c38c88c08 src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Tue Jul 01 10:38:11 1997 +0200
+++ b/src/HOL/Auth/Shared.ML	Tue Jul 01 10:39:28 1997 +0200
@@ -5,7 +5,7 @@
 
 Theory of Shared Keys (common to all symmetric-key protocols)
 
-Server keys; initial states of agents; new nonces and keys; function "sees" 
+Server keys; initial states of agents; freshness; function "sees" 
 *)
 
 
@@ -24,36 +24,17 @@
   will not!*)
 Addsimps [o_def];
 
-(*** Basic properties of shrK and newK ***)
-
-(*Injectiveness and freshness of new keys and nonces*)
-AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, 
-         inj_newK RS inj_eq, inj_nPair RS inj_eq];
-
-(* invKey (shrK A) = shrK A *)
-bind_thm ("invKey_id", rewrite_rule [isSymKey_def] isSym_keys);
+(*** Basic properties of shrK ***)
 
-Addsimps [invKey_id];
+(*Injectiveness: Agents' long-term keys are distinct.*)
+AddIffs [inj_shrK RS inj_eq];
 
-goal thy "!!K. newK i = invKey K ==> newK i = K";
-by (rtac (invKey_eq RS iffD1) 1);
-by (Full_simp_tac 1);
-val newK_invKey = result();
-
-AddSDs [newK_invKey, sym RS newK_invKey];
-
-Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
+(* invKey(shrK A) = shrK A *)
+Addsimps [rewrite_rule [isSymKey_def] isSym_keys];
 
 (** Rewrites should not refer to  initState(Friend i) 
     -- not in normal form! **)
 
-goal thy "Key (newK i) ~: parts (initState lost B)";
-by (agent.induct_tac "B" 1);
-by (Auto_tac ());
-qed "newK_notin_initState";
-
-AddIffs [newK_notin_initState];
-
 goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
 by (agent.induct_tac "C" 1);
 by (Auto_tac ());
@@ -65,12 +46,6 @@
 qed "keysFor_image_Key";
 Addsimps [keysFor_image_Key];
 
-goal thy "shrK A ~: newK``E";
-by (agent.induct_tac "A" 1);
-by (Auto_tac ());
-qed "shrK_notin_image_newK";
-Addsimps [shrK_notin_image_newK];
-
 
 (*** Function "sees" ***)
 
@@ -371,10 +346,7 @@
                  |> standard;
 
 
-(*** Specialized rewriting for analz_insert_Key_newK ***)
-
-(*Push newK applications in, allowing other keys to be pulled out*)
-val pushKey_newK = insComm thy "Key (newK ?evs)"  "Key (shrK ?C)";
+(*** Specialized rewriting for analz_insert_freshK ***)
 
 goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
 by (Blast_tac 1);
diff -r cd37ec057028 -r fb3c38c88c08 src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Tue Jul 01 10:38:11 1997 +0200
+++ b/src/HOL/Auth/Shared.thy	Tue Jul 01 10:39:28 1997 +0200
@@ -14,8 +14,8 @@
   shrK    :: agent => key  (*symmetric keys*)
 
 rules
-  (*ALL keys are symmetric*)
-  isSym_keys "isSymKey K"
+  isSym_keys "isSymKey K"	(*All keys are symmetric*)
+  inj_shrK   "inj shrK"		(*No two agents have the same long-term key*)
 
 consts  (*Initial states of agents -- parameter of the construction*)
   initState :: [agent set, agent] => msg set
@@ -61,25 +61,4 @@
     an unspecified finite number.*)
   Key_supply_ax  "finite KK ==> 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
-	in one protocol round.  A typical candidate for npair(i,j) is
-	2^j(2i+1)
-*)
-
-consts
-  nPair :: "nat*nat => nat"
-  newN  :: "nat => nat"
-  newK  :: "nat => key"
-
-rules
-  inj_shrK        "inj shrK"
-  inj_nPair       "inj nPair"
-  inj_newN        "inj newN"
-  inj_newK        "inj newK"
-
-  newK_neq_shrK   "newK i ~= shrK A" 
-
 end