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