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