src/HOL/Auth/OtwayRees.ML
author nipkow
Fri Oct 17 15:25:12 1997 +0200 (1997-10-17)
changeset 3919 c036caebfc75
parent 3730 6933d20f335f
child 3961 6a8996fb7d99
permissions -rw-r--r--
setloop split_tac -> addsplits
     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 (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 (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 (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 addIs [impOfSubs analz_subset_parts]
   114                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   115                       impOfSubs (parts_insert_subset_Un 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 2);
   177 (*Base*)
   178 by (Blast_tac 1);
   179 qed_spec_mp "analz_image_freshK";
   180 
   181 
   182 goal thy
   183  "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
   184 \        Key K : analz (insert (Key KAB) (spies evs)) =  \
   185 \        (K = KAB | Key K : analz (spies evs))";
   186 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   187 qed "analz_insert_freshK";
   188 
   189 
   190 (*** The Key K uniquely identifies the Server's  message. **)
   191 
   192 goal thy 
   193  "!!evs. evs : otway ==>                                                  \
   194 \   EX B' NA' NB' X'. ALL B NA NB X.                                      \
   195 \     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs -->     \
   196 \     B=B' & NA=NA' & NB=NB' & X=X'";
   197 by (etac otway.induct 1);
   198 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   199 by (ALLGOALS Clarify_tac);
   200 (*Remaining cases: OR3 and OR4*)
   201 by (ex_strip_tac 2);
   202 by (Best_tac 2);
   203 by (expand_case_tac "K = ?y" 1);
   204 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   205 (*...we assume X is a recent message, and handle this case by contradiction*)
   206 by (blast_tac (!claset addSEs spies_partsEs
   207                        delrules [conjI] (*no split-up into 4 subgoals*)) 1);
   208 val lemma = result();
   209 
   210 goal thy 
   211  "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
   212 \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
   213 \           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
   214 by (prove_unique_tac lemma 1);
   215 qed "unique_session_keys";
   216 
   217 
   218 
   219 (**** Authenticity properties relating to NA ****)
   220 
   221 (*Only OR1 can have caused such a part of a message to appear.*)
   222 goal thy 
   223  "!!evs. [| A ~: bad;  evs : otway |]                             \
   224 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   225 \            Says A B {|NA, Agent A, Agent B,                      \
   226 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
   227 \             : set evs";
   228 by (parts_induct_tac 1);
   229 by (Fake_parts_insert_tac 1);
   230 qed_spec_mp "Crypt_imp_OR1";
   231 
   232 
   233 (** The Nonce NA uniquely identifies A's message. **)
   234 
   235 goal thy 
   236  "!!evs. [| evs : otway; A ~: bad |]               \
   237 \ ==> EX B'. ALL B.                                 \
   238 \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \
   239 \        --> B = B'";
   240 by (parts_induct_tac 1);
   241 by (Fake_parts_insert_tac 1);
   242 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   243 (*OR1: creation of new Nonce.  Move assertion into global context*)
   244 by (expand_case_tac "NA = ?y" 1);
   245 by (blast_tac (!claset addSEs spies_partsEs) 1);
   246 val lemma = result();
   247 
   248 goal thy 
   249  "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
   250 \          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (spies evs); \
   251 \          evs : otway;  A ~: bad |]                                   \
   252 \        ==> B = C";
   253 by (prove_unique_tac lemma 1);
   254 qed "unique_NA";
   255 
   256 
   257 (*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   258   OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   259   over-simplified version of this protocol: see OtwayRees_Bad.*)
   260 goal thy 
   261  "!!evs. [| A ~: bad;  evs : otway |]                      \
   262 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   263 \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}  \
   264 \             ~: parts (spies evs)";
   265 by (parts_induct_tac 1);
   266 by (Fake_parts_insert_tac 1);
   267 by (REPEAT (blast_tac (!claset addSEs spies_partsEs
   268                                addSDs  [impOfSubs parts_insert_subset_Un]) 1));
   269 qed_spec_mp"no_nonce_OR1_OR2";
   270 
   271 
   272 (*Crucial property: If the encrypted message appears, and A has used NA
   273   to start a run, then it originated with the Server!*)
   274 goal thy 
   275  "!!evs. [| A ~: bad;  A ~= Spy;  evs : otway |]                      \
   276 \    ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs)              \
   277 \        --> Says A B {|NA, Agent A, Agent B,                          \
   278 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
   279 \             : set evs -->                                            \
   280 \            (EX NB. Says Server B                                     \
   281 \                 {|NA,                                                \
   282 \                   Crypt (shrK A) {|NA, Key K|},                      \
   283 \                   Crypt (shrK B) {|NB, Key K|}|}                     \
   284 \                   : set evs)";
   285 by (parts_induct_tac 1);
   286 by (Fake_parts_insert_tac 1);
   287 (*OR1: it cannot be a new Nonce, contradiction.*)
   288 by (blast_tac (!claset addSIs [parts_insertI] addSEs spies_partsEs) 1);
   289 (*OR3 and OR4*)
   290 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   291 by (rtac conjI 1);
   292 by (ALLGOALS Clarify_tac);
   293 (*OR4*)
   294 by (blast_tac (!claset addSIs [Crypt_imp_OR1]
   295                        addEs  spies_partsEs) 3);
   296 (*OR3, two cases*)  (** LEVEL 5 **)
   297 by (blast_tac (!claset addSEs [MPair_parts]
   298                        addSDs [Says_imp_spies RS parts.Inj]
   299                        addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   300                        delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   301 by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
   302                        addSEs [MPair_parts]
   303                        addIs  [unique_NA]) 1);
   304 qed_spec_mp "NA_Crypt_imp_Server_msg";
   305 
   306 
   307 (*Corollary: if A receives B's OR4 message and the nonce NA agrees
   308   then the key really did come from the Server!  CANNOT prove this of the
   309   bad form of this protocol, even though we can prove
   310   Spy_not_see_encrypted_key*)
   311 goal thy 
   312  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
   313 \           Says A  B {|NA, Agent A, Agent B,                       \
   314 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   315 \           A ~: bad;  A ~= Spy;  evs : otway |]                  \
   316 \        ==> EX NB. Says Server B                                  \
   317 \                     {|NA,                                        \
   318 \                       Crypt (shrK A) {|NA, Key K|},              \
   319 \                       Crypt (shrK B) {|NB, Key K|}|}             \
   320 \                       : set evs";
   321 by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   322                        addEs  spies_partsEs) 1);
   323 qed "A_trusts_OR4";
   324 
   325 
   326 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   327     Does not in itself guarantee security: an attack could violate 
   328     the premises, e.g. by having A=Spy **)
   329 
   330 goal thy 
   331  "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                    \
   332 \        ==> Says Server B                                            \
   333 \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   334 \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
   335 \            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
   336 \            Key K ~: analz (spies evs)";
   337 by (etac otway.induct 1);
   338 by analz_spies_tac;
   339 by (ALLGOALS
   340     (asm_simp_tac (!simpset addcongs [conj_cong] 
   341                             addsimps [analz_insert_eq, analz_insert_freshK]
   342                             addsplits [expand_if])));
   343 (*Oops*)
   344 by (blast_tac (!claset addSDs [unique_session_keys]) 4);
   345 (*OR4*) 
   346 by (Blast_tac 3);
   347 (*OR3*)
   348 by (blast_tac (!claset addSEs spies_partsEs
   349                        addIs [impOfSubs analz_subset_parts]) 2);
   350 (*Fake*) 
   351 by (spy_analz_tac 1);
   352 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   353 
   354 goal thy 
   355  "!!evs. [| Says Server B                                           \
   356 \            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   357 \                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
   358 \           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
   359 \           A ~: bad;  B ~: bad;  evs : otway |]                  \
   360 \        ==> Key K ~: analz (spies evs)";
   361 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   362 by (blast_tac (!claset addSEs [lemma]) 1);
   363 qed "Spy_not_see_encrypted_key";
   364 
   365 
   366 (**** Authenticity properties relating to NB ****)
   367 
   368 (*Only OR2 can have caused such a part of a message to appear.  We do not
   369   know anything about X: it does NOT have to have the right form.*)
   370 goal thy 
   371  "!!evs. [| B ~: bad;  evs : otway |]                         \
   372 \        ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
   373 \             : parts (spies evs) -->                       \
   374 \            (EX X. Says B Server                              \
   375 \             {|NA, Agent A, Agent B, X,                       \
   376 \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   377 \             : set evs)";
   378 by (parts_induct_tac 1);
   379 by (Fake_parts_insert_tac 1);
   380 by (ALLGOALS Blast_tac);
   381 bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
   382 
   383 
   384 (** The Nonce NB uniquely identifies B's  message. **)
   385 
   386 goal thy 
   387  "!!evs. [| evs : otway; B ~: bad |]                    \
   388 \ ==> EX NA' A'. ALL NA A.                               \
   389 \      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
   390 \      --> NA = NA' & A = A'";
   391 by (parts_induct_tac 1);
   392 by (Fake_parts_insert_tac 1);
   393 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   394 (*OR2: creation of new Nonce.  Move assertion into global context*)
   395 by (expand_case_tac "NB = ?y" 1);
   396 by (blast_tac (!claset addSEs spies_partsEs) 1);
   397 val lemma = result();
   398 
   399 goal thy 
   400  "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
   401 \          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(spies evs); \
   402 \          evs : otway;  B ~: bad |]             \
   403 \        ==> NC = NA & C = A";
   404 by (prove_unique_tac lemma 1);
   405 qed "unique_NB";
   406 
   407 
   408 (*If the encrypted message appears, and B has used Nonce NB,
   409   then it originated with the Server!*)
   410 goal thy 
   411  "!!evs. [| B ~: bad;  B ~= Spy;  evs : otway |]                        \
   412 \    ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs)             \
   413 \        --> (ALL X'. Says B Server                                      \
   414 \                       {|NA, Agent A, Agent B, X',                      \
   415 \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   416 \             : set evs                                                  \
   417 \             --> Says Server B                                          \
   418 \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
   419 \                        Crypt (shrK B) {|NB, Key K|}|}                  \
   420 \                   : set evs)";
   421 by (parts_induct_tac 1);
   422 by (Fake_parts_insert_tac 1);
   423 (*OR1: it cannot be a new Nonce, contradiction.*)
   424 by (blast_tac (!claset addSIs [parts_insertI] addSEs spies_partsEs) 1);
   425 (*OR4*)
   426 by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   427 (*OR3*)
   428 by (safe_tac (!claset delrules [disjCI, impCE]));
   429 by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
   430 by (blast_tac (!claset addSDs [Says_imp_spies RS parts.Inj]
   431                        addSEs [MPair_parts]
   432                        addDs  [unique_NB]) 2);
   433 by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
   434                        addSDs [Says_imp_spies RS parts.Inj]
   435                        delrules [conjI, impCE] (*stop split-up*)) 1);
   436 qed_spec_mp "NB_Crypt_imp_Server_msg";
   437 
   438 
   439 (*Guarantee for B: if it gets a message with matching NB then the Server
   440   has sent the correct message.*)
   441 goal thy 
   442  "!!evs. [| B ~: bad;  B ~= Spy;  evs : otway;                    \
   443 \           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
   444 \           Says B Server {|NA, Agent A, Agent B, X',              \
   445 \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   446 \            : set evs |]                                          \
   447 \        ==> Says Server B                                         \
   448 \                 {|NA,                                            \
   449 \                   Crypt (shrK A) {|NA, Key K|},                  \
   450 \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   451 \                   : set evs";
   452 by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   453                        addSEs spies_partsEs) 1);
   454 qed "B_trusts_OR3";
   455 
   456 
   457 B_trusts_OR3 RS Spy_not_see_encrypted_key;
   458 
   459 
   460 goal thy 
   461  "!!evs. [| B ~: bad;  evs : otway |]                           \
   462 \        ==> Says Server B                                       \
   463 \              {|NA, Crypt (shrK A) {|NA, Key K|},               \
   464 \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->    \
   465 \            (EX X. Says B Server {|NA, Agent A, Agent B, X,     \
   466 \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   467 \            : set evs)";
   468 by (etac otway.induct 1);
   469 by (ALLGOALS Asm_simp_tac);
   470 by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
   471 		       addSEs [MPair_parts, Crypt_imp_OR2]) 3);
   472 by (ALLGOALS Blast_tac);
   473 bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
   474 
   475 
   476 (*After getting and checking OR4, agent A can trust that B has been active.
   477   We could probably prove that X has the expected form, but that is not
   478   strictly necessary for authentication.*)
   479 goal thy 
   480  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;       \
   481 \           Says A B {|NA, Agent A, Agent B,                                \
   482 \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   483 \           A ~: bad;  A ~= Spy;  B ~: bad;  evs : otway |]               \
   484 \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,              \
   485 \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   486 \            : set evs";
   487 by (blast_tac (!claset addSDs  [A_trusts_OR4]
   488                        addSEs [OR3_imp_OR2]) 1);
   489 qed "A_auths_B";