src/HOL/Auth/OtwayRees.ML
author paulson
Thu Jun 19 11:31:14 1997 +0200 (1997-06-19)
changeset 3451 d10f100676d8
parent 3207 fe79ad367d77
child 3465 e85c24717cad
permissions -rw-r--r--
Made proofs more concise by replacing calls to spy_analz_tac by uses of
analz_insert_eq in rewriting
     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 (*Replacing the variable by a constant improves search speed by 50%!*)
    21 val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
    22 
    23 
    24 (*A "possibility property": there are traces that reach the end*)
    25 goal thy 
    26  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    27 \        ==> EX K. EX NA. EX evs: otway lost.          \
    28 \               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    29 \                 : set_of_list evs";
    30 by (REPEAT (resolve_tac [exI,bexI] 1));
    31 by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    32 by possibility_tac;
    33 result();
    34 
    35 
    36 (**** Inductive proofs about otway ****)
    37 
    38 (*Monotonicity*)
    39 goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
    40 by (rtac subsetI 1);
    41 by (etac otway.induct 1);
    42 by (ALLGOALS
    43     (blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono)
    44                               :: otway.intrs))));
    45 qed "otway_mono";
    46 
    47 (*Nobody sends themselves messages*)
    48 goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
    49 by (etac otway.induct 1);
    50 by (Auto_tac());
    51 qed_spec_mp "not_Says_to_self";
    52 Addsimps [not_Says_to_self];
    53 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    54 
    55 
    56 (** For reasoning about the encrypted portion of messages **)
    57 
    58 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs \
    59 \                ==> X : analz (sees lost Spy evs)";
    60 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    61 qed "OR2_analz_sees_Spy";
    62 
    63 goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs \
    64 \                ==> X : analz (sees lost Spy evs)";
    65 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    66 qed "OR4_analz_sees_Spy";
    67 
    68 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
    69 \                 ==> K : parts (sees lost Spy evs)";
    70 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
    71 qed "Oops_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 (*For proving the easier theorems about X ~: parts (sees lost Spy evs).
    84   We instantiate the variable to "lost" since leaving it as a Var would
    85   interfere with simplification.*)
    86 val parts_induct_tac = 
    87     let val tac = forw_inst_tac [("lost","lost")] 
    88     in  etac otway.induct	   1 THEN 
    89 	tac OR2_parts_sees_Spy     4 THEN 
    90         tac OR4_parts_sees_Spy     6 THEN
    91         tac Oops_parts_sees_Spy    7 THEN
    92 	prove_simple_subgoals_tac  1
    93     end;
    94 
    95 
    96 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    97     sends messages containing X! **)
    98 
    99 
   100 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
   101 goal thy 
   102  "!!evs. evs : otway lost \
   103 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
   104 by parts_induct_tac;
   105 by (Fake_parts_insert_tac 1);
   106 by (Blast_tac 1);
   107 qed "Spy_see_shrK";
   108 Addsimps [Spy_see_shrK];
   109 
   110 goal thy 
   111  "!!evs. evs : otway lost \
   112 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
   113 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   114 qed "Spy_analz_shrK";
   115 Addsimps [Spy_analz_shrK];
   116 
   117 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   118 \                  evs : otway lost |] ==> A:lost";
   119 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   120 qed "Spy_see_shrK_D";
   121 
   122 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   123 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   124 
   125 
   126 (*Nobody can have used non-existent keys!*)
   127 goal thy "!!evs. evs : otway lost ==>          \
   128 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   129 by parts_induct_tac;
   130 (*Fake*)
   131 by (best_tac
   132       (!claset addIs [impOfSubs analz_subset_parts]
   133                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   134                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   135                addss (!simpset)) 1);
   136 by (ALLGOALS Blast_tac);
   137 qed_spec_mp "new_keys_not_used";
   138 
   139 bind_thm ("new_keys_not_analzd",
   140           [analz_subset_parts RS keysFor_mono,
   141            new_keys_not_used] MRS contra_subsetD);
   142 
   143 Addsimps [new_keys_not_used, new_keys_not_analzd];
   144 
   145 
   146 
   147 (*** Proofs involving analz ***)
   148 
   149 (*Describes the form of K and NA when the Server sends this message.  Also
   150   for Oops case.*)
   151 goal thy 
   152  "!!evs. [| Says Server B                                                 \
   153 \            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;   \
   154 \           evs : otway lost |]                                           \
   155 \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   156 by (etac rev_mp 1);
   157 by (etac otway.induct 1);
   158 by (ALLGOALS Simp_tac);
   159 by (ALLGOALS Blast_tac);
   160 qed "Says_Server_message_form";
   161 
   162 
   163 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   164 val analz_sees_tac = 
   165     dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN 
   166     dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   167     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   168     assume_tac 7 THEN
   169     REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
   170 
   171 
   172 (****
   173  The following is to prove theorems of the form
   174 
   175   Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   176   Key K : analz (sees lost Spy evs)
   177 
   178  A more general formula must be proved inductively.
   179 ****)
   180 
   181 
   182 (** Session keys are not used to encrypt other session keys **)
   183 
   184 (*The equality makes the induction hypothesis easier to apply*)
   185 goal thy  
   186  "!!evs. evs : otway lost ==>                                         \
   187 \  ALL K KK. KK <= Compl (range shrK) -->                      \
   188 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   189 \            (K : KK | Key K : analz (sees lost Spy evs))";
   190 by (etac otway.induct 1);
   191 by analz_sees_tac;
   192 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   193 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   194 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   195 (*Fake*) 
   196 by (spy_analz_tac 2);
   197 (*Base*)
   198 by (Blast_tac 1);
   199 qed_spec_mp "analz_image_freshK";
   200 
   201 
   202 goal thy
   203  "!!evs. [| evs : otway lost;  KAB ~: range shrK |] ==>             \
   204 \        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
   205 \        (K = KAB | Key K : analz (sees lost Spy evs))";
   206 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   207 qed "analz_insert_freshK";
   208 
   209 
   210 (*** The Key K uniquely identifies the Server's  message. **)
   211 
   212 goal thy 
   213  "!!evs. evs : otway lost ==>                                                 \
   214 \   EX B' NA' NB' X'. ALL B NA NB X.                                          \
   215 \     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
   216 \     B=B' & NA=NA' & NB=NB' & X=X'";
   217 by (etac otway.induct 1);
   218 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   219 by (Step_tac 1);
   220 (*Remaining cases: OR3 and OR4*)
   221 by (ex_strip_tac 2);
   222 by (Best_tac 2);
   223 by (expand_case_tac "K = ?y" 1);
   224 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   225 (*...we assume X is a recent message, and handle this case by contradiction*)
   226 by (blast_tac (!claset addSEs sees_Spy_partsEs
   227                        delrules [conjI] (*no split-up into 4 subgoals*)) 1);
   228 val lemma = result();
   229 
   230 goal thy 
   231  "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
   232 \            : set_of_list evs;                                    \ 
   233 \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
   234 \            : set_of_list evs;                                    \
   235 \           evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
   236 by (prove_unique_tac lemma 1);
   237 qed "unique_session_keys";
   238 
   239 
   240 
   241 (**** Authenticity properties relating to NA ****)
   242 
   243 (*Only OR1 can have caused such a part of a message to appear.*)
   244 goal thy 
   245  "!!evs. [| A ~: lost;  evs : otway lost |]                        \
   246 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}               \
   247 \             : parts (sees lost Spy evs) -->                      \
   248 \            Says A B {|NA, Agent A, Agent B,                      \
   249 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
   250 \             : set_of_list evs";
   251 by parts_induct_tac;
   252 by (Fake_parts_insert_tac 1);
   253 qed_spec_mp "Crypt_imp_OR1";
   254 
   255 
   256 (** The Nonce NA uniquely identifies A's message. **)
   257 
   258 goal thy 
   259  "!!evs. [| evs : otway lost; A ~: lost |]               \
   260 \ ==> EX B'. ALL B.    \
   261 \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
   262 \        --> B = B'";
   263 by parts_induct_tac;
   264 by (Fake_parts_insert_tac 1);
   265 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   266 (*OR1: creation of new Nonce.  Move assertion into global context*)
   267 by (expand_case_tac "NA = ?y" 1);
   268 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   269 val lemma = result();
   270 
   271 goal thy 
   272  "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts(sees lost Spy evs); \
   273 \          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \
   274 \          evs : otway lost;  A ~: lost |]                                    \
   275 \        ==> B = C";
   276 by (prove_unique_tac lemma 1);
   277 qed "unique_NA";
   278 
   279 
   280 (*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   281   OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   282   over-simplified version of this protocol: see OtwayRees_Bad.*)
   283 goal thy 
   284  "!!evs. [| A ~: lost;  evs : otway lost |]                      \
   285 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}             \
   286 \             : parts (sees lost Spy evs) -->                    \
   287 \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
   288 \             ~: parts (sees lost Spy evs)";
   289 by parts_induct_tac;
   290 by (Fake_parts_insert_tac 1);
   291 by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs
   292                                addSDs  [impOfSubs parts_insert_subset_Un]) 1));
   293 qed_spec_mp"no_nonce_OR1_OR2";
   294 
   295 
   296 (*Crucial property: If the encrypted message appears, and A has used NA
   297   to start a run, then it originated with the Server!*)
   298 goal thy 
   299  "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                 \
   300 \    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs)      \
   301 \        --> Says A B {|NA, Agent A, Agent B,                          \
   302 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
   303 \             : set_of_list evs -->                                    \
   304 \            (EX NB. Says Server B                                     \
   305 \                 {|NA,                                                \
   306 \                   Crypt (shrK A) {|NA, Key K|},                      \
   307 \                   Crypt (shrK B) {|NB, Key K|}|}                     \
   308 \                   : set_of_list evs)";
   309 by parts_induct_tac;
   310 by (Fake_parts_insert_tac 1);
   311 (*OR1: it cannot be a new Nonce, contradiction.*)
   312 by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   313 (*OR3 and OR4*) 
   314 (*OR4*)
   315 by (REPEAT (Safe_step_tac 2));
   316 by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
   317 by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   318                       addEs  sees_Spy_partsEs) 2);
   319 (*OR3*)  (** LEVEL 5 **)
   320 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   321 by (step_tac (!claset delrules [disjCI, impCE]) 1);
   322 by (blast_tac (!claset addSEs [MPair_parts]
   323                       addSDs [Says_imp_sees_Spy' RS parts.Inj]
   324                       addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   325                       delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   326 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   327                       addSEs [MPair_parts]
   328                       addIs  [unique_NA]) 1);
   329 qed_spec_mp "NA_Crypt_imp_Server_msg";
   330 
   331 
   332 (*Corollary: if A receives B's OR4 message and the nonce NA agrees
   333   then the key really did come from the Server!  CANNOT prove this of the
   334   bad form of this protocol, even though we can prove
   335   Spy_not_see_encrypted_key*)
   336 goal thy 
   337  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   338 \            : set_of_list evs;                                    \
   339 \           Says A B {|NA, Agent A, Agent B,                       \
   340 \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   341 \            : set_of_list evs;                                    \
   342 \           A ~: lost;  A ~= Spy;  evs : otway lost |]             \
   343 \        ==> EX NB. Says Server B                                  \
   344 \                     {|NA,                                        \
   345 \                       Crypt (shrK A) {|NA, Key K|},              \
   346 \                       Crypt (shrK B) {|NB, Key K|}|}             \
   347 \                       : set_of_list evs";
   348 by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   349                        addEs  sees_Spy_partsEs) 1);
   350 qed "A_trusts_OR4";
   351 
   352 
   353 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   354     Does not in itself guarantee security: an attack could violate 
   355     the premises, e.g. by having A=Spy **)
   356 
   357 goal thy 
   358  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
   359 \        ==> Says Server B                                                 \
   360 \              {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   361 \                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs -->      \
   362 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   363 \            Key K ~: analz (sees lost Spy evs)";
   364 by (etac otway.induct 1);
   365 by analz_sees_tac;
   366 by (ALLGOALS
   367     (asm_simp_tac (!simpset addcongs [conj_cong] 
   368                             addsimps [analz_insert_eq, not_parts_not_analz, 
   369 				      analz_insert_freshK]
   370                             setloop split_tac [expand_if])));
   371 (*Oops*)
   372 by (blast_tac (!claset addSDs [unique_session_keys]) 4);
   373 (*OR4*) 
   374 by (Blast_tac 3);
   375 (*OR3*)
   376 by (blast_tac (!claset addSEs sees_Spy_partsEs
   377                        addIs [impOfSubs analz_subset_parts]) 2);
   378 (*Fake*) 
   379 by (spy_analz_tac 1);
   380 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   381 
   382 goal thy 
   383  "!!evs. [| Says Server B                                                \
   384 \            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   385 \                  Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;     \
   386 \           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;             \
   387 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   388 \        ==> Key K ~: analz (sees lost Spy evs)";
   389 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   390 by (blast_tac (!claset addSEs [lemma]) 1);
   391 qed "Spy_not_see_encrypted_key";
   392 
   393 
   394 goal thy 
   395  "!!evs. [| C ~: {A,B,Server};                                           \
   396 \           Says Server B                                                \
   397 \            {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   398 \                  Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs;     \
   399 \           Says B Spy {|NA, NB, Key K|} ~: set_of_list evs;             \
   400 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   401 \        ==> Key K ~: analz (sees lost C evs)";
   402 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   403 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   404 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   405 by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
   406 qed "Agent_not_see_encrypted_key";
   407 
   408 
   409 (**** Authenticity properties relating to NB ****)
   410 
   411 (*Only OR2 can have caused such a part of a message to appear.  We do not
   412   know anything about X: it does NOT have to have the right form.*)
   413 goal thy 
   414  "!!evs. [| B ~: lost;  evs : otway lost |]                    \
   415 \        ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
   416 \             : parts (sees lost Spy evs) -->                  \
   417 \            (EX X. Says B Server                              \
   418 \             {|NA, Agent A, Agent B, X,                       \
   419 \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   420 \             : set_of_list evs)";
   421 by parts_induct_tac;
   422 by (Fake_parts_insert_tac 1);
   423 by (ALLGOALS Blast_tac);
   424 bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
   425 
   426 
   427 (** The Nonce NB uniquely identifies B's  message. **)
   428 
   429 goal thy 
   430  "!!evs. [| evs : otway lost; B ~: lost |]               \
   431 \ ==> EX NA' A'. ALL NA A.                               \
   432 \      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \
   433 \      --> NA = NA' & A = A'";
   434 by parts_induct_tac;
   435 by (Fake_parts_insert_tac 1);
   436 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   437 (*OR2: creation of new Nonce.  Move assertion into global context*)
   438 by (expand_case_tac "NB = ?y" 1);
   439 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   440 val lemma = result();
   441 
   442 goal thy 
   443  "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
   444 \                  : parts(sees lost Spy evs);         \
   445 \          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \
   446 \                  : parts(sees lost Spy evs);         \
   447 \          evs : otway lost;  B ~: lost |]             \
   448 \        ==> NC = NA & C = A";
   449 by (prove_unique_tac lemma 1);
   450 qed "unique_NB";
   451 
   452 
   453 (*If the encrypted message appears, and B has used Nonce NB,
   454   then it originated with the Server!*)
   455 goal thy 
   456  "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost |]                   \
   457 \    ==> Crypt (shrK B) {|NB, Key K|} : parts (sees lost Spy evs)        \
   458 \        --> (ALL X'. Says B Server                                      \
   459 \                       {|NA, Agent A, Agent B, X',                      \
   460 \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   461 \             : set_of_list evs                                          \
   462 \             --> Says Server B                                          \
   463 \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
   464 \                        Crypt (shrK B) {|NB, Key K|}|}                  \
   465 \                   : set_of_list evs)";
   466 by parts_induct_tac;
   467 by (Fake_parts_insert_tac 1);
   468 (*OR1: it cannot be a new Nonce, contradiction.*)
   469 by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   470 (*OR4*)
   471 by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   472 (*OR3*)
   473 by (step_tac (!claset delrules [disjCI, impCE]) 1);
   474 by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
   475 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   476                        addSEs [MPair_parts]
   477                        addDs  [unique_NB]) 2);
   478 by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
   479                        addSDs [Says_imp_sees_Spy' RS parts.Inj]
   480                        delrules [conjI, impCE] (*stop split-up*)) 1);
   481 qed_spec_mp "NB_Crypt_imp_Server_msg";
   482 
   483 
   484 (*Guarantee for B: if it gets a message with matching NB then the Server
   485   has sent the correct message.*)
   486 goal thy 
   487  "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
   488 \           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}      \
   489 \            : set_of_list evs;                                    \
   490 \           Says B Server {|NA, Agent A, Agent B, X',              \
   491 \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   492 \            : set_of_list evs |]                                  \
   493 \        ==> Says Server B                                         \
   494 \                 {|NA,                                            \
   495 \                   Crypt (shrK A) {|NA, Key K|},                  \
   496 \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   497 \                   : set_of_list evs";
   498 by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   499                        addSEs sees_Spy_partsEs) 1);
   500 qed "B_trusts_OR3";
   501 
   502 
   503 B_trusts_OR3 RS Spy_not_see_encrypted_key;
   504 
   505 
   506 goal thy 
   507  "!!evs. [| B ~: lost;  evs : otway lost |]                           \
   508 \        ==> Says Server B                                            \
   509 \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   510 \                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
   511 \            (EX X. Says B Server {|NA, Agent A, Agent B, X,          \
   512 \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   513 \            : set_of_list evs)";
   514 by (etac otway.induct 1);
   515 by (ALLGOALS Asm_simp_tac);
   516 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
   517 		       addSEs [MPair_parts, Crypt_imp_OR2]) 3);
   518 by (ALLGOALS Blast_tac);
   519 bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
   520 
   521 
   522 (*After getting and checking OR4, agent A can trust that B has been active.
   523   We could probably prove that X has the expected form, but that is not
   524   strictly necessary for authentication.*)
   525 goal thy 
   526  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   527 \            : set_of_list evs;                                    \
   528 \           Says A B {|NA, Agent A, Agent B,                       \
   529 \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   530 \            : set_of_list evs;                                    \
   531 \           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |] \
   532 \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
   533 \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   534 \            : set_of_list evs";
   535 by (blast_tac (!claset addSDs  [A_trusts_OR4]
   536                        addSEs [OR3_imp_OR2]) 1);
   537 qed "A_auths_B";