Bad version of Otway-Rees and the new attack on it
authorpaulson
Mon Sep 23 17:41:57 1996 +0200 (1996-09-23)
changeset 2002ed423882c6a9
parent 2001 974167c1d2c4
child 2003 b48f066d52dc
Bad version of Otway-Rees and the new attack on it
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/OtwayRees_Bad.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Mon Sep 23 17:41:57 1996 +0200
     1.3 @@ -0,0 +1,668 @@
     1.4 +(*  Title:      HOL/Auth/OtwayRees_Bad
     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 Otway-Rees protocol.
    1.10 +
    1.11 +The FAULTY version omitting encryption of Nonce NB, as suggested on page 247 of
    1.12 +  Burrows, Abadi and Needham.  A Logic of Authentication.
    1.13 +  Proc. Royal Soc. 426 (1989)
    1.14 +
    1.15 +This file illustrates the consequences of such errors.  We can still prove
    1.16 +impressive-looking properties such as Enemy_not_see_encrypted_key, yet the
    1.17 +protocol is open to a middleperson attack.  Attempting to prove some key lemmas
    1.18 +indicates the possibility of this attack.
    1.19 +*)
    1.20 +
    1.21 +open OtwayRees_Bad;
    1.22 +
    1.23 +proof_timing:=true;
    1.24 +HOL_quantifiers := false;
    1.25 +
    1.26 +
    1.27 +(*Weak liveness: there are traces that reach the end*)
    1.28 +goal thy 
    1.29 + "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    1.30 +\        ==> EX K. EX NA. EX evs: otway.          \
    1.31 +\               Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
    1.32 +\                 : set_of_list evs";
    1.33 +by (REPEAT (resolve_tac [exI,bexI] 1));
    1.34 +br (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2;
    1.35 +by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    1.36 +by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    1.37 +by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    1.38 +result();
    1.39 +
    1.40 +
    1.41 +(**** Inductive proofs about otway ****)
    1.42 +
    1.43 +(*The Enemy can see more than anybody else, except for their initial state*)
    1.44 +goal thy 
    1.45 + "!!evs. evs : otway ==> \
    1.46 +\     sees A evs <= initState A Un sees Enemy evs";
    1.47 +be otway.induct 1;
    1.48 +by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    1.49 +			        addss (!simpset))));
    1.50 +qed "sees_agent_subset_sees_Enemy";
    1.51 +
    1.52 +
    1.53 +(*Nobody sends themselves messages*)
    1.54 +goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs";
    1.55 +be otway.induct 1;
    1.56 +by (Auto_tac());
    1.57 +qed_spec_mp "not_Says_to_self";
    1.58 +Addsimps [not_Says_to_self];
    1.59 +AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    1.60 +
    1.61 +
    1.62 +(** For reasoning about the encrypted portion of messages **)
    1.63 +
    1.64 +goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
    1.65 +\                X : analz (sees Enemy evs)";
    1.66 +by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    1.67 +qed "OR2_analz_sees_Enemy";
    1.68 +
    1.69 +goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \
    1.70 +\                X : analz (sees Enemy evs)";
    1.71 +by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    1.72 +qed "OR4_analz_sees_Enemy";
    1.73 +
    1.74 +goal thy "!!evs. Says B' A {|N, Crypt {|N,K|} K'|} : set_of_list evs ==> \
    1.75 +\                K : parts (sees Enemy evs)";
    1.76 +by (fast_tac (!claset addSEs partsEs
    1.77 +	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    1.78 +qed "Reveal_parts_sees_Enemy";
    1.79 +
    1.80 +(*OR2_analz... and OR4_analz... let us treat those cases using the same 
    1.81 +  argument as for the Fake case.  This is possible for most, but not all,
    1.82 +  proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    1.83 +  messages originate from the Enemy. *)
    1.84 +
    1.85 +val parts_Fake_tac = 
    1.86 +    dtac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
    1.87 +    dtac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6 THEN
    1.88 +    dtac Reveal_parts_sees_Enemy 7;
    1.89 +
    1.90 +
    1.91 +(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
    1.92 +    sends messages containing X! **)
    1.93 +
    1.94 +(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
    1.95 +goal thy 
    1.96 + "!!evs. [| evs : otway;  A ~: bad |]    \
    1.97 +\        ==> Key (shrK A) ~: parts (sees Enemy evs)";
    1.98 +be otway.induct 1;
    1.99 +by parts_Fake_tac;
   1.100 +by (Auto_tac());
   1.101 +(*Deals with Fake message*)
   1.102 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.103 +			     impOfSubs Fake_parts_insert]) 1);
   1.104 +qed "Enemy_not_see_shrK";
   1.105 +
   1.106 +bind_thm ("Enemy_not_analz_shrK",
   1.107 +	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
   1.108 +
   1.109 +Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
   1.110 +
   1.111 +(*We go to some trouble to preserve R in the 3rd and 4th subgoals
   1.112 +  As usual fast_tac cannot be used because it uses the equalities too soon*)
   1.113 +val major::prems = 
   1.114 +goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
   1.115 +\             evs : otway;                                 \
   1.116 +\             A:bad ==> R                                  \
   1.117 +\           |] ==> R";
   1.118 +br ccontr 1;
   1.119 +br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
   1.120 +by (swap_res_tac prems 2);
   1.121 +by (ALLGOALS (fast_tac (!claset addIs prems)));
   1.122 +qed "Enemy_see_shrK_E";
   1.123 +
   1.124 +bind_thm ("Enemy_analz_shrK_E", 
   1.125 +	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   1.126 +
   1.127 +AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   1.128 +
   1.129 +
   1.130 +(*** Future keys can't be seen or used! ***)
   1.131 +
   1.132 +(*Nobody can have SEEN keys that will be generated in the future.
   1.133 +  This has to be proved anew for each protocol description,
   1.134 +  but should go by similar reasoning every time.  Hardest case is the
   1.135 +  standard Fake rule.  
   1.136 +      The Union over C is essential for the induction! *)
   1.137 +goal thy "!!evs. evs : otway ==> \
   1.138 +\                length evs <= length evs' --> \
   1.139 +\                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   1.140 +be otway.induct 1;
   1.141 +by parts_Fake_tac;
   1.142 +(*auto_tac does not work here, as it performs safe_tac first*)
   1.143 +by (ALLGOALS Asm_simp_tac);
   1.144 +by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.145 +				       impOfSubs parts_insert_subset_Un,
   1.146 +				       Suc_leD]
   1.147 +			        addss (!simpset))));
   1.148 +val lemma = result();
   1.149 +
   1.150 +(*Variant needed for the main theorem below*)
   1.151 +goal thy 
   1.152 + "!!evs. [| evs : otway;  length evs <= length evs' |]    \
   1.153 +\        ==> Key (newK evs') ~: parts (sees C evs)";
   1.154 +by (fast_tac (!claset addDs [lemma]) 1);
   1.155 +qed "new_keys_not_seen";
   1.156 +Addsimps [new_keys_not_seen];
   1.157 +
   1.158 +(*Another variant: old messages must contain old keys!*)
   1.159 +goal thy 
   1.160 + "!!evs. [| Says A B X : set_of_list evs;  \
   1.161 +\           Key (newK evt) : parts {X};    \
   1.162 +\           evs : otway                 \
   1.163 +\        |] ==> length evt < length evs";
   1.164 +br ccontr 1;
   1.165 +by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   1.166 +	              addIs  [impOfSubs parts_mono, leI]) 1);
   1.167 +qed "Says_imp_old_keys";
   1.168 +
   1.169 +
   1.170 +(*** Future nonces can't be seen or used! [proofs resemble those above] ***)
   1.171 +
   1.172 +goal thy "!!evs. evs : otway ==> \
   1.173 +\                length evs <= length evs' --> \
   1.174 +\                          Nonce (newN evs') ~: (UN C. parts (sees C evs))";
   1.175 +be otway.induct 1;
   1.176 +(*auto_tac does not work here, as it performs safe_tac first*)
   1.177 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [de_Morgan_disj]
   1.178 +                                     addcongs [conj_cong])));
   1.179 +by (REPEAT_FIRST (fast_tac (!claset (*60 seconds???*)
   1.180 +			      addSEs [MPair_parts]
   1.181 +			      addDs  [Says_imp_sees_Enemy RS parts.Inj,
   1.182 +				      impOfSubs analz_subset_parts,
   1.183 +				      impOfSubs parts_insert_subset_Un,
   1.184 +				      Suc_leD]
   1.185 +			      addss (!simpset))));
   1.186 +val lemma = result();
   1.187 +
   1.188 +(*Variant needed for the main theorem below*)
   1.189 +goal thy 
   1.190 + "!!evs. [| evs : otway;  length evs <= length evs' |]    \
   1.191 +\        ==> Nonce (newN evs') ~: parts (sees C evs)";
   1.192 +by (fast_tac (!claset addDs [lemma]) 1);
   1.193 +qed "new_nonces_not_seen";
   1.194 +Addsimps [new_nonces_not_seen];
   1.195 +
   1.196 +(*Another variant: old messages must contain old nonces!*)
   1.197 +goal thy 
   1.198 + "!!evs. [| Says A B X : set_of_list evs;  \
   1.199 +\           Nonce (newN evt) : parts {X};    \
   1.200 +\           evs : otway                 \
   1.201 +\        |] ==> length evt < length evs";
   1.202 +br ccontr 1;
   1.203 +by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Enemy]
   1.204 +	              addIs  [impOfSubs parts_mono, leI]) 1);
   1.205 +qed "Says_imp_old_nonces";
   1.206 +
   1.207 +
   1.208 +(*Nobody can have USED keys that will be generated in the future.
   1.209 +  ...very like new_keys_not_seen*)
   1.210 +goal thy "!!evs. evs : otway ==> \
   1.211 +\                length evs <= length evs' --> \
   1.212 +\                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   1.213 +be otway.induct 1;
   1.214 +by parts_Fake_tac;
   1.215 +by (ALLGOALS Asm_simp_tac);
   1.216 +(*OR1 and OR3*)
   1.217 +by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   1.218 +(*Fake, OR2, OR4: these messages send unknown (X) components*)
   1.219 +by (EVERY 
   1.220 +    (map
   1.221 +     (best_tac
   1.222 +      (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   1.223 +		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   1.224 +		      Suc_leD]
   1.225 +	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   1.226 +	       addss (!simpset)))
   1.227 +     [3,2,1]));
   1.228 +(*Reveal: dummy message*)
   1.229 +by (best_tac (!claset addEs  [new_keys_not_seen RSN(2,rev_notE)]
   1.230 +		      addIs  [less_SucI, impOfSubs keysFor_mono]
   1.231 +		      addss (!simpset addsimps [le_def])) 1);
   1.232 +val lemma = result();
   1.233 +
   1.234 +goal thy 
   1.235 + "!!evs. [| evs : otway;  length evs <= length evs' |]    \
   1.236 +\        ==> newK evs' ~: keysFor (parts (sees C evs))";
   1.237 +by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   1.238 +qed "new_keys_not_used";
   1.239 +
   1.240 +bind_thm ("new_keys_not_analzd",
   1.241 +	  [analz_subset_parts RS keysFor_mono,
   1.242 +	   new_keys_not_used] MRS contra_subsetD);
   1.243 +
   1.244 +Addsimps [new_keys_not_used, new_keys_not_analzd];
   1.245 +
   1.246 +
   1.247 +(** Lemmas concerning the form of items passed in messages **)
   1.248 +
   1.249 +
   1.250 +(****
   1.251 + The following is to prove theorems of the form
   1.252 +
   1.253 +          Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
   1.254 +          Key K : analz (sees Enemy evs)
   1.255 +
   1.256 + A more general formula must be proved inductively.
   1.257 +
   1.258 +****)
   1.259 +
   1.260 +
   1.261 +(*NOT useful in this form, but it says that session keys are not used
   1.262 +  to encrypt messages containing other keys, in the actual protocol.
   1.263 +  We require that agents should behave like this subsequently also.*)
   1.264 +goal thy 
   1.265 + "!!evs. evs : otway ==> \
   1.266 +\        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   1.267 +\        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   1.268 +be otway.induct 1;
   1.269 +by parts_Fake_tac;
   1.270 +by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   1.271 +(*Deals with Faked messages*)
   1.272 +by (best_tac (!claset addSEs partsEs
   1.273 +		      addDs [impOfSubs analz_subset_parts,
   1.274 +                             impOfSubs parts_insert_subset_Un]
   1.275 +                      addss (!simpset)) 2);
   1.276 +(*Base case and Reveal*)
   1.277 +by (Auto_tac());
   1.278 +result();
   1.279 +
   1.280 +
   1.281 +(** Specialized rewriting for this proof **)
   1.282 +
   1.283 +Delsimps [image_insert];
   1.284 +Addsimps [image_insert RS sym];
   1.285 +
   1.286 +Delsimps [image_Un];
   1.287 +Addsimps [image_Un RS sym];
   1.288 +
   1.289 +goal thy "insert (Key (newK x)) (sees A evs) = \
   1.290 +\         Key `` (newK``{x}) Un (sees A evs)";
   1.291 +by (Fast_tac 1);
   1.292 +val insert_Key_singleton = result();
   1.293 +
   1.294 +goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
   1.295 +\         Key `` (f `` (insert x E)) Un C";
   1.296 +by (Fast_tac 1);
   1.297 +val insert_Key_image = result();
   1.298 +
   1.299 +
   1.300 +(*This lets us avoid analyzing the new message -- unless we have to!*)
   1.301 +(*NEEDED??*)
   1.302 +goal thy "synth (analz (sees Enemy evs)) <=   \
   1.303 +\         synth (analz (sees Enemy (Says A B X # evs)))";
   1.304 +by (Simp_tac 1);
   1.305 +br (subset_insertI RS analz_mono RS synth_mono) 1;
   1.306 +qed "synth_analz_thin";
   1.307 +
   1.308 +AddIs [impOfSubs synth_analz_thin];
   1.309 +
   1.310 +
   1.311 +
   1.312 +(** Session keys are not used to encrypt other session keys **)
   1.313 +
   1.314 +(*Describes the form of Key K when the following message is sent.  The use of
   1.315 +  "parts" strengthens the induction hyp for proving the Fake case.  The
   1.316 +  assumptions on A are needed to prevent its being a Faked message.  (Based
   1.317 +  on NS_Shared/Says_S_message_form) *)
   1.318 +goal thy
   1.319 + "!!evs. evs: otway ==>  \
   1.320 +\          Crypt {|N, Key K|} (shrK A) : parts (sees Enemy evs) & \
   1.321 +\          A ~: bad --> \
   1.322 +\        (EX evt:otway. K = newK evt)";
   1.323 +be otway.induct 1;
   1.324 +by parts_Fake_tac;
   1.325 +by (Auto_tac());
   1.326 +(*Deals with Fake message*)
   1.327 +by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   1.328 +			     impOfSubs Fake_parts_insert]) 1);
   1.329 +val lemma = result() RS mp;
   1.330 +
   1.331 +
   1.332 +(*EITHER describes the form of Key K when the following message is sent, 
   1.333 +  OR     reduces it to the Fake case.*)
   1.334 +goal thy 
   1.335 + "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
   1.336 +\           evs : otway |]                      \
   1.337 +\        ==> (EX evt:otway. K = newK evt) | Key K : analz (sees Enemy evs)";
   1.338 +by (excluded_middle_tac "A : bad" 1);
   1.339 +by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]
   1.340 +	              addss (!simpset)) 2);
   1.341 +by (forward_tac [lemma] 1);
   1.342 +by (fast_tac (!claset addEs  partsEs
   1.343 +	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   1.344 +by (Fast_tac 1);
   1.345 +qed "Reveal_message_form";
   1.346 +
   1.347 +
   1.348 +(*Lemma for the trivial direction of the if-and-only-if*)
   1.349 +goal thy  
   1.350 + "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
   1.351 +\         (K : nE | Key K : analz sEe)  ==>     \
   1.352 +\        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
   1.353 +by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
   1.354 +val lemma = result();
   1.355 +
   1.356 +
   1.357 +(*The equality makes the induction hypothesis easier to apply*)
   1.358 +goal thy  
   1.359 + "!!evs. evs : otway ==> \
   1.360 +\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   1.361 +\           (K : newK``E | Key K : analz (sees Enemy evs))";
   1.362 +be otway.induct 1;
   1.363 +bd OR2_analz_sees_Enemy 4;
   1.364 +bd OR4_analz_sees_Enemy 6;
   1.365 +bd Reveal_message_form 7;
   1.366 +by (REPEAT_FIRST (ares_tac [allI, lemma]));
   1.367 +by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
   1.368 +by (ALLGOALS (*Takes 28 secs*)
   1.369 +    (asm_simp_tac 
   1.370 +     (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.371 +			 @ pushes)
   1.372 +               setloop split_tac [expand_if])));
   1.373 +(** LEVEL 7 **)
   1.374 +(*Reveal case 2, OR4, OR2, Fake*) 
   1.375 +by (EVERY (map enemy_analz_tac [7,5,3,2]));
   1.376 +(*Reveal case 1, OR3, Base*)
   1.377 +by (Auto_tac());
   1.378 +qed_spec_mp "analz_image_newK";
   1.379 +
   1.380 +
   1.381 +goal thy
   1.382 + "!!evs. evs : otway ==>                               \
   1.383 +\        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   1.384 +\        (K = newK evt | Key K : analz (sees Enemy evs))";
   1.385 +by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   1.386 +				   insert_Key_singleton]) 1);
   1.387 +by (Fast_tac 1);
   1.388 +qed "analz_insert_Key_newK";
   1.389 +
   1.390 +
   1.391 +(*Describes the form of K and NA when the Server sends this message.*)
   1.392 +goal thy 
   1.393 + "!!evs. [| Says Server B \
   1.394 +\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.395 +\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.396 +\           evs : otway |]                                        \
   1.397 +\        ==> (EX evt:otway. K = Key(newK evt)) &            \
   1.398 +\            (EX i. NA = Nonce i)";
   1.399 +be rev_mp 1;
   1.400 +be otway.induct 1;
   1.401 +by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   1.402 +qed "Says_Server_message_form";
   1.403 +
   1.404 +
   1.405 +(*Crucial security property, but not itself enough to guarantee correctness!
   1.406 +  The need for quantification over N, C seems to indicate the problem.
   1.407 +  Omitting the Reveal message from the description deprives us of even 
   1.408 +	this clue. *)
   1.409 +goal thy 
   1.410 + "!!evs. [| A ~: bad;  B ~: bad;  evs : otway;  evt : otway |]        \
   1.411 +\    ==> Says Server B \
   1.412 +\          {|Nonce NA, Crypt {|Nonce NA, Key(newK evt)|} (shrK A), \
   1.413 +\            Crypt {|NB, Key(newK evt)|} (shrK B)|} : set_of_list evs --> \
   1.414 +\        (ALL N C. Says C Enemy {|N, Key(newK evt)|} ~: set_of_list evs) --> \
   1.415 +\        Key(newK evt) ~: analz (sees Enemy evs)";
   1.416 +be otway.induct 1;
   1.417 +bd OR2_analz_sees_Enemy 4;
   1.418 +bd OR4_analz_sees_Enemy 6;
   1.419 +bd Reveal_message_form 7;
   1.420 +by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   1.421 +by (ALLGOALS
   1.422 +    (asm_full_simp_tac 
   1.423 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.424 +			  analz_insert_Key_newK] @ pushes)
   1.425 +               setloop split_tac [expand_if])));
   1.426 +(** LEVEL 6 **)
   1.427 +(*Reveal case 1*)
   1.428 +by (Fast_tac 5);
   1.429 +(*OR3*)
   1.430 +by (fast_tac (!claset addSIs [parts_insertI]
   1.431 +		      addEs [Says_imp_old_keys RS less_irrefl]
   1.432 +	              addss (!simpset)) 3);
   1.433 +(*Reveal case 2, OR4, OR2, Fake*) 
   1.434 +br conjI 3;
   1.435 +by (REPEAT (enemy_analz_tac 1));
   1.436 +val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.437 +
   1.438 +
   1.439 +
   1.440 +(*WEAK VERSION: NEED TO ELIMINATE QUANTIFICATION OVER N, C!!*)
   1.441 +goal thy 
   1.442 + "!!evs. [| Says Server B \
   1.443 +\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.444 +\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.445 +\           (ALL N C. Says C Enemy {|N, K|} ~: set_of_list evs);  \
   1.446 +\           A ~: bad;  B ~: bad;  evs : otway |]                  \
   1.447 +\        ==> K ~: analz (sees Enemy evs)";
   1.448 +by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.449 +by (fast_tac (!claset addSEs [lemma]) 1);
   1.450 +qed "Enemy_not_see_encrypted_key";
   1.451 +
   1.452 +
   1.453 +(*** Attempting to prove stronger properties ***)
   1.454 +
   1.455 +(** The Key K uniquely identifies the Server's  message. **)
   1.456 +
   1.457 +fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   1.458 +
   1.459 +goal thy 
   1.460 + "!!evs. evs : otway ==>                      \
   1.461 +\      EX A' B' NA' NB'. ALL A B NA NB.                    \
   1.462 +\       Says Server B \
   1.463 +\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.464 +\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
   1.465 +\       A=A' & B=B' & NA=NA' & NB=NB'";
   1.466 +be otway.induct 1;
   1.467 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   1.468 +by (Step_tac 1);
   1.469 +(*Remaining cases: OR3 and OR4*)
   1.470 +by (ex_strip_tac 2);
   1.471 +by (Fast_tac 2);
   1.472 +by (excluded_middle_tac "K = Key(newK evsa)" 1);
   1.473 +by (Asm_simp_tac 1);
   1.474 +by (REPEAT (ares_tac [refl,exI,impI,conjI] 1));
   1.475 +(*...we assume X is a very new message, and handle this case by contradiction*)
   1.476 +by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   1.477 +	              delrules [conjI]    (*prevent split-up into 4 subgoals*)
   1.478 +	              addss (!simpset addsimps [parts_insertI])) 1);
   1.479 +val lemma = result();
   1.480 +
   1.481 +
   1.482 +goal thy 
   1.483 + "!!evs. [| Says Server B                                          \
   1.484 +\              {|NA, Crypt {|NA, K|} (shrK A),                     \
   1.485 +\                    Crypt {|NB, K|} (shrK B)|}                    \
   1.486 +\            : set_of_list evs;                                    \ 
   1.487 +\           Says Server B'                                         \
   1.488 +\              {|NA', Crypt {|NA', K|} (shrK A'),                  \
   1.489 +\                     Crypt {|NB', K|} (shrK B')|}                 \
   1.490 +\            : set_of_list evs;                                    \
   1.491 +\           evs : otway |]                                         \
   1.492 +\        ==> A=A' & B=B' & NA=NA' & NB=NB'";
   1.493 +bd lemma 1;
   1.494 +by (REPEAT (etac exE 1));
   1.495 +(*Duplicate the assumption*)
   1.496 +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   1.497 +by (fast_tac (!claset addSDs [spec]) 1);
   1.498 +qed "unique_session_keys";
   1.499 +
   1.500 +
   1.501 +(*Could probably remove the A ~= B premise using another induction*)
   1.502 +goal thy 
   1.503 + "!!evs. [| A ~: bad;  A ~= B; evs : otway |]               \
   1.504 +\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)        \
   1.505 +\             : parts (sees Enemy evs) -->                  \
   1.506 +\            Says A B {|NA, Agent A, Agent B,               \
   1.507 +\                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
   1.508 +\             : set_of_list evs";
   1.509 +be otway.induct 1;
   1.510 +by parts_Fake_tac;
   1.511 +by (ALLGOALS Asm_simp_tac);
   1.512 +(*Fake*)
   1.513 +by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.514 +			      impOfSubs Fake_parts_insert]) 2);
   1.515 +by (Auto_tac());
   1.516 +qed_spec_mp "Crypt_imp_OR1";
   1.517 +
   1.518 +
   1.519 +(*This key property is FALSE.  Somebody could make a fake message to Server
   1.520 +          substituting some other nonce NA' for NB.*)
   1.521 +goal thy 
   1.522 + "!!evs. [| A ~: bad;  evs : otway |]                                 \
   1.523 +\        ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees Enemy evs) --> \
   1.524 +\            Says A B {|Nonce NA, Agent A, Agent B,  \
   1.525 +\                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}  \
   1.526 +\             : set_of_list evs --> \
   1.527 +\            (EX B NB. Says Server B               \
   1.528 +\                 {|Nonce NA,               \
   1.529 +\                   Crypt {|Nonce NA, Key K|} (shrK A),              \
   1.530 +\                   Crypt {|Nonce NB, Key K|} (shrK B)|}             \
   1.531 +\                   : set_of_list evs)";
   1.532 +be otway.induct 1;
   1.533 +fun ftac rl = forward_tac [rl];
   1.534 +by (
   1.535 +    ftac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
   1.536 +    ftac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6 THEN
   1.537 +    ftac Reveal_parts_sees_Enemy 7);
   1.538 +
   1.539 +(*  by parts_Fake_tac;  ?*)
   1.540 +by (ALLGOALS Asm_simp_tac);
   1.541 +(*Fake*)
   1.542 +by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   1.543 +			      impOfSubs Fake_parts_insert]) 1);
   1.544 +(*OR1: it cannot be a new Nonce, contradiction.*)
   1.545 +by (fast_tac (!claset addSIs [parts_insertI]
   1.546 +		      addSEs partsEs
   1.547 +		      addEs [Says_imp_old_nonces RS less_irrefl]
   1.548 +	              addss (!simpset)) 1);
   1.549 +(*OR3 and OR4*)  (** LEVEL 5 **)
   1.550 +(*OR4*)
   1.551 +by (REPEAT (Safe_step_tac 2));
   1.552 +by (best_tac (!claset addSDs [parts_cut]) 3);
   1.553 +by (best_tac (!claset addSDs [parts_cut]) 3);
   1.554 +by (forward_tac [Crypt_imp_OR1] 2);
   1.555 +by (fast_tac (!claset addEs  partsEs
   1.556 +	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 4);
   1.557 +by (REPEAT (Fast_tac 2));
   1.558 +(*OR3*)  (** LEVEL 11 **)
   1.559 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   1.560 +fr impI;
   1.561 +by (REPEAT (etac conjE 1 ORELSE hyp_subst_tac 1));
   1.562 +fr impI;
   1.563 +(*The hypotheses at this point suggest an attack in which nonce NA is used
   1.564 +  in two different places*)
   1.565 +writeln "GIVE UP!";
   1.566 +
   1.567 +
   1.568 +
   1.569 +(*What can A deduce from receipt of OR4?  This too is probably FALSE*)
   1.570 +goal thy 
   1.571 + "!!evs. [| A ~: bad;  evs : otway |]                                 \
   1.572 +\        ==> ALL B' NA K B.  \
   1.573 +\            Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
   1.574 +\             : set_of_list evs -->  \
   1.575 +\            Says A B {|Nonce NA, Agent A, Agent B,                     \
   1.576 +\                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|} \
   1.577 +\             : set_of_list evs --> \
   1.578 +\            (EX NB. Says Server B \
   1.579 +\                     {|Nonce NA,               \
   1.580 +\                       Crypt {|Nonce NA, Key K|} (shrK A),              \
   1.581 +\                       Crypt {|Nonce NB, Key K|} (shrK B)|}             \
   1.582 +\                       : set_of_list evs)";
   1.583 +be otway.induct 1;
   1.584 +by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
   1.585 +(*OR2*)
   1.586 +by (Fast_tac 3);
   1.587 +(*OR1: it cannot be a new Nonce, contradiction.*)
   1.588 +by (fast_tac (!claset addSIs [parts_insertI]
   1.589 +		      addEs [Says_imp_old_nonces RS less_irrefl]
   1.590 +	              addss (!simpset)) 2);
   1.591 +by (ALLGOALS 
   1.592 +    (asm_simp_tac (!simpset addsimps [all_conj_distrib, de_Morgan_disj, de_Morgan_conj])));
   1.593 +(*Fake, OR4*) (** LEVEL 5 **)
   1.594 +by (step_tac (!claset delrules [MPair_analz]) 1);
   1.595 +by (ALLGOALS Asm_simp_tac);
   1.596 +by (fast_tac (!claset addSDs [spec]) 4);
   1.597 +by (forward_tac [Crypt_imp_OR1] 3);
   1.598 +by (fast_tac (!claset addEs  partsEs
   1.599 +	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 5);
   1.600 +by (REPEAT (Fast_tac 3));
   1.601 +(** LEVEL 11 **)
   1.602 +(*Fake (??) and OR4*)
   1.603 +
   1.604 +
   1.605 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,  de_Morgan_disj, de_Morgan_conj])));
   1.606 +
   1.607 +
   1.608 +(*** Session keys are issued at most once, and identify the principals ***)
   1.609 +
   1.610 +(** First, two lemmas for the Fake, OR2 and OR4 cases **)
   1.611 +
   1.612 +goal thy 
   1.613 + "!!evs. [| X : synth (analz (sees Enemy evs));                \
   1.614 +\           Crypt X' (shrK C) : parts{X};                      \
   1.615 +\           C ~: bad;  evs : otway |]  \
   1.616 +\        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
   1.617 +by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   1.618 +	              addDs [impOfSubs parts_insert_subset_Un]
   1.619 +                      addss (!simpset)) 1);
   1.620 +qed "Crypt_Fake_parts";
   1.621 +
   1.622 +goal thy 
   1.623 + "!!evs. [| Crypt X' K : parts (sees A evs);  evs : otway |]  \
   1.624 +\        ==> EX S S' Y. Says S S' Y : set_of_list evs &       \
   1.625 +\            Crypt X' K : parts {Y}";
   1.626 +bd parts_singleton 1;
   1.627 +by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1);
   1.628 +qed "Crypt_parts_singleton";
   1.629 +
   1.630 +(*The Key K uniquely identifies a pair of senders in the message encrypted by
   1.631 +  C, but if C=Enemy then he could send all sorts of nonsense.*)
   1.632 +goal thy 
   1.633 + "!!evs. evs : otway ==>                                     \
   1.634 +\      EX A B. ALL C.                                        \
   1.635 +\         C ~: bad -->                                       \
   1.636 +\         (ALL S S' X. Says S S' X : set_of_list evs -->     \
   1.637 +\           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
   1.638 +by (Simp_tac 1);
   1.639 +be otway.induct 1;
   1.640 +bd OR2_analz_sees_Enemy 4;
   1.641 +bd OR4_analz_sees_Enemy 6;
   1.642 +by (ALLGOALS 
   1.643 +    (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib])));
   1.644 +by (REPEAT_FIRST (etac exE));
   1.645 +(*OR4*)
   1.646 +by (ex_strip_tac 4);
   1.647 +by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   1.648 +			      Crypt_parts_singleton]) 4);
   1.649 +(*OR3: Case split propagates some context to other subgoal...*)
   1.650 +	(** LEVEL 8 **)
   1.651 +by (excluded_middle_tac "K = newK evsa" 3);
   1.652 +by (Asm_simp_tac 3);
   1.653 +by (REPEAT (ares_tac [exI] 3));
   1.654 +(*...we prove this case by contradiction: the key is too new!*)
   1.655 +by (fast_tac (!claset addIs [parts_insertI]
   1.656 +		      addSEs partsEs
   1.657 +		      addEs [Says_imp_old_keys RS less_irrefl]
   1.658 +	              addss (!simpset)) 3);
   1.659 +(*OR2*) (** LEVEL 12 **)
   1.660 +(*enemy_analz_tac just does not work here: it is an entirely different proof!*)
   1.661 +by (ex_strip_tac 2);
   1.662 +by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 2);
   1.663 +by (Simp_tac 2);
   1.664 +by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, 
   1.665 +			      Crypt_parts_singleton]) 2);
   1.666 +(*Fake*) (** LEVEL 16 **)
   1.667 +by (ex_strip_tac 1);
   1.668 +by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1);
   1.669 +qed "unique_session_keys2";
   1.670 +
   1.671 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Mon Sep 23 17:41:57 1996 +0200
     2.3 @@ -0,0 +1,79 @@
     2.4 +(*  Title:      HOL/Auth/OtwayRees_Bad
     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 "otway" for the Otway-Rees protocol.
    2.10 +
    2.11 +The FAULTY version omitting encryption of Nonce NB, as suggested on 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 +OtwayRees_Bad = Shared + 
    2.17 +
    2.18 +consts  otway   :: "event list set"
    2.19 +inductive otway
    2.20 +  intrs 
    2.21 +         (*Initial trace is empty*)
    2.22 +    Nil  "[]: otway"
    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: otway;  B ~= Enemy;  X: synth (analz (sees Enemy evs)) |]
    2.28 +          ==> Says Enemy B X  # evs : otway"
    2.29 +
    2.30 +         (*Alice initiates a protocol run*)
    2.31 +    OR1  "[| evs: otway;  A ~= B;  B ~= Server |]
    2.32 +          ==> Says A B {|Nonce (newN evs), Agent A, Agent B, 
    2.33 +                         Crypt {|Nonce (newN evs), Agent A, Agent B|} 
    2.34 +                               (shrK A) |} 
    2.35 +                 # evs : otway"
    2.36 +
    2.37 +         (*Bob's response to Alice's message.  Bob doesn't know who 
    2.38 +	   the sender is, hence the A' in the sender field.
    2.39 +           We modify the published protocol by NOT encrypting NB.*)
    2.40 +    OR2  "[| evs: otway;  B ~= Server;
    2.41 +             Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs |]
    2.42 +          ==> Says B Server 
    2.43 +                  {|Nonce NA, Agent A, Agent B, X, Nonce (newN evs), 
    2.44 +                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    2.45 +                 # evs : otway"
    2.46 +
    2.47 +         (*The Server receives Bob's message and checks that the three NAs
    2.48 +           match.  Then he sends a new session key to Bob with a packet for
    2.49 +           forwarding to Alice.*)
    2.50 +    OR3  "[| evs: otway;  B ~= Server;
    2.51 +             Says B' Server 
    2.52 +                  {|Nonce NA, Agent A, Agent B, 
    2.53 +                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), 
    2.54 +                    Nonce NB, 
    2.55 +                    Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|}
    2.56 +               : set_of_list evs |]
    2.57 +          ==> Says Server B 
    2.58 +                  {|Nonce NA, 
    2.59 +                    Crypt {|Nonce NA, Key (newK evs)|} (shrK A),
    2.60 +                    Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|}
    2.61 +                 # evs : otway"
    2.62 +
    2.63 +         (*Bob receives the Server's (?) message and compares the Nonces with
    2.64 +	   those in the message he previously sent the Server.*)
    2.65 +    OR4  "[| evs: otway;  A ~= B;  B ~= Server;
    2.66 +             Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    2.67 +               : set_of_list evs;
    2.68 +             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    2.69 +               : set_of_list evs |]
    2.70 +          ==> Says B A {|Nonce NA, X|} # evs : otway"
    2.71 +
    2.72 +         (*This message models possible leaks of session keys.  Alice's Nonce
    2.73 +           identifies the protocol run.*)
    2.74 +    Reveal "[| evs: otway;  A ~= Enemy;
    2.75 +               Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    2.76 +                 : set_of_list evs;
    2.77 +               Says A  B {|Nonce NA, Agent A, Agent B, 
    2.78 +                           Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
    2.79 +                 : set_of_list evs |]
    2.80 +            ==> Says A Enemy {|Nonce NA, Key K|} # evs : otway"
    2.81 +
    2.82 +end