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