src/HOL/Auth/OtwayRees.ML
author paulson
Wed Sep 25 17:15:18 1996 +0200 (1996-09-25)
changeset 2026 0df5a96bf77e
parent 2014 5be4c8ca7b25
child 2032 1bbf1bdcaf56
permissions -rw-r--r--
Last working version prior to introduction of "lost"
     1 (*  Title:      HOL/Auth/OtwayRees
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "otway" for the Otway-Rees protocol.
     7 
     8 Version that encrypts Nonce NB
     9 
    10 From page 244 of
    11   Burrows, Abadi and Needham.  A Logic of Authentication.
    12   Proc. Royal Soc. 426 (1989)
    13 *)
    14 
    15 
    16 open OtwayRees;
    17 
    18 proof_timing:=true;
    19 HOL_quantifiers := false;
    20 
    21 
    22 (*Weak liveness: there are traces that reach the end*)
    23 goal thy 
    24  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    25 \        ==> EX K. EX NA. EX evs: otway.          \
    26 \               Says B A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} \
    27 \                 : set_of_list evs";
    28 by (REPEAT (resolve_tac [exI,bexI] 1));
    29 br (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2;
    30 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    31 by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    32 by (ALLGOALS (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    33 result();
    34 
    35 
    36 (**** Inductive proofs about otway ****)
    37 
    38 (*The Enemy can see more than anybody else, except for their initial state*)
    39 goal thy 
    40  "!!evs. evs : otway ==> \
    41 \     sees A evs <= initState A Un sees Enemy evs";
    42 be otway.induct 1;
    43 by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
    44 			        addss (!simpset))));
    45 qed "sees_agent_subset_sees_Enemy";
    46 
    47 
    48 (*Nobody sends themselves messages*)
    49 goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs";
    50 be otway.induct 1;
    51 by (Auto_tac());
    52 qed_spec_mp "not_Says_to_self";
    53 Addsimps [not_Says_to_self];
    54 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    55 
    56 
    57 (** For reasoning about the encrypted portion of messages **)
    58 
    59 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
    60 \                X : analz (sees Enemy evs)";
    61 by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    62 qed "OR2_analz_sees_Enemy";
    63 
    64 goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \
    65 \                X : analz (sees Enemy evs)";
    66 by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1);
    67 qed "OR4_analz_sees_Enemy";
    68 
    69 goal thy "!!evs. Says B' A {|N, Crypt {|N,K|} K'|} : set_of_list evs ==> \
    70 \                K : parts (sees Enemy evs)";
    71 by (fast_tac (!claset addSEs partsEs
    72 	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
    73 qed "Reveal_parts_sees_Enemy";
    74 
    75 (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    76   argument as for the Fake case.  This is possible for most, but not all,
    77   proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    78   messages originate from the Enemy. *)
    79 
    80 val parts_Fake_tac = 
    81     forward_tac [OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)] 4 THEN
    82     forward_tac [OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)] 6 THEN
    83     forward_tac [Reveal_parts_sees_Enemy] 7;
    84 
    85 
    86 (** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY
    87     sends messages containing X! **)
    88 
    89 (*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
    90 goal thy 
    91  "!!evs. [| evs : otway;  A ~: bad |]    \
    92 \        ==> Key (shrK A) ~: parts (sees Enemy evs)";
    93 be otway.induct 1;
    94 by parts_Fake_tac;
    95 by (Auto_tac());
    96 (*Deals with Fake message*)
    97 by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    98 			     impOfSubs Fake_parts_insert]) 1);
    99 qed "Enemy_not_see_shrK";
   100 
   101 bind_thm ("Enemy_not_analz_shrK",
   102 	  [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD);
   103 
   104 Addsimps [Enemy_not_see_shrK, Enemy_not_analz_shrK];
   105 
   106 (*We go to some trouble to preserve R in the 3rd and 4th subgoals
   107   As usual fast_tac cannot be used because it uses the equalities too soon*)
   108 val major::prems = 
   109 goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
   110 \             evs : otway;                                 \
   111 \             A:bad ==> R                                  \
   112 \           |] ==> R";
   113 br ccontr 1;
   114 br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
   115 by (swap_res_tac prems 2);
   116 by (ALLGOALS (fast_tac (!claset addIs prems)));
   117 qed "Enemy_see_shrK_E";
   118 
   119 bind_thm ("Enemy_analz_shrK_E", 
   120 	  analz_subset_parts RS subsetD RS Enemy_see_shrK_E);
   121 
   122 AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
   123 
   124 
   125 (*** Future keys can't be seen or used! ***)
   126 
   127 (*Nobody can have SEEN keys that will be generated in the future.
   128   This has to be proved anew for each protocol description,
   129   but should go by similar reasoning every time.  Hardest case is the
   130   standard Fake rule.  
   131       The Union over C is essential for the induction! *)
   132 goal thy "!!evs. evs : otway ==> \
   133 \                length evs <= length evs' --> \
   134 \                          Key (newK evs') ~: (UN C. parts (sees C evs))";
   135 be otway.induct 1;
   136 by parts_Fake_tac;
   137 (*auto_tac does not work here, as it performs safe_tac first*)
   138 by (ALLGOALS Asm_simp_tac);
   139 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   140 					   impOfSubs parts_insert_subset_Un,
   141 					   Suc_leD]
   142 			            addss (!simpset))));
   143 val lemma = result();
   144 
   145 (*Variant needed for the main theorem below*)
   146 goal thy 
   147  "!!evs. [| evs : otway;  length evs <= length evs' |]    \
   148 \        ==> Key (newK evs') ~: parts (sees C evs)";
   149 by (fast_tac (!claset addDs [lemma]) 1);
   150 qed "new_keys_not_seen";
   151 Addsimps [new_keys_not_seen];
   152 
   153 (*Another variant: old messages must contain old keys!*)
   154 goal thy 
   155  "!!evs. [| Says A B X : set_of_list evs;  \
   156 \           Key (newK evt) : parts {X};    \
   157 \           evs : otway                 \
   158 \        |] ==> length evt < length evs";
   159 br ccontr 1;
   160 bd leI 1;
   161 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy]
   162                       addIs  [impOfSubs parts_mono]) 1);
   163 qed "Says_imp_old_keys";
   164 
   165 
   166 (*** Future nonces can't be seen or used! [proofs resemble those above] ***)
   167 
   168 goal thy "!!evs. evs : otway ==> \
   169 \                length evs <= length evt --> \
   170 \                          Nonce (newN evt) ~: (UN C. parts (sees C evs))";
   171 be otway.induct 1;
   172 (*auto_tac does not work here, as it performs safe_tac first*)
   173 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ parts_insert2]
   174                                      addcongs [disj_cong])));
   175 by (REPEAT_FIRST (fast_tac (!claset 
   176 			      addSEs partsEs
   177 			      addSDs  [Says_imp_sees_Enemy RS parts.Inj]
   178 			      addDs  [impOfSubs analz_subset_parts,
   179 				      impOfSubs parts_insert_subset_Un,
   180 				      Suc_leD]
   181 			      addss (!simpset))));
   182 val lemma = result();
   183 
   184 (*Variant needed for the main theorem below*)
   185 goal thy 
   186  "!!evs. [| evs : otway;  length evs <= length evs' |]    \
   187 \        ==> Nonce (newN evs') ~: parts (sees C evs)";
   188 by (fast_tac (!claset addDs [lemma]) 1);
   189 qed "new_nonces_not_seen";
   190 Addsimps [new_nonces_not_seen];
   191 
   192 (*Another variant: old messages must contain old nonces!*)
   193 goal thy 
   194  "!!evs. [| Says A B X : set_of_list evs;  \
   195 \           Nonce (newN evt) : parts {X};    \
   196 \           evs : otway                 \
   197 \        |] ==> length evt < length evs";
   198 br ccontr 1;
   199 bd leI 1;
   200 by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Enemy]
   201 	              addIs  [impOfSubs parts_mono]) 1);
   202 qed "Says_imp_old_nonces";
   203 
   204 
   205 (*Nobody can have USED keys that will be generated in the future.
   206   ...very like new_keys_not_seen*)
   207 goal thy "!!evs. evs : otway ==> \
   208 \                length evs <= length evs' --> \
   209 \                newK evs' ~: keysFor (UN C. parts (sees C evs))";
   210 be otway.induct 1;
   211 by parts_Fake_tac;
   212 by (ALLGOALS Asm_simp_tac);
   213 (*OR1 and OR3*)
   214 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   215 (*Fake, OR2, OR4: these messages send unknown (X) components*)
   216 by (EVERY 
   217     (map
   218      (best_tac
   219       (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   220 		      impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   221 		      Suc_leD]
   222 	       addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   223 	       addss (!simpset)))
   224      [3,2,1]));
   225 (*Reveal: dummy message*)
   226 by (best_tac (!claset addEs  [new_keys_not_seen RSN(2,rev_notE)]
   227 		      addIs  [less_SucI, impOfSubs keysFor_mono]
   228 		      addss (!simpset addsimps [le_def])) 1);
   229 val lemma = result();
   230 
   231 goal thy 
   232  "!!evs. [| evs : otway;  length evs <= length evs' |]    \
   233 \        ==> newK evs' ~: keysFor (parts (sees C evs))";
   234 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   235 qed "new_keys_not_used";
   236 
   237 bind_thm ("new_keys_not_analzd",
   238 	  [analz_subset_parts RS keysFor_mono,
   239 	   new_keys_not_used] MRS contra_subsetD);
   240 
   241 Addsimps [new_keys_not_used, new_keys_not_analzd];
   242 
   243 
   244 (** Lemmas concerning the form of items passed in messages **)
   245 
   246 
   247 (****
   248  The following is to prove theorems of the form
   249 
   250           Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
   251           Key K : analz (sees Enemy evs)
   252 
   253  A more general formula must be proved inductively.
   254 
   255 ****)
   256 
   257 
   258 (*NOT useful in this form, but it says that session keys are not used
   259   to encrypt messages containing other keys, in the actual protocol.
   260   We require that agents should behave like this subsequently also.*)
   261 goal thy 
   262  "!!evs. evs : otway ==> \
   263 \        (Crypt X (newK evt)) : parts (sees Enemy evs) & \
   264 \        Key K : parts {X} --> Key K : parts (sees Enemy evs)";
   265 be otway.induct 1;
   266 by parts_Fake_tac;
   267 by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes)));
   268 (*Deals with Faked messages*)
   269 by (best_tac (!claset addSEs partsEs
   270 		      addDs [impOfSubs parts_insert_subset_Un]
   271                       addss (!simpset)) 2);
   272 (*Base case and Reveal*)
   273 by (Auto_tac());
   274 result();
   275 
   276 
   277 (** Specialized rewriting for this proof **)
   278 
   279 Delsimps [image_insert];
   280 Addsimps [image_insert RS sym];
   281 
   282 Delsimps [image_Un];
   283 Addsimps [image_Un RS sym];
   284 
   285 goal thy "insert (Key (newK x)) (sees A evs) = \
   286 \         Key `` (newK``{x}) Un (sees A evs)";
   287 by (Fast_tac 1);
   288 val insert_Key_singleton = result();
   289 
   290 goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
   291 \         Key `` (f `` (insert x E)) Un C";
   292 by (Fast_tac 1);
   293 val insert_Key_image = result();
   294 
   295 
   296 (*This lets us avoid analyzing the new message -- unless we have to!*)
   297 (*NEEDED??*)
   298 goal thy "synth (analz (sees Enemy evs)) <=   \
   299 \         synth (analz (sees Enemy (Says A B X # evs)))";
   300 by (Simp_tac 1);
   301 br (subset_insertI RS analz_mono RS synth_mono) 1;
   302 qed "synth_analz_thin";
   303 
   304 AddIs [impOfSubs synth_analz_thin];
   305 
   306 
   307 
   308 (** Session keys are not used to encrypt other session keys **)
   309 
   310 (*Describes the form of Key K when the following message is sent.  The use of
   311   "parts" strengthens the induction hyp for proving the Fake case.  The
   312   assumptions on A are needed to prevent its being a Faked message.  (Based
   313   on NS_Shared/Says_S_message_form) *)
   314 goal thy
   315  "!!evs. evs: otway ==>                                           \
   316 \          Crypt {|N, Key K|} (shrK A) : parts (sees Enemy evs) & \
   317 \          A ~: bad -->                                           \
   318 \        (EX evt:otway. K = newK evt)";
   319 be otway.induct 1;
   320 by parts_Fake_tac;
   321 by (Auto_tac());
   322 (*Deals with Fake message*)
   323 by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   324 			     impOfSubs Fake_parts_insert]) 1);
   325 val lemma = result() RS mp;
   326 
   327 
   328 (*EITHER describes the form of Key K when the following message is sent, 
   329   OR     reduces it to the Fake case.*)
   330 goal thy 
   331  "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
   332 \           evs : otway |]                      \
   333 \        ==> (EX evt:otway. K = newK evt) | Key K : analz (sees Enemy evs)";
   334 by (excluded_middle_tac "A : bad" 1);
   335 by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]
   336 	              addss (!simpset)) 2);
   337 by (forward_tac [lemma] 1);
   338 by (fast_tac (!claset addEs  partsEs
   339 	              addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   340 by (Fast_tac 1);
   341 qed "Reveal_message_form";
   342 
   343 
   344 (*Lemma for the trivial direction of the if-and-only-if*)
   345 goal thy  
   346  "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
   347 \         (K : nE | Key K : analz sEe)  ==>     \
   348 \        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
   349 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
   350 val lemma = result();
   351 
   352 
   353 (*The equality makes the induction hypothesis easier to apply*)
   354 goal thy  
   355  "!!evs. evs : otway ==> \
   356 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   357 \           (K : newK``E | Key K : analz (sees Enemy evs))";
   358 be otway.induct 1;
   359 bd OR2_analz_sees_Enemy 4;
   360 bd OR4_analz_sees_Enemy 6;
   361 bd Reveal_message_form 7;
   362 by (REPEAT_FIRST (ares_tac [allI, lemma]));
   363 by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
   364 by (ALLGOALS (*Takes 28 secs*)
   365     (asm_simp_tac 
   366      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   367 			 @ pushes)
   368                setloop split_tac [expand_if])));
   369 (** LEVEL 7 **)
   370 (*Reveal case 2, OR4, OR2, Fake*) 
   371 by (EVERY (map enemy_analz_tac [7,5,3,2]));
   372 (*Reveal case 1, OR3, Base*)
   373 by (Auto_tac());
   374 qed_spec_mp "analz_image_newK";
   375 
   376 
   377 goal thy
   378  "!!evs. evs : otway ==>                               \
   379 \        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   380 \        (K = newK evt | Key K : analz (sees Enemy evs))";
   381 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   382 				   insert_Key_singleton]) 1);
   383 by (Fast_tac 1);
   384 qed "analz_insert_Key_newK";
   385 
   386 
   387 (*** The Key K uniquely identifies the Server's  message. **)
   388 
   389 fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   390 
   391 goal thy 
   392  "!!evs. evs : otway ==>                      \
   393 \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   394 \       Says Server B \
   395 \            {|NA, Crypt {|NA, K|} (shrK A),                      \
   396 \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
   397 \       A=A' & B=B' & NA=NA' & NB=NB'";
   398 be otway.induct 1;
   399 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   400 by (Step_tac 1);
   401 (*Remaining cases: OR3 and OR4*)
   402 by (ex_strip_tac 2);
   403 by (Fast_tac 2);
   404 by (excluded_middle_tac "K = Key(newK evsa)" 1);
   405 by (Asm_simp_tac 1);
   406 by (REPEAT (ares_tac [refl,exI,impI,conjI] 1));
   407 (*...we assume X is a very new message, and handle this case by contradiction*)
   408 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   409 	              delrules [conjI]    (*prevent split-up into 4 subgoals*)
   410 	              addss (!simpset addsimps [parts_insertI])) 1);
   411 val lemma = result();
   412 
   413 goal thy 
   414  "!!evs. [| Says Server B                                          \
   415 \              {|NA, Crypt {|NA, K|} (shrK A),                     \
   416 \                    Crypt {|NB, K|} (shrK B)|}                    \
   417 \            : set_of_list evs;                                    \ 
   418 \           Says Server B'                                         \
   419 \              {|NA', Crypt {|NA', K|} (shrK A'),                  \
   420 \                     Crypt {|NB', K|} (shrK B')|}                 \
   421 \            : set_of_list evs;                                    \
   422 \           evs : otway |]                                         \
   423 \        ==> A=A' & B=B' & NA=NA' & NB=NB'";
   424 bd lemma 1;
   425 by (REPEAT (etac exE 1));
   426 (*Duplicate the assumption*)
   427 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   428 by (fast_tac (!claset addSDs [spec]) 1);
   429 qed "unique_session_keys";
   430 
   431 
   432 
   433 (**** Towards proving stronger authenticity properties ****)
   434 
   435 (*Only OR1 can have caused such a part of a message to appear.*)
   436 goal thy 
   437  "!!evs. [| A ~: bad;  evs : otway |]               \
   438 \        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)        \
   439 \             : parts (sees Enemy evs) -->                  \
   440 \            Says A B {|NA, Agent A, Agent B,               \
   441 \                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
   442 \             : set_of_list evs";
   443 be otway.induct 1;
   444 by parts_Fake_tac;
   445 by (ALLGOALS Asm_simp_tac);
   446 (*Fake*)
   447 by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   448 			      impOfSubs Fake_parts_insert]) 2);
   449 by (Auto_tac());
   450 qed_spec_mp "Crypt_imp_OR1";
   451 
   452 
   453 (** The Nonce NA uniquely identifies A's  message. **)
   454 
   455 goal thy 
   456  "!!evs. [| evs : otway; A ~: bad |]               \
   457 \ ==> EX B'. ALL B.    \
   458 \        Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees Enemy evs) --> \
   459 \        B = B'";
   460 be otway.induct 1;
   461 by parts_Fake_tac;
   462 by (ALLGOALS Asm_simp_tac);
   463 (*Fake*)
   464 by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   465 			      impOfSubs Fake_parts_insert]) 2);
   466 (*Base case*)
   467 by (fast_tac (!claset addss (!simpset)) 1);
   468 by (Step_tac 1);
   469 (*OR1: creation of new Nonce.  Move assertion into global context*)
   470 by (excluded_middle_tac "NA = Nonce (newN evsa)" 1);
   471 by (Asm_simp_tac 1);
   472 by (Fast_tac 1);
   473 by (best_tac (!claset addSEs partsEs
   474 	              addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
   475 val lemma = result();
   476 
   477 goal thy 
   478  "!!evs.[| Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees Enemy evs); \ 
   479 \          Crypt {|NA, Agent A, Agent C|} (shrK A) : parts (sees Enemy evs); \ 
   480 \          evs : otway;  A ~: bad |]                                         \
   481 \        ==> B = C";
   482 bd lemma 1;
   483 ba 1;
   484 by (etac exE 1);
   485 (*Duplicate the assumption*)
   486 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   487 by (fast_tac (!claset addSDs [spec]) 1);
   488 qed "unique_OR1_nonce";
   489 
   490 
   491 val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
   492 
   493 (*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   494   OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   495   over-simplified version of this protocol: see OtwayRees_Bad.*)
   496 goal thy 
   497  "!!evs. [| A ~: bad;  evs : otway |]                            \
   498 \        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)             \
   499 \             : parts (sees Enemy evs) -->                       \
   500 \            Crypt {|NA', NA, Agent A', Agent A|} (shrK A)       \
   501 \             ~: parts (sees Enemy evs)";
   502 be otway.induct 1;
   503 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2])));
   504 (*It is hard to generate this proof in a reasonable amount of time*)
   505 by (step_tac (!claset addSEs [MPair_parts, nonce_not_seen_now]
   506                       addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1);
   507 by (REPEAT_FIRST (fast_tac (!claset (*40 seconds??*)
   508 			    addSDs  [impOfSubs analz_subset_parts,
   509 				     impOfSubs parts_insert_subset_Un]
   510 			    addss  (!simpset))));
   511 by (REPEAT_FIRST (fast_tac (!claset 
   512 			      addSEs (partsEs@[nonce_not_seen_now])
   513                               addSDs  [impOfSubs parts_insert_subset_Un]
   514                               addss (!simpset))));
   515 qed_spec_mp"no_nonce_OR1_OR2";
   516 
   517 
   518 
   519 (*If the encrypted message appears, and A has used Nonce NA to start a run,
   520   then it originated with the Server!*)
   521 goal thy 
   522  "!!evs. [| A ~: bad;  evs : otway |]                                        \
   523 \        ==> Crypt {|Nonce NA, Key K|} (shrK A) : parts (sees Enemy evs) --> \
   524 \            Says A B {|Nonce NA, Agent A, Agent B,                          \
   525 \                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}      \
   526 \             : set_of_list evs -->                                          \
   527 \            (EX NB. Says Server B                                           \
   528 \                 {|Nonce NA,                                                \
   529 \                   Crypt {|Nonce NA, Key K|} (shrK A),                      \
   530 \                   Crypt {|Nonce NB, Key K|} (shrK B)|}                     \
   531 \                   : set_of_list evs)";
   532 be otway.induct 1;
   533 by parts_Fake_tac;
   534 by (ALLGOALS Asm_simp_tac);
   535 (*Fake*)
   536 by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   537 			      impOfSubs Fake_parts_insert]) 1);
   538 (*OR1: it cannot be a new Nonce, contradiction.*)
   539 by (fast_tac (!claset addSIs [parts_insertI]
   540 		      addSEs partsEs
   541 		      addEs [Says_imp_old_nonces RS less_irrefl]
   542 	              addss (!simpset)) 1);
   543 (*OR3 and OR4*)  (** LEVEL 5 **)
   544 (*OR4*)
   545 by (REPEAT (Safe_step_tac 2));
   546 by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
   547 by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   548 		      addEs  partsEs
   549 	              addDs [Says_imp_sees_Enemy RS parts.Inj]) 2);
   550 (*OR3*)  (** LEVEL 8 **)
   551 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   552 by (step_tac (!claset delrules [disjCI, impCE]) 1);
   553 by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS parts.Inj]
   554                       addSEs [MPair_parts]
   555                       addEs  [unique_OR1_nonce]) 1);
   556 by (fast_tac (!claset addSEs [MPair_parts]
   557                       addSDs [Says_imp_sees_Enemy RS parts.Inj]
   558                       addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   559 	              delrules [conjI] (*stop split-up into 4 subgoals*)) 1);
   560 qed_spec_mp "Crypt_imp_Server_msg";
   561 
   562 
   563 (*Crucial property: if A receives B's OR4 message and the nonce NA agrees
   564   then the key really did come from the Server!  CANNOT prove this of the
   565   bad form of this protocol, even though we can prove
   566   Enemy_not_see_encrypted_key*)
   567 goal thy 
   568  "!!evs. [| A ~: bad;  evs : otway |]                                    \
   569 \        ==> Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}  \
   570 \             : set_of_list evs -->                                      \
   571 \            Says A B {|Nonce NA, Agent A, Agent B,                      \
   572 \                       Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}  \
   573 \             : set_of_list evs -->                                      \
   574 \            (EX NB. Says Server B                                       \
   575 \                     {|Nonce NA,                                        \
   576 \                       Crypt {|Nonce NA, Key K|} (shrK A),              \
   577 \                       Crypt {|Nonce NB, Key K|} (shrK B)|}             \
   578 \                       : set_of_list evs)";
   579 be otway.induct 1;
   580 by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong])));
   581 (*OR2*)
   582 by (Fast_tac 3);
   583 (*OR1: it cannot be a new Nonce, contradiction.*)
   584 by (fast_tac (!claset addSIs [parts_insertI]
   585 		      addEs [Says_imp_old_nonces RS less_irrefl]
   586 	              addss (!simpset)) 2);
   587 (*Fake, OR4*) (** LEVEL 4 **)
   588 by (step_tac (!claset delrules [impCE]) 1);
   589 by (ALLGOALS Asm_simp_tac);
   590 by (Fast_tac 4);
   591 by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   592 		      addEs  partsEs
   593 	              addDs [Says_imp_sees_Enemy RS parts.Inj]) 3);
   594 (** LEVEL 8 **)
   595 (*Still subcases of Fake and OR4*)
   596 by (fast_tac (!claset addSIs [Crypt_imp_Server_msg]
   597 	              addDs  [impOfSubs analz_subset_parts]) 1);
   598 by (fast_tac (!claset addSIs [Crypt_imp_Server_msg]
   599 	              addEs  partsEs
   600 	              addDs  [Says_imp_sees_Enemy RS parts.Inj]) 1);
   601 val lemma = result();
   602 
   603 val OR4_imp_Says_Server_A = 
   604     lemma RSN (2, rev_mp) RS mp |> standard;
   605 
   606 
   607 
   608 (*Describes the form of K and NA when the Server sends this message.*)
   609 goal thy 
   610  "!!evs. [| Says Server B \
   611 \            {|NA, Crypt {|NA, K|} (shrK A),                      \
   612 \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   613 \           evs : otway |]                                        \
   614 \        ==> (EX evt:otway. K = Key(newK evt)) &                  \
   615 \            (EX i. NA = Nonce i)";
   616 be rev_mp 1;
   617 be otway.induct 1;
   618 by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   619 qed "Says_Server_message_form";
   620 
   621 
   622 (** Crucial secrecy property: Enemy does not see the keys sent in msg OR3 **)
   623 
   624 goal thy 
   625  "!!evs. [| A ~: bad;  B ~: bad;  evs : otway;  evt : otway |]         \
   626 \        ==> Says Server B                                             \
   627 \              {|Nonce NA, Crypt {|Nonce NA, Key(newK evt)|} (shrK A), \
   628 \                Crypt {|NB, Key(newK evt)|} (shrK B)|} : set_of_list evs --> \
   629 \            Says A Enemy {|Nonce NA, Key(newK evt)|} ~: set_of_list evs --> \
   630 \            Key(newK evt) ~: analz (sees Enemy evs)";
   631 be otway.induct 1;
   632 bd OR2_analz_sees_Enemy 4;
   633 bd OR4_analz_sees_Enemy 6;
   634 by (forward_tac [Reveal_message_form] 7);
   635 by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   636 by (ALLGOALS
   637     (asm_full_simp_tac 
   638      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   639 			  analz_insert_Key_newK] @ pushes)
   640                setloop split_tac [expand_if])));
   641 (** LEVEL 6 **)
   642 (*OR3*)
   643 by (fast_tac (!claset addSIs [parts_insertI]
   644 		      addEs [Says_imp_old_keys RS less_irrefl]
   645 	              addss (!simpset)) 3);
   646 (*Reveal case 2, OR4, OR2, Fake*) 
   647 by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' enemy_analz_tac));
   648 (*Reveal case 1*) (** LEVEL 8 **)
   649 by (excluded_middle_tac "Aa : bad" 1);
   650 (*But this contradicts Key(newK evt) ~: analz (sees Enemy evsa) *)
   651 bd (Says_imp_sees_Enemy RS analz.Inj) 2;
   652 by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 2);
   653 (*So now we have  Aa ~: bad *)
   654 by (dresolve_tac [OR4_imp_Says_Server_A] 1);
   655 by (REPEAT (assume_tac 1));
   656 by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   657 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   658 
   659 goal thy 
   660  "!!evs. [| Says Server B \
   661 \            {|NA, Crypt {|NA, K|} (shrK A),                      \
   662 \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   663 \           Says A Enemy {|NA, K|} ~: set_of_list evs;            \
   664 \           A ~: bad;  B ~: bad;  evs : otway |]                  \
   665 \        ==> K ~: analz (sees Enemy evs)";
   666 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   667 by (fast_tac (!claset addSEs [lemma]) 1);
   668 qed "Enemy_not_see_encrypted_key";
   669 
   670 
   671 
   672 (** A session key uniquely identifies a pair of senders in the message
   673     encrypted by a good agent C. **)
   674 goal thy 
   675  "!!evs. evs : otway ==>                                           \
   676 \      EX A B. ALL C N.                                            \
   677 \         C ~: bad -->                                             \
   678 \         Crypt {|N, Key K|} (shrK C) : parts (sees Enemy evs) --> \
   679 \         C=A | C=B";
   680 by (Simp_tac 1);	(*Miniscoping*)
   681 be otway.induct 1;
   682 bd OR2_analz_sees_Enemy 4;
   683 bd OR4_analz_sees_Enemy 6;
   684 (*enemy_analz_tac just does not work here: it is an entirely different proof!*)
   685 by (ALLGOALS 
   686     (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,
   687 				      imp_conj_distrib, parts_insert_sees,
   688 				      parts_insert2])));
   689 by (REPEAT_FIRST (etac exE));
   690 (*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **)
   691 by (excluded_middle_tac "K = newK evsa" 4);
   692 by (Asm_simp_tac 4);
   693 by (REPEAT (ares_tac [exI] 4));
   694 (*...we prove this case by contradiction: the key is too new!*)
   695 by (fast_tac (!claset addSEs partsEs
   696 		      addEs [Says_imp_old_keys RS less_irrefl]
   697 	              addss (!simpset)) 4);
   698 (*Base, Fake, OR2, OR4*)
   699 by (REPEAT_FIRST ex_strip_tac);
   700 bd synth.Inj 4;
   701 bd synth.Inj 3;
   702 (*Now in effect there are three Fake cases*)
   703 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs Fake_parts_insert]
   704 			            addss (!simpset))));
   705 qed "key_identifies_senders";