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