src/HOL/Auth/Yahalom.ML
changeset 1985 84cf16192e03
child 1995 c80e58e78d9c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/Yahalom.ML	Thu Sep 12 10:40:05 1996 +0200
     1.3 @@ -0,0 +1,446 @@
     1.4 +(*  Title:      HOL/Auth/OtwayRees
     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 "otway" for the Yahalom protocol.
    1.10 +
    1.11 +From page 257 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 OtwayRees;
    1.17 +
    1.18 +proof_timing:=true;
    1.19 +HOL_quantifiers := false;
    1.20 +
    1.21 +(**** Inductive proofs about yahalom ****)
    1.22 +
    1.23 +(*The Enemy can see more than anybody else, except for their initial state*)
    1.24 +goal thy 
    1.25 + "!!evs. evs : yahalom ==> \
    1.26 +\     sees A evs <= initState A Un sees Enemy evs";
    1.27 +be yahalom.induct 1;
    1.28 +by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    1.29 +			        addss (!simpset))));
    1.30 +qed "sees_agent_subset_sees_Enemy";
    1.31 +
    1.32 +
    1.33 +(*Nobody sends themselves messages*)
    1.34 +goal thy "!!evs. evs : yahalom ==> ALL A X. Says A A X ~: set_of_list evs";
    1.35 +be yahalom.induct 1;
    1.36 +by (Auto_tac());
    1.37 +qed_spec_mp "not_Says_to_self";
    1.38 +Addsimps [not_Says_to_self];
    1.39 +AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    1.40 +
    1.41 +goal thy "!!evs. evs : yahalom ==> Notes A X ~: set_of_list evs";
    1.42 +be yahalom.induct 1;
    1.43 +by (Auto_tac());
    1.44 +qed "not_Notes";
    1.45 +Addsimps [not_Notes];
    1.46 +AddSEs   [not_Notes RSN (2, rev_notE)];
    1.47 +
    1.48 +
    1.49 +(** For reasoning about the encrypted portion of messages **)
    1.50 +
    1.51 +goal thy "!!evs. (Says A' B {|N, Agent A, Agent B, X|}) : set_of_list evs ==> \
    1.52 +\                X : analz (sees Enemy evs)";
    1.53 +by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    1.54 +qed "YM2_analz_sees_Enemy";
    1.55 +
    1.56 +goal thy "!!evs. (Says S B {|N, X, X'|}) : set_of_list evs ==> \
    1.57 +\                X : analz (sees Enemy evs)";
    1.58 +by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    1.59 +qed "YM4_analz_sees_Enemy";
    1.60 +
    1.61 +goal thy "!!evs. (Says B' A {|N, Crypt {|N,K|} K'|}) : set_of_list evs ==> \
    1.62 +\                K : parts (sees Enemy evs)";
    1.63 +by (fast_tac (!claset addSEs partsEs
    1.64 +	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    1.65 +qed "YM5_parts_sees_Enemy";
    1.66 +
    1.67 +(*YM2_analz... and YM4_analz... let us treat those cases using the same 
    1.68 +  argument as for the Fake case.  This is possible for most, but not all,
    1.69 +  proofs: Fake does not invent new nonces (as in YM2), and of course Fake
    1.70 +  messages originate from the Enemy. *)
    1.71 +
    1.72 +val YM2_YM4_tac = 
    1.73 +    dtac (YM2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
    1.74 +    dtac (YM4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6;
    1.75 +
    1.76 +
    1.77 +(*** Shared keys are not betrayed ***)
    1.78 +
    1.79 +(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
    1.80 +goal thy 
    1.81 + "!!evs. [| evs : yahalom;  A ~: bad |] ==> \
    1.82 +\        Key (shrK A) ~: parts (sees Enemy evs)";
    1.83 +be yahalom.induct 1;
    1.84 +by YM2_YM4_tac;
    1.85 +by (Auto_tac());
    1.86 +(*Deals with Fake message*)
    1.87 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.88 +			     impOfSubs Fake_parts_insert]) 1);
    1.89 +qed "Enemy_not_see_shrK";
    1.90 +
    1.91 +bind_thm ("Enemy_not_analz_shrK",
    1.92 +	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
    1.93 +
    1.94 +Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
    1.95 +
    1.96 +(*We go to some trouble to preserve R in the 3rd and 4th subgoals
    1.97 +  As usual fast_tac cannot be used because it uses the equalities too soon*)
    1.98 +val major::prems = 
    1.99 +goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
   1.100 +\             evs : yahalom;                                 \
   1.101 +\             A:bad ==> R                                  \
   1.102 +\           |] ==> R";
   1.103 +br ccontr 1;
   1.104 +br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
   1.105 +by (swap_res_tac prems 2);
   1.106 +by (ALLGOALS (fast_tac (!claset addIs prems)));
   1.107 +qed "Enemy_see_shrK_E";
   1.108 +
   1.109 +bind_thm ("Enemy_analz_shrK_E", 
   1.110 +	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   1.111 +
   1.112 +AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   1.113 +
   1.114 +
   1.115 +(*** Future keys can't be seen or used! ***)
   1.116 +
   1.117 +(*Nobody can have SEEN keys that will be generated in the future.
   1.118 +  This has to be proved anew for each protocol description,
   1.119 +  but should go by similar reasoning every time.  Hardest case is the
   1.120 +  standard Fake rule.  
   1.121 +      The length comparison, and Union over C, are essential for the 
   1.122 +  induction! *)
   1.123 +goal thy "!!evs. evs : yahalom ==> \
   1.124 +\                length evs <= length evs' --> \
   1.125 +\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   1.126 +be yahalom.induct 1;
   1.127 +by YM2_YM4_tac;
   1.128 +(*auto_tac does not work here, as it performs safe_tac first*)
   1.129 +by (ALLGOALS Asm_simp_tac);
   1.130 +by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.131 +				       impOfSubs parts_insert_subset_Un,
   1.132 +				       Suc_leD]
   1.133 +			        addss (!simpset))));
   1.134 +val lemma = result();
   1.135 +
   1.136 +(*Variant needed for the main theorem below*)
   1.137 +goal thy 
   1.138 + "!!evs. [| evs : yahalom;  length evs <= length evs' |] ==> \
   1.139 +\        Key (newK evs') ~: parts (sees C evs)";
   1.140 +by (fast_tac (!claset addDs [lemma]) 1);
   1.141 +qed "new_keys_not_seen";
   1.142 +Addsimps [new_keys_not_seen];
   1.143 +
   1.144 +(*Another variant: old messages must contain old keys!*)
   1.145 +goal thy 
   1.146 + "!!evs. [| Says A B X : set_of_list evs;  \
   1.147 +\           Key (newK evt) : parts {X};    \
   1.148 +\           evs : yahalom                 \
   1.149 +\        |] ==> length evt < length evs";
   1.150 +br ccontr 1;
   1.151 +by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   1.152 +	              addIs [impOfSubs parts_mono, leI]) 1);
   1.153 +qed "Says_imp_old_keys";
   1.154 +
   1.155 +
   1.156 +(*Nobody can have USED keys that will be generated in the future.
   1.157 +  ...very like new_keys_not_seen*)
   1.158 +goal thy "!!evs. evs : yahalom ==> \
   1.159 +\                length evs <= length evs' --> \
   1.160 +\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   1.161 +be yahalom.induct 1;
   1.162 +by YM2_YM4_tac;
   1.163 +bd YM5_parts_sees_Enemy 7;
   1.164 +by (ALLGOALS Asm_simp_tac);
   1.165 +(*YM1 and YM3*)
   1.166 +by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   1.167 +(*Fake, YM2, YM4: these messages send unknown (X) components*)
   1.168 +by (EVERY 
   1.169 +    (map
   1.170 +     (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 +     [3,2,1]));
   1.178 +(*YM5: dummy message*)
   1.179 +by (best_tac (!claset addSDs [newK_invKey]
   1.180 +		        addEs  [new_keys_not_seen RSN(2,rev_notE)]
   1.181 +			addIs  [less_SucI, impOfSubs keysFor_mono]
   1.182 +			addss (!simpset addsimps [le_def])) 1);
   1.183 +val lemma = result();
   1.184 +
   1.185 +goal thy 
   1.186 + "!!evs. [| evs : yahalom;  length evs <= length evs' |] ==> \
   1.187 +\        newK evs' ~: keysFor (parts (sees C evs))";
   1.188 +by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   1.189 +qed "new_keys_not_used";
   1.190 +
   1.191 +bind_thm ("new_keys_not_analzd",
   1.192 +	  [analz_subset_parts RS keysFor_mono,
   1.193 +	   new_keys_not_used] MRS contra_subsetD);
   1.194 +
   1.195 +Addsimps [new_keys_not_used, new_keys_not_analzd];
   1.196 +
   1.197 +
   1.198 +(** Lemmas concerning the form of items passed in messages **)
   1.199 +
   1.200 +
   1.201 +(****
   1.202 + The following is to prove theorems of the form
   1.203 +
   1.204 +          Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
   1.205 +          Key K : analz (sees Enemy evs)
   1.206 +
   1.207 + A more general formula must be proved inductively.
   1.208 +
   1.209 +****)
   1.210 +
   1.211 +
   1.212 +(*NOT useful in this form, but it says that session keys are not used
   1.213 +  to encrypt messages containing other keys, in the actual protocol.
   1.214 +  We require that agents should behave like this subsequently also.*)
   1.215 +goal thy 
   1.216 + "!!evs. evs : yahalom ==> \
   1.217 +\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   1.218 +\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   1.219 +be yahalom.induct 1;
   1.220 +by YM2_YM4_tac;
   1.221 +by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.222 +(*Deals with Faked messages*)
   1.223 +by (best_tac (!claset addSEs partsEs
   1.224 +		      addDs [impOfSubs analz_subset_parts,
   1.225 +                             impOfSubs parts_insert_subset_Un]
   1.226 +                      addss (!simpset)) 2);
   1.227 +(*Base case and YM5*)
   1.228 +by (Auto_tac());
   1.229 +result();
   1.230 +
   1.231 +
   1.232 +(** Specialized rewriting for this proof **)
   1.233 +
   1.234 +Delsimps [image_insert];
   1.235 +Addsimps [image_insert RS sym];
   1.236 +
   1.237 +Delsimps [image_Un];
   1.238 +Addsimps [image_Un RS sym];
   1.239 +
   1.240 +goal thy "insert (Key (newK x)) (sees A evs) = \
   1.241 +\         Key `` (newK``{x}) Un (sees A evs)";
   1.242 +by (Fast_tac 1);
   1.243 +val insert_Key_singleton = result();
   1.244 +
   1.245 +goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
   1.246 +\         Key `` (f `` (insert x E)) Un C";
   1.247 +by (Fast_tac 1);
   1.248 +val insert_Key_image = result();
   1.249 +
   1.250 +
   1.251 +(*This lets us avoid analyzing the new message -- unless we have to!*)
   1.252 +(*NEEDED??*)
   1.253 +goal thy "synth (analz (sees Enemy evs)) <=   \
   1.254 +\         synth (analz (sees Enemy (Says A B X # evs)))";
   1.255 +by (Simp_tac 1);
   1.256 +br (subset_insertI RS analz_mono RS synth_mono) 1;
   1.257 +qed "synth_analz_thin";
   1.258 +
   1.259 +AddIs [impOfSubs synth_analz_thin];
   1.260 +
   1.261 +
   1.262 +
   1.263 +(** Session keys are not used to encrypt other session keys **)
   1.264 +
   1.265 +(*Could generalize this so that the X component doesn't have to be first
   1.266 +  in the message?*)
   1.267 +val enemy_analz_tac =
   1.268 +  SELECT_GOAL 
   1.269 +   (EVERY [REPEAT (resolve_tac [impI,notI] 1),
   1.270 +	   dtac (impOfSubs Fake_analz_insert) 1,
   1.271 +	   eresolve_tac [asm_rl, synth.Inj] 1,
   1.272 +	   Fast_tac 1,
   1.273 +	   Asm_full_simp_tac 1,
   1.274 +	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
   1.275 +	   ]);
   1.276 +
   1.277 +
   1.278 +(*Lemma for the trivial direction of the if-and-only-if*)
   1.279 +goal thy  
   1.280 + "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
   1.281 +\         (K : nE | Key K : analz sEe)  ==>     \
   1.282 +\        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
   1.283 +by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
   1.284 +val lemma = result();
   1.285 +
   1.286 +
   1.287 +goal thy  
   1.288 + "!!evs. evs : yahalom ==> \
   1.289 +\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   1.290 +\           (K : newK``E | Key K : analz (sees Enemy evs))";
   1.291 +be yahalom.induct 1;
   1.292 +bd YM2_analz_sees_Enemy 4;
   1.293 +bd YM4_analz_sees_Enemy 6;
   1.294 +by (REPEAT_FIRST (resolve_tac [allI, lemma]));
   1.295 +by (ALLGOALS (*Takes 35 secs*)
   1.296 +    (asm_simp_tac 
   1.297 +     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.298 +			 @ pushes)
   1.299 +               setloop split_tac [expand_if])));
   1.300 +(*YM4*) 
   1.301 +by (enemy_analz_tac 5);
   1.302 +(*YM3*)
   1.303 +by (Fast_tac 4);
   1.304 +(*YM2*) (** LEVEL 7 **)
   1.305 +by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] 
   1.306 +    (insert_commute RS ssubst) 3);
   1.307 +by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   1.308 +    (insert_commute RS ssubst) 3);
   1.309 +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3);
   1.310 +by (enemy_analz_tac 3);
   1.311 +(*Fake case*) (** LEVEL 11 **)
   1.312 +by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] 
   1.313 +    (insert_commute RS ssubst) 2);
   1.314 +by (enemy_analz_tac 2);
   1.315 +(*Base case*)
   1.316 +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
   1.317 +qed_spec_mp "analz_image_newK";
   1.318 +
   1.319 +
   1.320 +goal thy
   1.321 + "!!evs. evs : yahalom ==>                               \
   1.322 +\        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   1.323 +\        (K = newK evt | Key K : analz (sees Enemy evs))";
   1.324 +by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.325 +				   insert_Key_singleton]) 1);
   1.326 +by (Fast_tac 1);
   1.327 +qed "analz_insert_Key_newK";
   1.328 +
   1.329 +
   1.330 +(*Describes the form *and age* of K when the following message is sent*)
   1.331 +goal thy 
   1.332 + "!!evs. [| Says Server B \
   1.333 +\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.334 +\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.335 +\           evs : yahalom |]                                        \
   1.336 +\        ==> (EX evt:yahalom. K = Key(newK evt) & \
   1.337 +\                           length evt < length evs) &            \
   1.338 +\            (EX i. NA = Nonce i)";
   1.339 +be rev_mp 1;
   1.340 +be yahalom.induct 1;
   1.341 +by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   1.342 +qed "Says_Server_message_form";
   1.343 +
   1.344 +
   1.345 +(*Crucial secrecy property: Enemy does not see the keys sent in msg YM3*)
   1.346 +goal thy 
   1.347 + "!!evs. [| Says Server A \
   1.348 +\            {|NA, Crypt {|NA, K|} (shrK B),                      \
   1.349 +\                  Crypt {|NB, K|} (shrK A)|} : set_of_list evs;  \
   1.350 +\           A ~: bad;  B ~: bad;  evs : yahalom |] ==>              \
   1.351 +\     K ~: analz (sees Enemy evs)";
   1.352 +be rev_mp 1;
   1.353 +be yahalom.induct 1;
   1.354 +bd YM2_analz_sees_Enemy 4;
   1.355 +bd YM4_analz_sees_Enemy 6;
   1.356 +by (ALLGOALS Asm_simp_tac);
   1.357 +(*Next 3 steps infer that K has the form "Key (newK evs'" ... *)
   1.358 +by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   1.359 +by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
   1.360 +by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac));
   1.361 +by (ALLGOALS
   1.362 +    (asm_full_simp_tac 
   1.363 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.364 +			  analz_insert_Key_newK] @ pushes)
   1.365 +               setloop split_tac [expand_if])));
   1.366 +(*YM3*)
   1.367 +by (fast_tac (!claset addSEs [less_irrefl]) 3);
   1.368 +(*Fake*) (** LEVEL 10 **)
   1.369 +by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
   1.370 +by (enemy_analz_tac 1);
   1.371 +(*YM4*)
   1.372 +by (mp_tac 2);
   1.373 +by (enemy_analz_tac 2);
   1.374 +(*YM2*)
   1.375 +by (mp_tac 1);
   1.376 +by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   1.377 +    (insert_commute RS ssubst) 1);
   1.378 +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   1.379 +by (enemy_analz_tac 1);
   1.380 +qed "Enemy_not_see_encrypted_key";
   1.381 +
   1.382 +
   1.383 +
   1.384 +(*** Session keys are issued at most once, and identify the principals ***)
   1.385 +
   1.386 +(** First, two lemmas for the Fake, YM2 and YM4 cases **)
   1.387 +
   1.388 +goal thy 
   1.389 + "!!evs. [| X : synth (analz (sees Enemy evs));                \
   1.390 +\           Crypt X' (shrK C) : parts{X};                      \
   1.391 +\           C ~: bad;  evs : yahalom |]  \
   1.392 +\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
   1.393 +by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   1.394 +	              addDs [impOfSubs parts_insert_subset_Un]
   1.395 +                      addss (!simpset)) 1);
   1.396 +qed "Crypt_Fake_parts";
   1.397 +
   1.398 +goal thy 
   1.399 + "!!evs. [| Crypt X' K : parts (sees A evs);  evs : yahalom |]  \
   1.400 +\        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
   1.401 +\            Crypt X' K : parts {Y}";
   1.402 +bd parts_singleton 1;
   1.403 +by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
   1.404 +qed "Crypt_parts_singleton";
   1.405 +
   1.406 +fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   1.407 +
   1.408 +(*The Key K uniquely identifies a pair of senders in the message encrypted by
   1.409 +  C, but if C=Enemy then he could send all sorts of nonsense.*)
   1.410 +goal thy 
   1.411 + "!!evs. evs : yahalom ==>                                     \
   1.412 +\      EX A B. ALL C.                                        \
   1.413 +\         C ~: bad -->                                       \
   1.414 +\         (ALL S S' X. Says S S' X : set_of_list evs -->     \
   1.415 +\           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
   1.416 +by (Simp_tac 1);
   1.417 +be yahalom.induct 1;
   1.418 +bd YM2_analz_sees_Enemy 4;
   1.419 +bd YM4_analz_sees_Enemy 6;
   1.420 +by (ALLGOALS 
   1.421 +    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   1.422 +by (REPEAT_FIRST (etac exE));
   1.423 +(*YM4*)
   1.424 +by (ex_strip_tac 4);
   1.425 +by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   1.426 +			      Crypt_parts_singleton]) 4);
   1.427 +(*YM3: Case split propagates some context to other subgoal...*)
   1.428 +	(** LEVEL 8 **)
   1.429 +by (excluded_middle_tac "K = newK evsa" 3);
   1.430 +by (Asm_simp_tac 3);
   1.431 +by (REPEAT (ares_tac [exI] 3));
   1.432 +(*...we prove this case by contradiction: the key is too new!*)
   1.433 +by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)]
   1.434 +		      addSEs partsEs
   1.435 +		      addEs [Says_imp_old_keys RS less_irrefl]
   1.436 +	              addss (!simpset)) 3);
   1.437 +(*YM2*) (** LEVEL 12 **)
   1.438 +by (ex_strip_tac 2);
   1.439 +by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   1.440 +    (insert_commute RS ssubst) 2);
   1.441 +by (Simp_tac 2);
   1.442 +by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   1.443 +			      Crypt_parts_singleton]) 2);
   1.444 +(*Fake*) (** LEVEL 16 **)
   1.445 +by (ex_strip_tac 1);
   1.446 +by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
   1.447 +qed "unique_session_keys";
   1.448 +
   1.449 +(*It seems strange but this theorem is NOT needed to prove the main result!*)