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