Renaming and simplification
authorpaulson
Tue Sep 03 17:54:39 1996 +0200 (1996-09-03)
changeset 19426c9c1a42a869
parent 1941 f97a6e5b6375
child 1943 20574dca5a3e
Renaming and simplification
src/HOL/Auth/Event.ML
src/HOL/Auth/Event.thy
     1.1 --- a/src/HOL/Auth/Event.ML	Tue Sep 03 16:43:31 1996 +0200
     1.2 +++ b/src/HOL/Auth/Event.ML	Tue Sep 03 17:54:39 1996 +0200
     1.3 @@ -28,16 +28,6 @@
     1.4  by (Asm_simp_tac 1);
     1.5  qed "set_of_list_eqI1";
     1.6  
     1.7 -goal List.thy "set_of_list l <= set_of_list (x#l)";
     1.8 -by (Simp_tac 1);
     1.9 -by (Fast_tac 1);
    1.10 -qed "set_of_list_subset_Cons";
    1.11 -
    1.12 -(*Not for Addsimps -- it can cause goals to blow up!*)
    1.13 -goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
    1.14 -by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    1.15 -qed "mem_if";
    1.16 -
    1.17  (*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
    1.18  goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
    1.19  by (fast_tac (!claset addEs [equalityE]) 1);
    1.20 @@ -53,34 +43,34 @@
    1.21    will not!*)
    1.22  Addsimps [o_def];
    1.23  
    1.24 -(*** Basic properties of serverKey and newK ***)
    1.25 +(*** Basic properties of shrK and newK ***)
    1.26  
    1.27 -(* invKey (serverKey A) = serverKey A *)
    1.28 -bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey);
    1.29 +(* invKey (shrK A) = shrK A *)
    1.30 +bind_thm ("invKey_shrK", rewrite_rule [isSymKey_def] isSym_shrK);
    1.31  
    1.32  (* invKey (newK evs) = newK evs *)
    1.33  bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
    1.34 -Addsimps [invKey_serverKey, invKey_newK];
    1.35 +Addsimps [invKey_shrK, invKey_newK];
    1.36  
    1.37  
    1.38  (*New keys and nonces are fresh*)
    1.39 -val serverKey_inject = inj_serverKey RS injD;
    1.40 +val shrK_inject = inj_shrK RS injD;
    1.41  val newN_inject = inj_newN RS injD
    1.42  and newK_inject = inj_newK RS injD;
    1.43 -AddSEs [serverKey_inject, newN_inject, newK_inject,
    1.44 +AddSEs [shrK_inject, newN_inject, newK_inject,
    1.45  	fresh_newK RS notE, fresh_newN RS notE];
    1.46 -Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
    1.47 +Addsimps [inj_shrK RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
    1.48  Addsimps [fresh_newN, fresh_newK];
    1.49  
    1.50 -goal thy "newK evs ~= serverKey B";
    1.51 -by (subgoal_tac "newK evs = serverKey B --> \
    1.52 +goal thy "newK evs ~= shrK B";
    1.53 +by (subgoal_tac "newK evs = shrK B --> \
    1.54  \                Key (newK evs) : parts (initState B)" 1);
    1.55  by (Fast_tac 1);
    1.56  by (agent.induct_tac "B" 1);
    1.57  by (auto_tac (!claset addIs [range_eqI], !simpset));
    1.58 -qed "newK_neq_serverKey";
    1.59 +qed "newK_neq_shrK";
    1.60  
    1.61 -Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym];
    1.62 +Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
    1.63  
    1.64  (*Good for talking about Server's initial state*)
    1.65  goal thy "!!H. H <= Key``E ==> parts H = H";
    1.66 @@ -112,25 +102,25 @@
    1.67  qed "keysFor_image_Key";
    1.68  Addsimps [keysFor_image_Key];
    1.69  
    1.70 -goal thy "serverKey A ~: newK``E";
    1.71 +goal thy "shrK A ~: newK``E";
    1.72  by (agent.induct_tac "A" 1);
    1.73  by (Auto_tac ());
    1.74 -qed "serverKey_notin_image_newK";
    1.75 -Addsimps [serverKey_notin_image_newK];
    1.76 +qed "shrK_notin_image_newK";
    1.77 +Addsimps [shrK_notin_image_newK];
    1.78  
    1.79  
    1.80 -(*Agents see their own serverKeys!*)
    1.81 -goal thy "Key (serverKey A) : analz (sees A evs)";
    1.82 +(*Agents see their own shrKs!*)
    1.83 +goal thy "Key (shrK A) : analz (sees A evs)";
    1.84  by (list.induct_tac "evs" 1);
    1.85  by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2);
    1.86  by (agent.induct_tac "A" 1);
    1.87  by (auto_tac (!claset addIs [range_eqI], !simpset));
    1.88 -qed "analz_own_serverKey";
    1.89 +qed "analz_own_shrK";
    1.90  
    1.91 -bind_thm ("parts_own_serverKey",
    1.92 -	  [analz_subset_parts, analz_own_serverKey] MRS subsetD);
    1.93 +bind_thm ("parts_own_shrK",
    1.94 +	  [analz_subset_parts, analz_own_shrK] MRS subsetD);
    1.95  
    1.96 -Addsimps [analz_own_serverKey, parts_own_serverKey];
    1.97 +Addsimps [analz_own_shrK, parts_own_shrK];
    1.98  
    1.99  
   1.100  
   1.101 @@ -202,7 +192,7 @@
   1.102  Addsimps [Says_imp_sees_Enemy];
   1.103  AddIs    [Says_imp_sees_Enemy];
   1.104  
   1.105 -goal thy "initState C <= Key `` range serverKey";
   1.106 +goal thy "initState C <= Key `` range shrK";
   1.107  by (agent.induct_tac "C" 1);
   1.108  by (Auto_tac ());
   1.109  qed "initState_subset";
   1.110 @@ -210,7 +200,7 @@
   1.111  goal thy "X : sees C evs --> \
   1.112  \          (EX A B. Says A B X : set_of_list evs) | \
   1.113  \          (EX A. Notes A X : set_of_list evs) | \
   1.114 -\          (EX A. X = Key (serverKey A))";
   1.115 +\          (EX A. X = Key (shrK A))";
   1.116  by (list.induct_tac "evs" 1);
   1.117  by (ALLGOALS Asm_simp_tac);
   1.118  by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
   1.119 @@ -266,40 +256,40 @@
   1.120  (*Enemy never sees another agent's server key!*)
   1.121  goal thy 
   1.122   "!!evs. [| evs : traces; A ~= Enemy |] ==> \
   1.123 -\        Key (serverKey A) ~: parts (sees Enemy evs)";
   1.124 +\        Key (shrK A) ~: parts (sees Enemy evs)";
   1.125  be traces.induct 1;
   1.126  bd NS3_msg_in_parts_sees_Enemy 5;
   1.127  by (Auto_tac());
   1.128  (*Deals with Fake message*)
   1.129  by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.130  			     impOfSubs synth_analz_parts_insert_subset_Un]) 1);
   1.131 -qed "Enemy_not_see_serverKey";
   1.132 +qed "Enemy_not_see_shrK";
   1.133  
   1.134 -bind_thm ("Enemy_not_analz_serverKey",
   1.135 -	  [analz_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
   1.136 +bind_thm ("Enemy_not_analz_shrK",
   1.137 +	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
   1.138  
   1.139 -Addsimps [Enemy_not_see_serverKey, 
   1.140 -	  not_sym RSN (2, Enemy_not_see_serverKey), 
   1.141 -	  Enemy_not_analz_serverKey, 
   1.142 -	  not_sym RSN (2, Enemy_not_analz_serverKey)];
   1.143 +Addsimps [Enemy_not_see_shrK, 
   1.144 +	  not_sym RSN (2, Enemy_not_see_shrK), 
   1.145 +	  Enemy_not_analz_shrK, 
   1.146 +	  not_sym RSN (2, Enemy_not_analz_shrK)];
   1.147  
   1.148  (*We go to some trouble to preserve R in the 3rd subgoal*)
   1.149  val major::prems = 
   1.150 -goal thy  "[| Key (serverKey A) : parts (sees Enemy evs);    \
   1.151 +goal thy  "[| Key (shrK A) : parts (sees Enemy evs);    \
   1.152  \             evs : traces;                                  \
   1.153  \             A=Enemy ==> R                                  \
   1.154  \           |] ==> R";
   1.155  br ccontr 1;
   1.156 -br ([major, Enemy_not_see_serverKey] MRS rev_notE) 1;
   1.157 +br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
   1.158  by (swap_res_tac prems 2);
   1.159  by (ALLGOALS (fast_tac (!claset addIs prems)));
   1.160 -qed "Enemy_see_serverKey_E";
   1.161 +qed "Enemy_see_shrK_E";
   1.162  
   1.163 -bind_thm ("Enemy_analz_serverKey_E", 
   1.164 -	  analz_subset_parts RS subsetD RS Enemy_see_serverKey_E);
   1.165 +bind_thm ("Enemy_analz_shrK_E", 
   1.166 +	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   1.167  
   1.168  (*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *)
   1.169 -AddSEs [Enemy_see_serverKey_E, Enemy_analz_serverKey_E];
   1.170 +AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   1.171  
   1.172  
   1.173  (*No Friend will ever see another agent's server key 
   1.174 @@ -307,22 +297,22 @@
   1.175    The Server, of course, knows all server keys.*)
   1.176  goal thy 
   1.177   "!!evs. [| evs : traces; A ~= Enemy;  A ~= Friend j |] ==> \
   1.178 -\        Key (serverKey A) ~: parts (sees (Friend j) evs)";
   1.179 +\        Key (shrK A) ~: parts (sees (Friend j) evs)";
   1.180  br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
   1.181  by (ALLGOALS Asm_simp_tac);
   1.182 -qed "Friend_not_see_serverKey";
   1.183 +qed "Friend_not_see_shrK";
   1.184  
   1.185  
   1.186  (*Not for Addsimps -- it can cause goals to blow up!*)
   1.187  goal thy  
   1.188   "!!evs. evs : traces ==>                                  \
   1.189 -\        (Key (serverKey A) \
   1.190 -\           : analz (insert (Key (serverKey B)) (sees Enemy evs))) =  \
   1.191 +\        (Key (shrK A) \
   1.192 +\           : analz (insert (Key (shrK B)) (sees Enemy evs))) =  \
   1.193  \        (A=B | A=Enemy)";
   1.194  by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
   1.195  		      addIs [impOfSubs (subset_insertI RS analz_mono)]
   1.196  	              addss (!simpset)) 1);
   1.197 -qed "serverKey_mem_analz";
   1.198 +qed "shrK_mem_analz";
   1.199  
   1.200  
   1.201  
   1.202 @@ -429,7 +419,7 @@
   1.203  (*Cannot be added with Addsimps -- we don't always want to re-order messages*)
   1.204  val pushes = pushKeys@pushCrypts;
   1.205  
   1.206 -val pushKey_newK = insComm "Key (newK ?evs)"  "Key (serverKey ?C)";
   1.207 +val pushKey_newK = insComm "Key (newK ?evs)"  "Key (shrK ?C)";
   1.208  
   1.209  
   1.210  (** Lemmas concerning the form of items passed in messages **)
   1.211 @@ -441,8 +431,8 @@
   1.212  \           evs : traces    \
   1.213  \        |] ==> (EX evt:traces. \
   1.214  \                         K = Key(newK evt) & \
   1.215 -\                         X = (Crypt {|K, Agent A|} (serverKey B)) & \
   1.216 -\                         K' = serverKey A & \
   1.217 +\                         X = (Crypt {|K, Agent A|} (shrK B)) & \
   1.218 +\                         K' = shrK A & \
   1.219  \                         length evt < length evs)";
   1.220  be rev_mp 1;
   1.221  be traces.induct 1;
   1.222 @@ -461,7 +451,7 @@
   1.223  \                 (Crypt {|N, Agent(Friend j), K, X|} K') # evs';  \
   1.224  \           evs : traces;  i~=k                                    \
   1.225  \        |] ==>                                                    \
   1.226 -\     K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
   1.227 +\     K ~: analz (insert (Key (shrK (Friend k))) (sees Enemy evs))";
   1.228  be rev_mp 1;
   1.229  be traces.induct 1;
   1.230  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.231 @@ -475,10 +465,10 @@
   1.232  goal thy
   1.233   "!!evs. evs : traces ==>                             \
   1.234  \        ALL A NA B K X.                            \
   1.235 -\            (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.236 +\            (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
   1.237  \            : parts (sees Enemy evs) & A ~= Enemy  -->   \
   1.238  \          (EX evt:traces. K = newK evt & \
   1.239 -\                          X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   1.240 +\                          X = (Crypt {|Key K, Agent A|} (shrK B)))";
   1.241  be traces.induct 1;
   1.242  bd NS3_msg_in_parts_sees_Enemy 5;
   1.243  by (Step_tac 1);
   1.244 @@ -496,7 +486,7 @@
   1.245  goal thy 
   1.246   "!!evs. evs : traces ==>                             \
   1.247  \        ALL S A NA B K X.                            \
   1.248 -\            Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.249 +\            Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
   1.250  \            : set_of_list evs  -->   \
   1.251  \        S = Server | S = Enemy";
   1.252  be traces.induct 1;
   1.253 @@ -519,11 +509,11 @@
   1.254  (*Describes the form of X when the following message is sent;
   1.255    use Says_Server_message_form if applicable*)
   1.256  goal thy 
   1.257 - "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.258 + "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) \
   1.259  \            : set_of_list evs;                              \
   1.260  \           evs : traces               \
   1.261  \        |] ==> (EX evt:traces. K = newK evt & length evt < length evs & \
   1.262 -\                               X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   1.263 +\                               X = (Crypt {|Key K, Agent A|} (shrK B)))";
   1.264  by (forward_tac [Server_or_Enemy] 1);
   1.265  ba 1;
   1.266  by (Step_tac 1);
   1.267 @@ -536,11 +526,11 @@
   1.268  (*Currently unused.  Needed only to reason about the VERY LAST message.*)
   1.269  goal thy 
   1.270   "!!evs. [| evs = Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}   \
   1.271 -\                           (serverKey A)) # evs';                  \
   1.272 +\                           (shrK A)) # evs';                  \
   1.273  \           evs : traces                                           \
   1.274  \        |] ==> (EX evt:traces. evs' : traces & length evt < length evs & \
   1.275  \                               K = newK evt & \
   1.276 -\                               X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   1.277 +\                               X = (Crypt {|Key K, Agent A|} (shrK B)))";
   1.278  by (forward_tac [traces_eq_ConsE] 1);
   1.279  by (dtac (set_of_list_eqI1 RS Says_S_message_form) 2);
   1.280  by (Auto_tac());	
   1.281 @@ -552,8 +542,8 @@
   1.282   The following is to prove theorems of the form
   1.283  
   1.284            Key K : analz (insert (Key (newK evt)) 
   1.285 -	                   (insert (Key (serverKey C)) (sees Enemy evs))) ==>
   1.286 -          Key K : analz (insert (Key (serverKey C)) (sees Enemy evs))
   1.287 +	                   (insert (Key (shrK C)) (sees Enemy evs))) ==>
   1.288 +          Key K : analz (insert (Key (shrK C)) (sees Enemy evs))
   1.289  
   1.290   A more general formula must be proved inductively.
   1.291  
   1.292 @@ -600,10 +590,10 @@
   1.293  
   1.294  goal thy  
   1.295   "!!evs. evs : traces ==> \
   1.296 -\  ALL K E. (Key K : analz (insert (Key (serverKey C)) \
   1.297 +\  ALL K E. (Key K : analz (insert (Key (shrK C)) \
   1.298  \                             (Key``(newK``E) Un (sees Enemy evs)))) = \
   1.299  \           (K : newK``E |  \
   1.300 -\            Key K : analz (insert (Key (serverKey C)) \
   1.301 +\            Key K : analz (insert (Key (shrK C)) \
   1.302  \                             (sees Enemy evs)))";
   1.303  be traces.induct 1;
   1.304  by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   1.305 @@ -624,7 +614,7 @@
   1.306  by (subgoal_tac 
   1.307      "Key K : analz \
   1.308  \             (synth \
   1.309 -\              (analz (insert (Key (serverKey C)) \
   1.310 +\              (analz (insert (Key (shrK C)) \
   1.311  \                        (Key``(newK``E) Un (sees Enemy evsa)))))" 1);
   1.312  (*First, justify this subgoal*)
   1.313  (*Discard formulae for better speed*)
   1.314 @@ -640,10 +630,10 @@
   1.315  goal thy  
   1.316   "!!evs. evs : traces ==>                                  \
   1.317  \        Key K : analz (insert (Key (newK evt))            \
   1.318 -\                         (insert (Key (serverKey C))      \
   1.319 +\                         (insert (Key (shrK C))      \
   1.320  \                          (sees Enemy evs))) =            \
   1.321  \             (K = newK evt |                              \
   1.322 -\              Key K : analz (insert (Key (serverKey C))   \
   1.323 +\              Key K : analz (insert (Key (shrK C))   \
   1.324  \                               (sees Enemy evs)))";
   1.325  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.326  				   insert_Key_singleton]) 1);
   1.327 @@ -659,7 +649,7 @@
   1.328  \      EX X'. ALL C S A Y N B X.               \
   1.329  \         C ~= Enemy -->                       \
   1.330  \         Says S A Y : set_of_list evs -->     \
   1.331 -\         ((Crypt {|N, Agent B, Key K, X|} (serverKey C)) : parts{Y} --> \
   1.332 +\         ((Crypt {|N, Agent B, Key K, X|} (shrK C)) : parts{Y} --> \
   1.333  \       (X = X'))";
   1.334  be traces.induct 1;
   1.335  by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   1.336 @@ -682,7 +672,7 @@
   1.337  ba 2;
   1.338  by (Step_tac 1);
   1.339  (** LEVEL 12 **)
   1.340 -by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (serverKey C) \
   1.341 +by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (shrK C) \
   1.342  \                  : parts (sees Enemy evsa)" 1);
   1.343  by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.344  by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   1.345 @@ -701,10 +691,10 @@
   1.346  (*In messages of this form, the session key uniquely identifies the rest*)
   1.347  goal thy 
   1.348   "!!evs. [| Says S A          \
   1.349 -\             (Crypt {|N, Agent B, Key K, X|} (serverKey C))     \
   1.350 +\             (Crypt {|N, Agent B, Key K, X|} (shrK C))     \
   1.351  \                  : set_of_list evs; \
   1.352   \          Says S' A'                                         \
   1.353 -\             (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) \
   1.354 +\             (Crypt {|N', Agent B', Key K, X'|} (shrK C')) \
   1.355  \                  : set_of_list evs;                         \
   1.356  \           evs : traces;  C ~= Enemy;  C' ~= Enemy    |] ==> X = X'";
   1.357  bd lemma 1;
   1.358 @@ -722,7 +712,7 @@
   1.359  \            (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs;  \
   1.360  \           evs : traces;  Friend i ~= C;  Friend j ~= C              \
   1.361  \        |] ==>                                                       \
   1.362 -\     K ~: analz (insert (Key (serverKey C)) (sees Enemy evs))";
   1.363 +\     K ~: analz (insert (Key (shrK C)) (sees Enemy evs))";
   1.364  be rev_mp 1;
   1.365  be traces.induct 1;
   1.366  by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.367 @@ -742,7 +732,7 @@
   1.368  br notI 1;
   1.369  by (subgoal_tac 
   1.370      "Key (newK evt) : \
   1.371 -\    analz (synth (analz (insert (Key (serverKey C)) \
   1.372 +\    analz (synth (analz (insert (Key (shrK C)) \
   1.373  \                                  (sees Enemy evsa))))" 1);
   1.374  be (impOfSubs analz_mono) 2;
   1.375  by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD),
   1.376 @@ -764,7 +754,7 @@
   1.377  by (REPEAT_FIRST assume_tac);
   1.378  by (ALLGOALS Full_simp_tac);
   1.379  by (Step_tac 1);
   1.380 -by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analz]) 1);
   1.381 +by (asm_full_simp_tac (!simpset addsimps [shrK_mem_analz]) 1);
   1.382  qed "Enemy_not_see_encrypted_key";
   1.383  
   1.384  
   1.385 @@ -827,7 +817,7 @@
   1.386  \                 (Crypt {|N, Agent(Friend j), K, X|} K') # evs';  \
   1.387  \           evs : traces;  i~=k                                    \
   1.388  \        |] ==>                                                    \
   1.389 -\     K ~: analz (insert (Key (serverKey (Friend k))) (sees Enemy evs))";
   1.390 +\     K ~: analz (insert (Key (shrK (Friend k))) (sees Enemy evs))";
   1.391  be rev_mp 1;
   1.392  be traces.induct 1;
   1.393  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps pushes)));
   1.394 @@ -846,11 +836,11 @@
   1.395    same thing.*)
   1.396  goal thy 
   1.397   "!!evs. [| evs : traces; A ~= Enemy;  A ~= Friend j |] ==> \
   1.398 -\        Key (serverKey A) ~:                               \
   1.399 -\          analz (insert (Key (serverKey (Friend j))) (sees Enemy evs))";
   1.400 +\        Key (shrK A) ~:                               \
   1.401 +\          analz (insert (Key (shrK (Friend j))) (sees Enemy evs))";
   1.402  br (analz_subset_parts RS contra_subsetD) 1;
   1.403  by (Asm_simp_tac 1);
   1.404 -qed "insert_not_analz_serverKey";
   1.405 +qed "insert_not_analz_shrK";
   1.406  
   1.407  
   1.408  
   1.409 @@ -868,10 +858,10 @@
   1.410    that Friend or the Server originally sent it.*)
   1.411  goal thy 
   1.412   "!!evs. evs : traces ==>                             \
   1.413 -\    ALL A B X i. Says A B (Crypt X (serverKey (Friend i))) \
   1.414 +\    ALL A B X i. Says A B (Crypt X (shrK (Friend i))) \
   1.415  \        : set_of_list evs  -->   \
   1.416 -\    (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : set_of_list evs | \
   1.417 -\            Says (Friend i) B' (Crypt X (serverKey (Friend i))) : set_of_list evs)";
   1.418 +\    (EX B'. Says Server B' (Crypt X (shrK (Friend i))) : set_of_list evs | \
   1.419 +\            Says (Friend i) B' (Crypt X (shrK (Friend i))) : set_of_list evs)";
   1.420  be traces.induct 1;
   1.421  by (Step_tac 1);
   1.422  by (ALLGOALS Asm_full_simp_tac);
   1.423 @@ -894,7 +884,7 @@
   1.424  
   1.425  (*The NS3 case needs the induction hypothesis twice!
   1.426      One application is to the X component of the most recent message.*)
   1.427 -by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 2);
   1.428 +by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (shrK B)" 2);
   1.429  by (Fast_tac 3);
   1.430  by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
   1.431  be conjE 2;
     2.1 --- a/src/HOL/Auth/Event.thy	Tue Sep 03 16:43:31 1996 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Tue Sep 03 17:54:39 1996 +0200
     2.3 @@ -16,19 +16,19 @@
     2.4  
     2.5  consts
     2.6    publicKey    :: agent => key
     2.7 -  serverKey    :: agent => key  (*symmetric keys*)
     2.8 +  shrK    :: agent => key  (*symmetric keys*)
     2.9  
    2.10  rules
    2.11 -  isSym_serverKey "isSymKey (serverKey A)"
    2.12 +  isSym_shrK "isSymKey (shrK A)"
    2.13  
    2.14  consts  (*Initial states of agents -- parameter of the construction*)
    2.15    initState :: agent => msg set
    2.16  
    2.17  primrec initState agent
    2.18          (*Server knows all keys; other agents know only their own*)
    2.19 -  initState_Server  "initState Server     = Key `` range serverKey"
    2.20 -  initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
    2.21 -  initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
    2.22 +  initState_Server  "initState Server     = Key `` range shrK"
    2.23 +  initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
    2.24 +  initState_Enemy   "initState Enemy  = {Key (shrK Enemy)}"
    2.25  
    2.26  (**
    2.27  For asymmetric keys: server knows all public and private keys,
    2.28 @@ -72,7 +72,7 @@
    2.29    newK :: "event list => key"
    2.30  
    2.31  rules
    2.32 -  inj_serverKey "inj serverKey"
    2.33 +  inj_shrK "inj shrK"
    2.34  
    2.35    inj_newN   "inj(newN)"
    2.36    fresh_newN "Nonce (newN evs) ~: parts (initState B)" 
    2.37 @@ -108,14 +108,14 @@
    2.38               (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    2.39            |] ==> (Says Server A 
    2.40                    (Crypt {|Nonce NA, Agent B, Key (newK evs),   
    2.41 -                           (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
    2.42 -                   (serverKey A))) # evs : traces"
    2.43 +                           (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
    2.44 +                   (shrK A))) # evs : traces"
    2.45  
    2.46            (*We can't assume S=Server.  Agent A "remembers" her nonce.
    2.47              May assume WLOG that she is NOT the Enemy: the Fake rule
    2.48              covers this case.  Can inductively show A ~= Server*)
    2.49      NS3  "[| evs: traces;  A ~= B;
    2.50 -             (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
    2.51 +             (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))) 
    2.52                 : set_of_list evs;
    2.53               A = Friend i;
    2.54               (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    2.55 @@ -124,14 +124,14 @@
    2.56           (*Bob's nonce exchange.  He does not know who the message came
    2.57             from, but responds to A because she is mentioned inside.*)
    2.58      NS4  "[| evs: traces;  A ~= B;  
    2.59 -             (Says A' B (Crypt {|Key K, Agent A|} (serverKey B))) 
    2.60 +             (Says A' B (Crypt {|Key K, Agent A|} (shrK B))) 
    2.61                 : set_of_list evs
    2.62            |] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : traces"
    2.63  
    2.64           (*Alice responds with (Suc N), if she has seen the key before.*)
    2.65      NS5  "[| evs: traces;  A ~= B;  
    2.66               (Says B' A (Crypt (Nonce N) K)) : set_of_list evs;
    2.67 -             (Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
    2.68 +             (Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))) 
    2.69                 : set_of_list evs
    2.70            |] ==> (Says A B (Crypt (Nonce (Suc N)) K)) # evs : traces"
    2.71