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