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