Deleted the obsolete operators newK, newN and nPair
authorpaulson
Tue Jul 01 10:39:28 1997 +0200 (1997-07-01)
changeset 3472fb3c38c88c08
parent 3471 cd37ec057028
child 3473 c2334f9532ab
Deleted the obsolete operators newK, newN and nPair
src/HOL/Auth/Shared.ML
src/HOL/Auth/Shared.thy
     1.1 --- a/src/HOL/Auth/Shared.ML	Tue Jul 01 10:38:11 1997 +0200
     1.2 +++ b/src/HOL/Auth/Shared.ML	Tue Jul 01 10:39:28 1997 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  Theory of Shared Keys (common to all symmetric-key protocols)
     1.6  
     1.7 -Server keys; initial states of agents; new nonces and keys; function "sees" 
     1.8 +Server keys; initial states of agents; freshness; function "sees" 
     1.9  *)
    1.10  
    1.11  
    1.12 @@ -24,36 +24,17 @@
    1.13    will not!*)
    1.14  Addsimps [o_def];
    1.15  
    1.16 -(*** Basic properties of shrK and newK ***)
    1.17 -
    1.18 -(*Injectiveness and freshness of new keys and nonces*)
    1.19 -AddIffs [inj_shrK RS inj_eq, inj_newN RS inj_eq, 
    1.20 -         inj_newK RS inj_eq, inj_nPair RS inj_eq];
    1.21 -
    1.22 -(* invKey (shrK A) = shrK A *)
    1.23 -bind_thm ("invKey_id", rewrite_rule [isSymKey_def] isSym_keys);
    1.24 +(*** Basic properties of shrK ***)
    1.25  
    1.26 -Addsimps [invKey_id];
    1.27 +(*Injectiveness: Agents' long-term keys are distinct.*)
    1.28 +AddIffs [inj_shrK RS inj_eq];
    1.29  
    1.30 -goal thy "!!K. newK i = invKey K ==> newK i = K";
    1.31 -by (rtac (invKey_eq RS iffD1) 1);
    1.32 -by (Full_simp_tac 1);
    1.33 -val newK_invKey = result();
    1.34 -
    1.35 -AddSDs [newK_invKey, sym RS newK_invKey];
    1.36 -
    1.37 -Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
    1.38 +(* invKey(shrK A) = shrK A *)
    1.39 +Addsimps [rewrite_rule [isSymKey_def] isSym_keys];
    1.40  
    1.41  (** Rewrites should not refer to  initState(Friend i) 
    1.42      -- not in normal form! **)
    1.43  
    1.44 -goal thy "Key (newK i) ~: parts (initState lost B)";
    1.45 -by (agent.induct_tac "B" 1);
    1.46 -by (Auto_tac ());
    1.47 -qed "newK_notin_initState";
    1.48 -
    1.49 -AddIffs [newK_notin_initState];
    1.50 -
    1.51  goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
    1.52  by (agent.induct_tac "C" 1);
    1.53  by (Auto_tac ());
    1.54 @@ -65,12 +46,6 @@
    1.55  qed "keysFor_image_Key";
    1.56  Addsimps [keysFor_image_Key];
    1.57  
    1.58 -goal thy "shrK A ~: newK``E";
    1.59 -by (agent.induct_tac "A" 1);
    1.60 -by (Auto_tac ());
    1.61 -qed "shrK_notin_image_newK";
    1.62 -Addsimps [shrK_notin_image_newK];
    1.63 -
    1.64  
    1.65  (*** Function "sees" ***)
    1.66  
    1.67 @@ -371,10 +346,7 @@
    1.68                   |> standard;
    1.69  
    1.70  
    1.71 -(*** Specialized rewriting for analz_insert_Key_newK ***)
    1.72 -
    1.73 -(*Push newK applications in, allowing other keys to be pulled out*)
    1.74 -val pushKey_newK = insComm thy "Key (newK ?evs)"  "Key (shrK ?C)";
    1.75 +(*** Specialized rewriting for analz_insert_freshK ***)
    1.76  
    1.77  goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
    1.78  by (Blast_tac 1);
     2.1 --- a/src/HOL/Auth/Shared.thy	Tue Jul 01 10:38:11 1997 +0200
     2.2 +++ b/src/HOL/Auth/Shared.thy	Tue Jul 01 10:39:28 1997 +0200
     2.3 @@ -14,8 +14,8 @@
     2.4    shrK    :: agent => key  (*symmetric keys*)
     2.5  
     2.6  rules
     2.7 -  (*ALL keys are symmetric*)
     2.8 -  isSym_keys "isSymKey K"
     2.9 +  isSym_keys "isSymKey K"	(*All keys are symmetric*)
    2.10 +  inj_shrK   "inj shrK"		(*No two agents have the same long-term key*)
    2.11  
    2.12  consts  (*Initial states of agents -- parameter of the construction*)
    2.13    initState :: [agent set, agent] => msg set
    2.14 @@ -61,25 +61,4 @@
    2.15      an unspecified finite number.*)
    2.16    Key_supply_ax  "finite KK ==> EX K. K ~: KK & Key K ~: used evs"
    2.17  
    2.18 -
    2.19 -(*Agents generate random (symmetric) keys and nonces.
    2.20 -  The numeric argument is typically the length of the current trace.
    2.21 -  An injective pairing function allows multiple keys/nonces to be generated
    2.22 -	in one protocol round.  A typical candidate for npair(i,j) is
    2.23 -	2^j(2i+1)
    2.24 -*)
    2.25 -
    2.26 -consts
    2.27 -  nPair :: "nat*nat => nat"
    2.28 -  newN  :: "nat => nat"
    2.29 -  newK  :: "nat => key"
    2.30 -
    2.31 -rules
    2.32 -  inj_shrK        "inj shrK"
    2.33 -  inj_nPair       "inj nPair"
    2.34 -  inj_newN        "inj newN"
    2.35 -  inj_newK        "inj newK"
    2.36 -
    2.37 -  newK_neq_shrK   "newK i ~= shrK A" 
    2.38 -
    2.39  end