Separation of theory Event into two parts:
authorpaulson
Wed Aug 21 13:25:27 1996 +0200 (1996-08-21)
changeset 193458573e7041b4
parent 1933 8b24773de6db
child 1935 ec67a0507c2a
Separation of theory Event into two parts:
Shared for general shared-key material
NS_Shared for the Needham-Schroeder shared-key protocol
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/Shared.ML
src/HOL/Auth/Shared.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Wed Aug 21 13:25:27 1996 +0200
     1.3 @@ -0,0 +1,497 @@
     1.4 +(*  Title:      HOL/Auth/NS_Shared
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Inductive relation "ns_shared" for Needham-Schroeder Shared-Key protocol.
    1.10 +
    1.11 +From page 247 of
    1.12 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    1.13 +  Proc. Royal Soc. 426 (1989)
    1.14 +*)
    1.15 +
    1.16 +open NS_Shared;
    1.17 +
    1.18 +(**** Inductive proofs about ns_shared ****)
    1.19 +
    1.20 +(*The Enemy can see more than anybody else, except for their initial state*)
    1.21 +goal thy 
    1.22 + "!!evs. evs : ns_shared ==> \
    1.23 +\     sees A evs <= initState A Un sees Enemy evs";
    1.24 +be ns_shared.induct 1;
    1.25 +by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    1.26 +			        addss (!simpset))));
    1.27 +qed "sees_agent_subset_sees_Enemy";
    1.28 +
    1.29 +
    1.30 +(*Nobody sends themselves messages*)
    1.31 +goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set_of_list evs";
    1.32 +be ns_shared.induct 1;
    1.33 +by (Auto_tac());
    1.34 +qed_spec_mp "not_Says_to_self";
    1.35 +Addsimps [not_Says_to_self];
    1.36 +AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    1.37 +
    1.38 +goal thy "!!evs. evs : ns_shared ==> Notes A X ~: set_of_list evs";
    1.39 +be ns_shared.induct 1;
    1.40 +by (Auto_tac());
    1.41 +qed "not_Notes";
    1.42 +Addsimps [not_Notes];
    1.43 +AddSEs   [not_Notes RSN (2, rev_notE)];
    1.44 +
    1.45 +
    1.46 +(*For reasoning about message NS3*)
    1.47 +goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \
    1.48 +\                X : parts (sees Enemy evs)";
    1.49 +by (fast_tac (!claset addSEs partsEs
    1.50 +	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    1.51 +qed "NS3_msg_in_parts_sees_Enemy";
    1.52 +			      
    1.53 +
    1.54 +(*** Server keys are not betrayed ***)
    1.55 +
    1.56 +(*Enemy never sees another agent's server key!*)
    1.57 +goal thy 
    1.58 + "!!evs. [| evs : ns_shared; A ~= Enemy |] ==> \
    1.59 +\        Key (serverKey A) ~: parts (sees Enemy evs)";
    1.60 +be ns_shared.induct 1;
    1.61 +bd NS3_msg_in_parts_sees_Enemy 5;
    1.62 +by (Auto_tac());
    1.63 +(*Deals with Fake message*)
    1.64 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.65 +			     impOfSubs synth_analz_parts_insert_subset_Un]) 1);
    1.66 +qed "Enemy_not_see_serverKey";
    1.67 +
    1.68 +bind_thm ("Enemy_not_analz_serverKey",
    1.69 +	  [analz_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD);
    1.70 +
    1.71 +Addsimps [Enemy_not_see_serverKey, 
    1.72 +	  not_sym RSN (2, Enemy_not_see_serverKey), 
    1.73 +	  Enemy_not_analz_serverKey, 
    1.74 +	  not_sym RSN (2, Enemy_not_analz_serverKey)];
    1.75 +
    1.76 +(*We go to some trouble to preserve R in the 3rd subgoal*)
    1.77 +val major::prems = 
    1.78 +goal thy  "[| Key (serverKey A) : parts (sees Enemy evs);    \
    1.79 +\             evs : ns_shared;                                  \
    1.80 +\             A=Enemy ==> R                                  \
    1.81 +\           |] ==> R";
    1.82 +br ccontr 1;
    1.83 +br ([major, Enemy_not_see_serverKey] MRS rev_notE) 1;
    1.84 +by (swap_res_tac prems 2);
    1.85 +by (ALLGOALS (fast_tac (!claset addIs prems)));
    1.86 +qed "Enemy_see_serverKey_E";
    1.87 +
    1.88 +bind_thm ("Enemy_analz_serverKey_E", 
    1.89 +	  analz_subset_parts RS subsetD RS Enemy_see_serverKey_E);
    1.90 +
    1.91 +(*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *)
    1.92 +AddSEs [Enemy_see_serverKey_E, Enemy_analz_serverKey_E];
    1.93 +
    1.94 +
    1.95 +(*No Friend will ever see another agent's server key 
    1.96 +  (excluding the Enemy, who might transmit his).
    1.97 +  The Server, of course, knows all server keys.*)
    1.98 +goal thy 
    1.99 + "!!evs. [| evs : ns_shared; A ~= Enemy;  A ~= Friend j |] ==> \
   1.100 +\        Key (serverKey A) ~: parts (sees (Friend j) evs)";
   1.101 +br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
   1.102 +by (ALLGOALS Asm_simp_tac);
   1.103 +qed "Friend_not_see_serverKey";
   1.104 +
   1.105 +
   1.106 +(*Not for Addsimps -- it can cause goals to blow up!*)
   1.107 +goal thy  
   1.108 + "!!evs. evs : ns_shared ==>                                  \
   1.109 +\        (Key (serverKey A) \
   1.110 +\           : analz (insert (Key (serverKey B)) (sees Enemy evs))) =  \
   1.111 +\        (A=B | A=Enemy)";
   1.112 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
   1.113 +		      addIs [impOfSubs (subset_insertI RS analz_mono)]
   1.114 +	              addss (!simpset)) 1);
   1.115 +qed "serverKey_mem_analz";
   1.116 +
   1.117 +
   1.118 +(*** Future keys can't be seen or used! ***)
   1.119 +
   1.120 +(*Nobody can have SEEN keys that will be generated in the future.
   1.121 +  This has to be proved anew for each protocol description,
   1.122 +  but should go by similar reasoning every time.  Hardest case is the
   1.123 +  standard Fake rule.  
   1.124 +      The length comparison, and Union over C, are essential for the 
   1.125 +  induction! *)
   1.126 +goal thy "!!evs. evs : ns_shared ==> \
   1.127 +\                length evs <= length evs' --> \
   1.128 +\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   1.129 +be ns_shared.induct 1;
   1.130 +bd NS3_msg_in_parts_sees_Enemy 5;
   1.131 +(*auto_tac does not work here, as it performs safe_tac first*)
   1.132 +by (ALLGOALS Asm_simp_tac);
   1.133 +by (ALLGOALS (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.134 +				       impOfSubs parts_insert_subset_Un,
   1.135 +				       Suc_leD]
   1.136 +			        addss (!simpset))));
   1.137 +val lemma = result();
   1.138 +
   1.139 +(*Variant needed for the main theorem below*)
   1.140 +goal thy 
   1.141 + "!!evs. [| evs : ns_shared;  length evs <= length evs' |] ==> \
   1.142 +\        Key (newK evs') ~: parts (sees C evs)";
   1.143 +by (fast_tac (!claset addDs [lemma]) 1);
   1.144 +qed "new_keys_not_seen";
   1.145 +Addsimps [new_keys_not_seen];
   1.146 +
   1.147 +(*Another variant: old messages must contain old keys!*)
   1.148 +goal thy 
   1.149 + "!!evs. [| Says A B X : set_of_list evs;  \
   1.150 +\           Key (newK evt) : parts {X};    \
   1.151 +\           evs : ns_shared                 \
   1.152 +\        |] ==> length evt < length evs";
   1.153 +br ccontr 1;
   1.154 +by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   1.155 +	              addIs [impOfSubs parts_mono, leI]) 1);
   1.156 +qed "Says_imp_old_keys";
   1.157 +
   1.158 +
   1.159 +(*Nobody can have USED keys that will be generated in the future.
   1.160 +  ...very like new_keys_not_seen*)
   1.161 +goal thy "!!evs. evs : ns_shared ==> \
   1.162 +\                length evs <= length evs' --> \
   1.163 +\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   1.164 +be ns_shared.induct 1;
   1.165 +bd NS3_msg_in_parts_sees_Enemy 5;
   1.166 +by (ALLGOALS Asm_simp_tac);
   1.167 +(*NS1 and NS2*)
   1.168 +map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2];
   1.169 +(*Fake and NS3*)
   1.170 +map (by o best_tac
   1.171 +     (!claset addSDs [newK_invKey]
   1.172 +	      addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.173 +		     impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.174 +		     Suc_leD]
   1.175 +	      addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
   1.176 +	      addss (!simpset)))
   1.177 +    [2,1];
   1.178 +(*NS4 and NS5: nonce exchange*)
   1.179 +by (ALLGOALS (deepen_tac (!claset addSDs [newK_invKey, Says_imp_old_keys]
   1.180 +	                          addIs  [less_SucI, impOfSubs keysFor_mono]
   1.181 +		                  addss (!simpset addsimps [le_def])) 0));
   1.182 +val lemma = result();
   1.183 +
   1.184 +goal thy 
   1.185 + "!!evs. [| evs : ns_shared;  length evs <= length evs' |] ==> \
   1.186 +\        newK evs' ~: keysFor (parts (sees C evs))";
   1.187 +by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   1.188 +qed "new_keys_not_used";
   1.189 +
   1.190 +bind_thm ("new_keys_not_analzd",
   1.191 +	  [analz_subset_parts RS keysFor_mono,
   1.192 +	   new_keys_not_used] MRS contra_subsetD);
   1.193 +
   1.194 +Addsimps [new_keys_not_used, new_keys_not_analzd];
   1.195 +
   1.196 +
   1.197 +(** Lemmas concerning the form of items passed in messages **)
   1.198 +
   1.199 +(*Describes the form *and age* of K, and the form of X,
   1.200 +  when the following message is sent*)
   1.201 +goal thy 
   1.202 + "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') : set_of_list evs; \
   1.203 +\           evs : ns_shared    \
   1.204 +\        |] ==> (EX evt:ns_shared. \
   1.205 +\                         K = Key(newK evt) & \
   1.206 +\                         X = (Crypt {|K, Agent A|} (serverKey B)) & \
   1.207 +\                         K' = serverKey A & \
   1.208 +\                         length evt < length evs)";
   1.209 +be rev_mp 1;
   1.210 +be ns_shared.induct 1;
   1.211 +by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   1.212 +qed "Says_Server_message_form";
   1.213 +
   1.214 +
   1.215 +(*Describes the form of X when the following message is sent*)
   1.216 +goal thy
   1.217 + "!!evs. evs : ns_shared ==>                             \
   1.218 +\        ALL A NA B K X.                            \
   1.219 +\            (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.220 +\            : parts (sees Enemy evs) & A ~= Enemy  -->   \
   1.221 +\          (EX evt:ns_shared. K = newK evt & \
   1.222 +\                          X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   1.223 +be ns_shared.induct 1;
   1.224 +bd NS3_msg_in_parts_sees_Enemy 5;
   1.225 +by (Step_tac 1);
   1.226 +by (ALLGOALS Asm_full_simp_tac);
   1.227 +(*Remaining cases are Fake and NS2*)
   1.228 +by (fast_tac (!claset addSDs [spec]) 2);
   1.229 +(*Now for the Fake case*)
   1.230 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.231 +			     impOfSubs synth_analz_parts_insert_subset_Un]
   1.232 +	              addss (!simpset)) 1);
   1.233 +qed_spec_mp "encrypted_form";
   1.234 +
   1.235 +
   1.236 +(*For eliminating the A ~= Enemy condition from the previous result*)
   1.237 +goal thy 
   1.238 + "!!evs. evs : ns_shared ==>                             \
   1.239 +\        ALL S A NA B K X.                            \
   1.240 +\            Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.241 +\            : set_of_list evs  -->   \
   1.242 +\        S = Server | S = Enemy";
   1.243 +be ns_shared.induct 1;
   1.244 +by (ALLGOALS Asm_simp_tac);
   1.245 +(*We are left with NS3*)
   1.246 +by (subgoal_tac "S = Server | S = Enemy" 1);
   1.247 +(*First justify this assumption!*)
   1.248 +by (fast_tac (!claset addSEs [allE, mp] addss (!simpset)) 2);
   1.249 +by (Step_tac 1);
   1.250 +bd Says_Server_message_form 1;
   1.251 +by (ALLGOALS Full_simp_tac);
   1.252 +(*Final case.  Clear out needless quantifiers to speed the following step*)
   1.253 +by (eres_inst_tac [("V","ALL x. ?P(x)")] thin_rl 1);
   1.254 +bd encrypted_form 1;
   1.255 +br (parts.Inj RS conjI) 1;
   1.256 +auto();
   1.257 +qed_spec_mp "Server_or_Enemy";
   1.258 +
   1.259 +
   1.260 +(*Describes the form of X when the following message is sent;
   1.261 +  use Says_Server_message_form if applicable*)
   1.262 +goal thy 
   1.263 + "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \
   1.264 +\            : set_of_list evs;                              \
   1.265 +\           evs : ns_shared               \
   1.266 +\        |] ==> (EX evt:ns_shared. K = newK evt & length evt < length evs & \
   1.267 +\                               X = (Crypt {|Key K, Agent A|} (serverKey B)))";
   1.268 +by (forward_tac [Server_or_Enemy] 1);
   1.269 +ba 1;
   1.270 +by (Step_tac 1);
   1.271 +by (fast_tac (!claset addSDs [Says_Server_message_form] addss (!simpset)) 1);
   1.272 +by (forward_tac [encrypted_form] 1);
   1.273 +br (parts.Inj RS conjI) 1;
   1.274 +by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset));
   1.275 +qed "Says_S_message_form";
   1.276 +
   1.277 +
   1.278 +
   1.279 +(****
   1.280 + The following is to prove theorems of the form
   1.281 +
   1.282 +          Key K : analz (insert (Key (newK evt)) 
   1.283 +	                   (insert (Key (serverKey C)) (sees Enemy evs))) ==>
   1.284 +          Key K : analz (insert (Key (serverKey C)) (sees Enemy evs))
   1.285 +
   1.286 + A more general formula must be proved inductively.
   1.287 +
   1.288 +****)
   1.289 +
   1.290 +
   1.291 +(*NOT useful in this form, but it says that session keys are not used
   1.292 +  to encrypt messages containing other keys, in the actual protocol.
   1.293 +  We require that agents should behave like this subsequently also.*)
   1.294 +goal thy 
   1.295 + "!!evs. evs : ns_shared ==> \
   1.296 +\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   1.297 +\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   1.298 +be ns_shared.induct 1;
   1.299 +bd NS3_msg_in_parts_sees_Enemy 5;
   1.300 +by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.301 +(*Deals with Faked messages*)
   1.302 +by (best_tac (!claset addSEs partsEs
   1.303 +		      addDs [impOfSubs analz_subset_parts,
   1.304 +                             impOfSubs parts_insert_subset_Un]
   1.305 +                      addss (!simpset)) 1);
   1.306 +(*NS4 and NS5*)
   1.307 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.308 +result();
   1.309 +
   1.310 +
   1.311 +(** Specialized rewriting for this proof **)
   1.312 +
   1.313 +Delsimps [image_insert];
   1.314 +Addsimps [image_insert RS sym];
   1.315 +
   1.316 +goal thy "insert (Key (newK x)) (sees A evs) = \
   1.317 +\         Key `` (newK``{x}) Un (sees A evs)";
   1.318 +by (Fast_tac 1);
   1.319 +val insert_Key_singleton = result();
   1.320 +
   1.321 +goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
   1.322 +\         Key `` (f `` (insert x E)) Un C";
   1.323 +by (Fast_tac 1);
   1.324 +val insert_Key_image = result();
   1.325 +
   1.326 +
   1.327 +(** Session keys are not used to encrypt other session keys **)
   1.328 +
   1.329 +goal thy  
   1.330 + "!!evs. evs : ns_shared ==> \
   1.331 +\  ALL K E. (Key K : analz (insert (Key (serverKey C)) \
   1.332 +\                             (Key``(newK``E) Un (sees Enemy evs)))) = \
   1.333 +\           (K : newK``E |  \
   1.334 +\            Key K : analz (insert (Key (serverKey C)) \
   1.335 +\                             (sees Enemy evs)))";
   1.336 +be ns_shared.induct 1;
   1.337 +by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   1.338 +by (REPEAT ((eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac) 5));
   1.339 +by (ALLGOALS 
   1.340 +    (asm_simp_tac 
   1.341 +     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.342 +			 @ pushes)
   1.343 +               setloop split_tac [expand_if])));
   1.344 +(*Cases NS2 and NS3!!  Simple, thanks to auto case splits*)
   1.345 +by (REPEAT (Fast_tac 3));
   1.346 +(*Base case*)
   1.347 +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   1.348 +(** LEVEL 7 **)
   1.349 +(*Fake case*)
   1.350 +by (REPEAT (Safe_step_tac 1));
   1.351 +by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 2);
   1.352 +by (subgoal_tac 
   1.353 +    "Key K : analz \
   1.354 +\             (synth \
   1.355 +\              (analz (insert (Key (serverKey C)) \
   1.356 +\                        (Key``(newK``E) Un (sees Enemy evsa)))))" 1);
   1.357 +(*First, justify this subgoal*)
   1.358 +(*Discard formulae for better speed*)
   1.359 +by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.360 +by (eres_inst_tac [("V","?Q ~: ?QQ")] thin_rl 2);
   1.361 +by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
   1.362 +                      addSEs [impOfSubs analz_mono]) 2);
   1.363 +by (Asm_full_simp_tac 1);
   1.364 +by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1);
   1.365 +qed_spec_mp "analz_image_newK";
   1.366 +
   1.367 +
   1.368 +goal thy
   1.369 + "!!evs. evs : ns_shared ==>                               \
   1.370 +\        Key K : analz (insert (Key (newK evt))            \
   1.371 +\                         (insert (Key (serverKey C))      \
   1.372 +\                          (sees Enemy evs))) =            \
   1.373 +\             (K = newK evt |                              \
   1.374 +\              Key K : analz (insert (Key (serverKey C))   \
   1.375 +\                               (sees Enemy evs)))";
   1.376 +by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.377 +				   insert_Key_singleton]) 1);
   1.378 +by (Fast_tac 1);
   1.379 +qed "analz_insert_Key_newK";
   1.380 +
   1.381 +
   1.382 +
   1.383 +(*This says that the Key, K, uniquely identifies the message.
   1.384 +    But if C=Enemy then he could send all sorts of nonsense.*)
   1.385 +goal thy 
   1.386 + "!!evs. evs : ns_shared ==>                      \
   1.387 +\      EX X'. ALL C S A Y N B X.               \
   1.388 +\         C ~= Enemy -->                       \
   1.389 +\         Says S A Y : set_of_list evs -->     \
   1.390 +\         ((Crypt {|N, Agent B, Key K, X|} (serverKey C)) : parts{Y} --> \
   1.391 +\       (X = X'))";
   1.392 +be ns_shared.induct 1;
   1.393 +by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);	
   1.394 +by (ALLGOALS 
   1.395 +    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   1.396 +(*NS2: Case split propagates some context to other subgoal...*)
   1.397 +by (excluded_middle_tac "K = newK evsa" 2);
   1.398 +by (Asm_simp_tac 2);
   1.399 +(*...we assume X is a very new message, and handle this case by contradiction*)
   1.400 +by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
   1.401 +		      addSEs partsEs
   1.402 +		      addEs [Says_imp_old_keys RS less_irrefl]
   1.403 +	              addss (!simpset)) 2);
   1.404 +(*NS3: No relevant messages*)
   1.405 +by (fast_tac (!claset addSEs [exI] addss (!simpset)) 2);
   1.406 +(*Fake*)
   1.407 +by (Step_tac 1);
   1.408 +br exI 1;
   1.409 +br conjI 1;
   1.410 +ba 2;
   1.411 +by (Step_tac 1);
   1.412 +(** LEVEL 12 **)
   1.413 +by (subgoal_tac "Crypt {|N, Agent Ba, Key K, Xa|} (serverKey C) \
   1.414 +\                  : parts (sees Enemy evsa)" 1);
   1.415 +by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2);
   1.416 +by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   1.417 +	              addDs [impOfSubs parts_insert_subset_Un]
   1.418 +                      addss (!simpset)) 2);
   1.419 +by (eres_inst_tac [("V","?aa : parts {X}")] thin_rl 1);
   1.420 +bd parts_singleton 1;
   1.421 +by (Step_tac 1);
   1.422 +bd seesD 1;
   1.423 +by (Step_tac 1);
   1.424 +by (Full_simp_tac 2);
   1.425 +by (fast_tac (!claset addSDs [spec]) 1);
   1.426 +val lemma = result();
   1.427 +
   1.428 +
   1.429 +(*In messages of this form, the session key uniquely identifies the rest*)
   1.430 +goal thy 
   1.431 + "!!evs. [| Says S A          \
   1.432 +\             (Crypt {|N, Agent B, Key K, X|} (serverKey C))     \
   1.433 +\                  : set_of_list evs; \
   1.434 + \          Says S' A'                                         \
   1.435 +\             (Crypt {|N', Agent B', Key K, X'|} (serverKey C')) \
   1.436 +\                  : set_of_list evs;                         \
   1.437 +\           evs : ns_shared;  C ~= Enemy;  C' ~= Enemy    |] ==> X = X'";
   1.438 +bd lemma 1;
   1.439 +be exE 1;
   1.440 +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   1.441 +by (Fast_tac 1);
   1.442 +qed "unique_session_keys";
   1.443 +
   1.444 +
   1.445 +
   1.446 +(*Crucial secrecy property: Enemy does not see the keys sent in msg NS2
   1.447 +   -- even if another key is compromised*)
   1.448 +goal thy 
   1.449 + "!!evs. [| Says Server (Friend i) \
   1.450 +\            (Crypt {|N, Agent(Friend j), K, X|} K') : set_of_list evs;  \
   1.451 +\           evs : ns_shared;  Friend i ~= C;  Friend j ~= C              \
   1.452 +\        |] ==>                                                       \
   1.453 +\     K ~: analz (insert (Key (serverKey C)) (sees Enemy evs))";
   1.454 +be rev_mp 1;
   1.455 +be ns_shared.induct 1;
   1.456 +by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.457 +(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   1.458 +by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   1.459 +by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
   1.460 +by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   1.461 +by (ALLGOALS 
   1.462 +    (asm_full_simp_tac 
   1.463 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.464 +			  analz_insert_Key_newK] @ pushes)
   1.465 +               setloop split_tac [expand_if])));
   1.466 +(*NS2*)
   1.467 +by (fast_tac (!claset addSEs [less_irrefl]) 2);
   1.468 +(** LEVEL 8 **)
   1.469 +(*Now for the Fake case*)
   1.470 +br notI 1;
   1.471 +by (subgoal_tac 
   1.472 +    "Key (newK evt) : \
   1.473 +\    analz (synth (analz (insert (Key (serverKey C)) \
   1.474 +\                                  (sees Enemy evsa))))" 1);
   1.475 +be (impOfSubs analz_mono) 2;
   1.476 +by (deepen_tac (!claset addIs [analz_mono RS synth_mono RSN (2,rev_subsetD),
   1.477 +			       impOfSubs synth_increasing,
   1.478 +			       impOfSubs analz_increasing]) 0 2);
   1.479 +(*Proves the Fake goal*)
   1.480 +by (fast_tac (!claset addss (!simpset)) 1);
   1.481 +
   1.482 +(**LEVEL 13**)
   1.483 +(*NS3: that message from the Server was sent earlier*)
   1.484 +by (mp_tac 1);
   1.485 +by (forward_tac [Says_S_message_form] 1 THEN assume_tac 1);
   1.486 +by (REPEAT_FIRST (eresolve_tac [bexE, conjE] ORELSE' hyp_subst_tac));
   1.487 +by (asm_full_simp_tac
   1.488 +    (!simpset addsimps (mem_if::analz_insert_Key_newK::pushes)) 1);
   1.489 +by (Step_tac 1);
   1.490 +(**LEVEL 18 **)
   1.491 +bd unique_session_keys 1;
   1.492 +by (REPEAT_FIRST assume_tac);
   1.493 +by (ALLGOALS Full_simp_tac);
   1.494 +by (Step_tac 1);
   1.495 +by (asm_full_simp_tac (!simpset addsimps [serverKey_mem_analz]) 1);
   1.496 +qed "Enemy_not_see_encrypted_key";
   1.497 +
   1.498 +
   1.499 +
   1.500 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Auth/NS_Shared.thy	Wed Aug 21 13:25:27 1996 +0200
     2.3 @@ -0,0 +1,67 @@
     2.4 +(*  Title:      HOL/Auth/NS_Shared
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1996  University of Cambridge
     2.8 +
     2.9 +Inductive relation "ns_shared" for Needham-Schroeder Shared-Key protocol.
    2.10 +
    2.11 +From page 247 of
    2.12 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    2.13 +  Proc. Royal Soc. 426 (1989)
    2.14 +*)
    2.15 +
    2.16 +NS_Shared = Shared + 
    2.17 +
    2.18 +consts  ns_shared   :: "event list set"
    2.19 +inductive ns_shared
    2.20 +  intrs 
    2.21 +         (*Initial trace is empty*)
    2.22 +    Nil  "[]: ns_shared"
    2.23 +
    2.24 +         (*The enemy MAY say anything he CAN say.  We do not expect him to
    2.25 +           invent new nonces here, but he can also use NS1.  Common to
    2.26 +           all similar protocols.*)
    2.27 +    Fake "[| evs: ns_shared;  B ~= Enemy;  X: synth (analz (sees Enemy evs))
    2.28 +          |] ==> (Says Enemy B X) # evs : ns_shared"
    2.29 +
    2.30 +         (*Alice initiates a protocol run*)
    2.31 +    NS1  "[| evs: ns_shared;  A ~= Server
    2.32 +          |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) 
    2.33 +                 # evs : ns_shared"
    2.34 +
    2.35 +         (*Server's response to Alice's message.
    2.36 +           !! It may respond more than once to A's request !!
    2.37 +	   Server doesn't know who the true sender is, hence the A' in
    2.38 +               the sender field.*)
    2.39 +    NS2  "[| evs: ns_shared;  A ~= B;  A ~= Server;
    2.40 +             (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    2.41 +          |] ==> (Says Server A 
    2.42 +                  (Crypt {|Nonce NA, Agent B, Key (newK evs),   
    2.43 +                           (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
    2.44 +                   (serverKey A))) # evs : ns_shared"
    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: ns_shared;  A ~= B;
    2.50 +             (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
    2.51 +               : set_of_list evs;
    2.52 +             A = Friend i;
    2.53 +             (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    2.54 +          |] ==> (Says A B X) # evs : ns_shared"
    2.55 +
    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: ns_shared;  A ~= B;  
    2.59 +             (Says A' B (Crypt {|Key K, Agent A|} (serverKey B))) 
    2.60 +               : set_of_list evs
    2.61 +          |] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : ns_shared"
    2.62 +
    2.63 +         (*Alice responds with (Suc N), if she has seen the key before.*)
    2.64 +    NS5  "[| evs: ns_shared;  A ~= B;  
    2.65 +             (Says B' A (Crypt (Nonce N) K)) : set_of_list evs;
    2.66 +             (Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
    2.67 +               : set_of_list evs
    2.68 +          |] ==> (Says A B (Crypt (Nonce (Suc N)) K)) # evs : ns_shared"
    2.69 +
    2.70 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Auth/Shared.ML	Wed Aug 21 13:25:27 1996 +0200
     3.3 @@ -0,0 +1,216 @@
     3.4 +(*  Title:      HOL/Auth/Message
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1996  University of Cambridge
     3.8 +
     3.9 +Theory of Shared Keys (common to all symmetric-key protocols)
    3.10 +
    3.11 +Server keys; initial states of agents; new nonces and keys; function "sees" 
    3.12 +
    3.13 +
    3.14 +*)
    3.15 +
    3.16 +Addsimps [parts_cut_eq];
    3.17 +
    3.18 +proof_timing:=true;
    3.19 +
    3.20 +(*IN SET.ML*)
    3.21 +goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
    3.22 +by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    3.23 +qed "mem_if";
    3.24 +
    3.25 +(*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
    3.26 +goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
    3.27 +by (fast_tac (!claset addEs [equalityE]) 1);
    3.28 +val subset_range_iff = result();
    3.29 +
    3.30 +
    3.31 +open Shared;
    3.32 +
    3.33 +Addsimps [Un_insert_left, Un_insert_right];
    3.34 +
    3.35 +(*By default only o_apply is built-in.  But in the presence of eta-expansion
    3.36 +  this means that some terms displayed as (f o g) will be rewritten, and others
    3.37 +  will not!*)
    3.38 +Addsimps [o_def];
    3.39 +
    3.40 +(*** Basic properties of serverKey and newK ***)
    3.41 +
    3.42 +(* invKey (serverKey A) = serverKey A *)
    3.43 +bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey);
    3.44 +
    3.45 +(* invKey (newK evs) = newK evs *)
    3.46 +bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
    3.47 +Addsimps [invKey_serverKey, invKey_newK];
    3.48 +
    3.49 +
    3.50 +(*New keys and nonces are fresh*)
    3.51 +val serverKey_inject = inj_serverKey RS injD;
    3.52 +val newN_inject = inj_newN RS injD
    3.53 +and newK_inject = inj_newK RS injD;
    3.54 +AddSEs [serverKey_inject, newN_inject, newK_inject,
    3.55 +	fresh_newK RS notE, fresh_newN RS notE];
    3.56 +Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
    3.57 +Addsimps [fresh_newN, fresh_newK];
    3.58 +
    3.59 +(** Rewrites should not refer to  initState(Friend i) 
    3.60 +    -- not in normal form! **)
    3.61 +
    3.62 +goal thy "newK evs ~= serverKey B";
    3.63 +by (subgoal_tac "newK evs = serverKey B --> \
    3.64 +\                Key (newK evs) : parts (initState B)" 1);
    3.65 +by (Fast_tac 1);
    3.66 +by (agent.induct_tac "B" 1);
    3.67 +by (auto_tac (!claset addIs [range_eqI], !simpset));
    3.68 +qed "newK_neq_serverKey";
    3.69 +
    3.70 +Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym];
    3.71 +
    3.72 +(*Good for talking about Server's initial state*)
    3.73 +goal thy "!!H. H <= Key``E ==> parts H = H";
    3.74 +by (Auto_tac ());
    3.75 +be parts.induct 1;
    3.76 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    3.77 +qed "parts_image_subset";
    3.78 +
    3.79 +bind_thm ("parts_image_Key", subset_refl RS parts_image_subset);
    3.80 +
    3.81 +goal thy "!!H. H <= Key``E ==> analz H = H";
    3.82 +by (Auto_tac ());
    3.83 +be analz.induct 1;
    3.84 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    3.85 +qed "analz_image_subset";
    3.86 +
    3.87 +bind_thm ("analz_image_Key", subset_refl RS analz_image_subset);
    3.88 +
    3.89 +Addsimps [parts_image_Key, analz_image_Key];
    3.90 +
    3.91 +goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
    3.92 +by (agent.induct_tac "C" 1);
    3.93 +by (auto_tac (!claset addIs [range_eqI] delrules partsEs, !simpset));
    3.94 +qed "keysFor_parts_initState";
    3.95 +Addsimps [keysFor_parts_initState];
    3.96 +
    3.97 +goalw thy [keysFor_def] "keysFor (Key``E) = {}";
    3.98 +by (Auto_tac ());
    3.99 +qed "keysFor_image_Key";
   3.100 +Addsimps [keysFor_image_Key];
   3.101 +
   3.102 +goal thy "serverKey A ~: newK``E";
   3.103 +by (agent.induct_tac "A" 1);
   3.104 +by (Auto_tac ());
   3.105 +qed "serverKey_notin_image_newK";
   3.106 +Addsimps [serverKey_notin_image_newK];
   3.107 +
   3.108 +
   3.109 +(*Agents see their own serverKeys!*)
   3.110 +goal thy "Key (serverKey A) : analz (sees A evs)";
   3.111 +by (list.induct_tac "evs" 1);
   3.112 +by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2);
   3.113 +by (agent.induct_tac "A" 1);
   3.114 +by (auto_tac (!claset addIs [range_eqI], !simpset));
   3.115 +qed "analz_own_serverKey";
   3.116 +
   3.117 +bind_thm ("parts_own_serverKey",
   3.118 +	  [analz_subset_parts, analz_own_serverKey] MRS subsetD);
   3.119 +
   3.120 +Addsimps [analz_own_serverKey, parts_own_serverKey];
   3.121 +
   3.122 +
   3.123 +
   3.124 +(** Specialized rewrite rules for (sees A (Says...#evs)) **)
   3.125 +
   3.126 +goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";
   3.127 +by (Simp_tac 1);
   3.128 +qed "sees_own";
   3.129 +
   3.130 +goal thy "!!A. Server ~= A ==> \
   3.131 +\              sees Server (Says A B X # evs) = sees Server evs";
   3.132 +by (Asm_simp_tac 1);
   3.133 +qed "sees_Server";
   3.134 +
   3.135 +goal thy "!!A. Friend i ~= A ==> \
   3.136 +\              sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
   3.137 +by (Asm_simp_tac 1);
   3.138 +qed "sees_Friend";
   3.139 +
   3.140 +goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)";
   3.141 +by (Simp_tac 1);
   3.142 +qed "sees_Enemy";
   3.143 +
   3.144 +goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
   3.145 +by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   3.146 +by (Fast_tac 1);
   3.147 +qed "sees_Says_subset_insert";
   3.148 +
   3.149 +goal thy "sees A evs <= sees A (Says A' B X # evs)";
   3.150 +by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   3.151 +by (Fast_tac 1);
   3.152 +qed "sees_subset_sees_Says";
   3.153 +
   3.154 +(*Pushing Unions into parts; one of the A's equals B, and thus sees Y*)
   3.155 +goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
   3.156 +\         parts {Y} Un (UN A. parts (sees A evs))";
   3.157 +by (Step_tac 1);
   3.158 +be rev_mp 1;	(*for some reason, split_tac does not work on assumptions*)
   3.159 +val ss = (!simpset addsimps [parts_Un, sees_Cons] 
   3.160 +	           setloop split_tac [expand_if]);
   3.161 +by (ALLGOALS (fast_tac (!claset addss ss)));
   3.162 +qed "UN_parts_sees_Says";
   3.163 +
   3.164 +goal thy "Says A B X : set_of_list evs --> X : sees Enemy evs";
   3.165 +by (list.induct_tac "evs" 1);
   3.166 +by (Auto_tac ());
   3.167 +qed_spec_mp "Says_imp_sees_Enemy";
   3.168 +
   3.169 +Addsimps [Says_imp_sees_Enemy];
   3.170 +AddIs    [Says_imp_sees_Enemy];
   3.171 +
   3.172 +goal thy "initState C <= Key `` range serverKey";
   3.173 +by (agent.induct_tac "C" 1);
   3.174 +by (Auto_tac ());
   3.175 +qed "initState_subset";
   3.176 +
   3.177 +goal thy "X : sees C evs --> \
   3.178 +\          (EX A B. Says A B X : set_of_list evs) | \
   3.179 +\          (EX A. Notes A X : set_of_list evs) | \
   3.180 +\          (EX A. X = Key (serverKey A))";
   3.181 +by (list.induct_tac "evs" 1);
   3.182 +by (ALLGOALS Asm_simp_tac);
   3.183 +by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
   3.184 +br conjI 1;
   3.185 +by (Fast_tac 2);
   3.186 +by (event.induct_tac "a" 1);
   3.187 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if])));
   3.188 +by (ALLGOALS Fast_tac);
   3.189 +qed_spec_mp "seesD";
   3.190 +
   3.191 +
   3.192 +Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];
   3.193 +Delsimps [sees_Cons];	(**** NOTE REMOVAL -- laws above are cleaner ****)
   3.194 +
   3.195 +
   3.196 +goal thy "!!K. newK evs = invKey K ==> newK evs = K";
   3.197 +br (invKey_eq RS iffD1) 1;
   3.198 +by (Simp_tac 1);
   3.199 +val newK_invKey = result();
   3.200 +
   3.201 +
   3.202 +(** Rewrites to push in Key and Crypt messages, so that other messages can
   3.203 +    be pulled out using the analz_insert rules **)
   3.204 +
   3.205 +fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 
   3.206 +                      insert_commute;
   3.207 +
   3.208 +val pushKeys = map (insComm "Key ?K") 
   3.209 +                  ["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"];
   3.210 +
   3.211 +val pushCrypts = map (insComm "Crypt ?X ?K") 
   3.212 +                    ["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"];
   3.213 +
   3.214 +(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
   3.215 +val pushes = pushKeys@pushCrypts;
   3.216 +
   3.217 +val pushKey_newK = insComm "Key (newK ?evs)"  "Key (serverKey ?C)";
   3.218 +
   3.219 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Auth/Shared.thy	Wed Aug 21 13:25:27 1996 +0200
     4.3 @@ -0,0 +1,67 @@
     4.4 +(*  Title:      HOL/Auth/Shared
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1996  University of Cambridge
     4.8 +
     4.9 +Theory of Shared Keys (common to all symmetric-key protocols)
    4.10 +
    4.11 +Server keys; initial states of agents; new nonces and keys; function "sees" 
    4.12 +*)
    4.13 +
    4.14 +Shared = Message + List + 
    4.15 +
    4.16 +consts
    4.17 +  serverKey    :: agent => key  (*symmetric keys*)
    4.18 +
    4.19 +rules
    4.20 +  isSym_serverKey "isSymKey (serverKey A)"
    4.21 +
    4.22 +consts  (*Initial states of agents -- parameter of the construction*)
    4.23 +  initState :: agent => msg set
    4.24 +
    4.25 +primrec initState agent
    4.26 +        (*Server knows all keys; other agents know only their own*)
    4.27 +  initState_Server  "initState Server     = Key `` range serverKey"
    4.28 +  initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
    4.29 +  initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
    4.30 +
    4.31 +datatype  (*Messages, and components of agent stores*)
    4.32 +  event = Says agent agent msg
    4.33 +        | Notes agent msg
    4.34 +
    4.35 +consts  
    4.36 +  sees1 :: [agent, event] => msg set
    4.37 +
    4.38 +primrec sees1 event
    4.39 +           (*First agent recalls all that it says, but NOT everything
    4.40 +             that is sent to it; it must note such things if/when received*)
    4.41 +  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
    4.42 +          (*part of A's internal state*)
    4.43 +  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' then {X} else {})"
    4.44 +
    4.45 +consts  
    4.46 +  sees :: [agent, event list] => msg set
    4.47 +
    4.48 +primrec sees list
    4.49 +        (*Initial knowledge includes all public keys and own private key*)
    4.50 +  sees_Nil  "sees A []       = initState A"
    4.51 +  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
    4.52 +
    4.53 +
    4.54 +(*Agents generate "random" nonces.  Different traces always yield
    4.55 +  different nonces.  Same applies for keys.*)
    4.56 +consts
    4.57 +  newN :: "event list => nat"
    4.58 +  newK :: "event list => key"
    4.59 +
    4.60 +rules
    4.61 +  inj_serverKey "inj serverKey"
    4.62 +
    4.63 +  inj_newN   "inj newN"
    4.64 +  fresh_newN "Nonce (newN evs) ~: parts (initState B)" 
    4.65 +
    4.66 +  inj_newK   "inj newK"
    4.67 +  fresh_newK "Key (newK evs) ~: parts (initState B)" 
    4.68 +  isSym_newK "isSymKey (newK evs)"
    4.69 +
    4.70 +end