src/HOL/Auth/OtwayRees.ML
author paulson
Mon Jul 14 12:47:21 1997 +0200 (1997-07-14)
changeset 3519 ab0a9fbed4c0
parent 3516 470626799511
child 3543 82f33248d89d
permissions -rw-r--r--
Changing "lost" from a parameter of protocol definitions to a constant.

Advantages: no "lost" argument everywhere; fewer Vars in subgoals;
less need for specially instantiated rules
Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this
theorem was never used, and its original proof was also broken
the introduction of the "Notes" constructor.
     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|}|}      \
   213 \            : set evs;                                            \ 
   214 \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
   215 \            : set evs;                                            \
   216 \           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
   217 by (prove_unique_tac lemma 1);
   218 qed "unique_session_keys";
   219 
   220 
   221 
   222 (**** Authenticity properties relating to NA ****)
   223 
   224 (*Only OR1 can have caused such a part of a message to appear.*)
   225 goal thy 
   226  "!!evs. [| A ~: lost;  evs : otway |]                             \
   227 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}               \
   228 \             : parts (sees Spy evs) -->                           \
   229 \            Says A B {|NA, Agent A, Agent B,                      \
   230 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
   231 \             : set evs";
   232 by (parts_induct_tac 1);
   233 by (Fake_parts_insert_tac 1);
   234 qed_spec_mp "Crypt_imp_OR1";
   235 
   236 
   237 (** The Nonce NA uniquely identifies A's message. **)
   238 
   239 goal thy 
   240  "!!evs. [| evs : otway; A ~: lost |]               \
   241 \ ==> EX B'. ALL B.                                 \
   242 \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees Spy evs) \
   243 \        --> B = B'";
   244 by (parts_induct_tac 1);
   245 by (Fake_parts_insert_tac 1);
   246 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   247 (*OR1: creation of new Nonce.  Move assertion into global context*)
   248 by (expand_case_tac "NA = ?y" 1);
   249 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   250 val lemma = result();
   251 
   252 goal thy 
   253  "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (sees Spy evs); \
   254 \          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (sees Spy evs); \
   255 \          evs : otway;  A ~: lost |]                                     \
   256 \        ==> B = C";
   257 by (prove_unique_tac lemma 1);
   258 qed "unique_NA";
   259 
   260 
   261 (*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   262   OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   263   over-simplified version of this protocol: see OtwayRees_Bad.*)
   264 goal thy 
   265  "!!evs. [| A ~: lost;  evs : otway |]                      \
   266 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}        \
   267 \             : parts (sees Spy evs) -->                    \
   268 \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}  \
   269 \             ~: parts (sees Spy evs)";
   270 by (parts_induct_tac 1);
   271 by (Fake_parts_insert_tac 1);
   272 by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs
   273                                addSDs  [impOfSubs parts_insert_subset_Un]) 1));
   274 qed_spec_mp"no_nonce_OR1_OR2";
   275 
   276 
   277 (*Crucial property: If the encrypted message appears, and A has used NA
   278   to start a run, then it originated with the Server!*)
   279 goal thy 
   280  "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                 \
   281 \    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees Spy evs)      \
   282 \        --> Says A B {|NA, Agent A, Agent B,                          \
   283 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
   284 \             : set evs -->                                            \
   285 \            (EX NB. Says Server B                                     \
   286 \                 {|NA,                                                \
   287 \                   Crypt (shrK A) {|NA, Key K|},                      \
   288 \                   Crypt (shrK B) {|NB, Key K|}|}                     \
   289 \                   : set evs)";
   290 by (parts_induct_tac 1);
   291 by (Fake_parts_insert_tac 1);
   292 (*OR1: it cannot be a new Nonce, contradiction.*)
   293 by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   294 (*OR3 and OR4*) 
   295 (*OR4*)
   296 by (REPEAT (Safe_step_tac 2));
   297 by (REPEAT (blast_tac (!claset addSDs [parts_cut]) 3));
   298 by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   299                       addEs  sees_Spy_partsEs) 2);
   300 (*OR3*)  (** LEVEL 5 **)
   301 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   302 by (step_tac (!claset delrules [disjCI, impCE]) 1);
   303 by (blast_tac (!claset addSEs [MPair_parts]
   304                       addSDs [Says_imp_sees_Spy RS parts.Inj]
   305                       addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   306                       delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   307 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   308                       addSEs [MPair_parts]
   309                       addIs  [unique_NA]) 1);
   310 qed_spec_mp "NA_Crypt_imp_Server_msg";
   311 
   312 
   313 (*Corollary: if A receives B's OR4 message and the nonce NA agrees
   314   then the key really did come from the Server!  CANNOT prove this of the
   315   bad form of this protocol, even though we can prove
   316   Spy_not_see_encrypted_key*)
   317 goal thy 
   318  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   319 \            : set evs;                                            \
   320 \           Says A B {|NA, Agent A, Agent B,                       \
   321 \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   322 \            : set evs;                                            \
   323 \           A ~: lost;  A ~= Spy;  evs : otway |]                  \
   324 \        ==> EX NB. Says Server B                                  \
   325 \                     {|NA,                                        \
   326 \                       Crypt (shrK A) {|NA, Key K|},              \
   327 \                       Crypt (shrK B) {|NB, Key K|}|}             \
   328 \                       : set evs";
   329 by (blast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   330                        addEs  sees_Spy_partsEs) 1);
   331 qed "A_trusts_OR4";
   332 
   333 
   334 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   335     Does not in itself guarantee security: an attack could violate 
   336     the premises, e.g. by having A=Spy **)
   337 
   338 goal thy 
   339  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway |]                    \
   340 \        ==> Says Server B                                            \
   341 \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   342 \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
   343 \            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
   344 \            Key K ~: analz (sees Spy evs)";
   345 by (etac otway.induct 1);
   346 by analz_sees_tac;
   347 by (ALLGOALS
   348     (asm_simp_tac (!simpset addcongs [conj_cong] 
   349                             addsimps [analz_insert_eq, not_parts_not_analz, 
   350 				      analz_insert_freshK]
   351                             setloop split_tac [expand_if])));
   352 (*Oops*)
   353 by (blast_tac (!claset addSDs [unique_session_keys]) 4);
   354 (*OR4*) 
   355 by (Blast_tac 3);
   356 (*OR3*)
   357 by (blast_tac (!claset addSEs sees_Spy_partsEs
   358                        addIs [impOfSubs analz_subset_parts]) 2);
   359 (*Fake*) 
   360 by (spy_analz_tac 1);
   361 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   362 
   363 goal thy 
   364  "!!evs. [| Says Server B                                           \
   365 \            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   366 \                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
   367 \           Says B Spy {|NA, NB, Key K|} ~: set evs;                \
   368 \           A ~: lost;  B ~: lost;  evs : otway |]                  \
   369 \        ==> Key K ~: analz (sees Spy evs)";
   370 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   371 by (blast_tac (!claset addSEs [lemma]) 1);
   372 qed "Spy_not_see_encrypted_key";
   373 
   374 
   375 (**** Authenticity properties relating to NB ****)
   376 
   377 (*Only OR2 can have caused such a part of a message to appear.  We do not
   378   know anything about X: it does NOT have to have the right form.*)
   379 goal thy 
   380  "!!evs. [| B ~: lost;  evs : otway |]                         \
   381 \        ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
   382 \             : parts (sees Spy evs) -->                       \
   383 \            (EX X. Says B Server                              \
   384 \             {|NA, Agent A, Agent B, X,                       \
   385 \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   386 \             : set evs)";
   387 by (parts_induct_tac 1);
   388 by (Fake_parts_insert_tac 1);
   389 by (ALLGOALS Blast_tac);
   390 bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
   391 
   392 
   393 (** The Nonce NB uniquely identifies B's  message. **)
   394 
   395 goal thy 
   396  "!!evs. [| evs : otway; B ~: lost |]                    \
   397 \ ==> EX NA' A'. ALL NA A.                               \
   398 \      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees Spy evs) \
   399 \      --> NA = NA' & A = A'";
   400 by (parts_induct_tac 1);
   401 by (Fake_parts_insert_tac 1);
   402 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   403 (*OR2: creation of new Nonce.  Move assertion into global context*)
   404 by (expand_case_tac "NB = ?y" 1);
   405 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   406 val lemma = result();
   407 
   408 goal thy 
   409  "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
   410 \                  : parts(sees Spy evs);         \
   411 \          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \
   412 \                  : parts(sees Spy evs);         \
   413 \          evs : otway;  B ~: lost |]             \
   414 \        ==> NC = NA & C = A";
   415 by (prove_unique_tac lemma 1);
   416 qed "unique_NB";
   417 
   418 
   419 (*If the encrypted message appears, and B has used Nonce NB,
   420   then it originated with the Server!*)
   421 goal thy 
   422  "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway |]                        \
   423 \    ==> Crypt (shrK B) {|NB, Key K|} : parts (sees Spy evs)             \
   424 \        --> (ALL X'. Says B Server                                      \
   425 \                       {|NA, Agent A, Agent B, X',                      \
   426 \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   427 \             : set evs                                                  \
   428 \             --> Says Server B                                          \
   429 \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
   430 \                        Crypt (shrK B) {|NB, Key K|}|}                  \
   431 \                   : set evs)";
   432 by (parts_induct_tac 1);
   433 by (Fake_parts_insert_tac 1);
   434 (*OR1: it cannot be a new Nonce, contradiction.*)
   435 by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1);
   436 (*OR4*)
   437 by (blast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   438 (*OR3*)
   439 by (step_tac (!claset delrules [disjCI, impCE]) 1);
   440 by (blast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
   441 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   442                        addSEs [MPair_parts]
   443                        addDs  [unique_NB]) 2);
   444 by (blast_tac (!claset addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)]
   445                        addSDs [Says_imp_sees_Spy RS parts.Inj]
   446                        delrules [conjI, impCE] (*stop split-up*)) 1);
   447 qed_spec_mp "NB_Crypt_imp_Server_msg";
   448 
   449 
   450 (*Guarantee for B: if it gets a message with matching NB then the Server
   451   has sent the correct message.*)
   452 goal thy 
   453  "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway;                    \
   454 \           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}      \
   455 \            : set evs;                                            \
   456 \           Says B Server {|NA, Agent A, Agent B, X',              \
   457 \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   458 \            : set evs |]                                          \
   459 \        ==> Says Server B                                         \
   460 \                 {|NA,                                            \
   461 \                   Crypt (shrK A) {|NA, Key K|},                  \
   462 \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   463 \                   : set evs";
   464 by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   465                        addSEs sees_Spy_partsEs) 1);
   466 qed "B_trusts_OR3";
   467 
   468 
   469 B_trusts_OR3 RS Spy_not_see_encrypted_key;
   470 
   471 
   472 goal thy 
   473  "!!evs. [| B ~: lost;  evs : otway |]                           \
   474 \        ==> Says Server B                                       \
   475 \              {|NA, Crypt (shrK A) {|NA, Key K|},               \
   476 \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->    \
   477 \            (EX X. Says B Server {|NA, Agent A, Agent B, X,     \
   478 \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   479 \            : set evs)";
   480 by (etac otway.induct 1);
   481 by (ALLGOALS Asm_simp_tac);
   482 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
   483 		       addSEs [MPair_parts, Crypt_imp_OR2]) 3);
   484 by (ALLGOALS Blast_tac);
   485 bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
   486 
   487 
   488 (*After getting and checking OR4, agent A can trust that B has been active.
   489   We could probably prove that X has the expected form, but that is not
   490   strictly necessary for authentication.*)
   491 goal thy 
   492  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;       \
   493 \           Says A B {|NA, Agent A, Agent B,                                \
   494 \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   495 \           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway |]               \
   496 \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,              \
   497 \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   498 \            : set evs";
   499 by (blast_tac (!claset addSDs  [A_trusts_OR4]
   500                        addSEs [OR3_imp_OR2]) 1);
   501 qed "A_auths_B";