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