src/HOL/Auth/OtwayRees_AN.ML
author paulson
Thu Oct 10 18:40:34 1996 +0200 (1996-10-10)
changeset 2090 307ebbbec862
child 2106 1a52e2c5897e
permissions -rw-r--r--
Abadi and Needham's variant of Otway-Rees
     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 Simplified version with minimal encryption but explicit messages
     9 
    10 From page 11 of
    11   Abadi and Needham.  Prudent Engineering Practice for Cryptographic Protocols.
    12   IEEE Trans. SE 22 (1), 1996
    13 *)
    14 
    15 open OtwayRees_AN;
    16 
    17 proof_timing:=true;
    18 HOL_quantifiers := false;
    19 
    20 
    21 (*Weak liveness: 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 lost.          \
    25 \             Says B A (Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A)) \
    26 \             : set_of_list 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 (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    30 by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    31 by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    32 result();
    33 
    34 
    35 (**** Inductive proofs about otway ****)
    36 
    37 goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
    38 by (rtac subsetI 1);
    39 by (etac otway.induct 1);
    40 by (REPEAT_FIRST
    41     (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    42                               :: otway.intrs))));
    43 qed "otway_mono";
    44 
    45 (*Nobody sends themselves messages*)
    46 goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
    47 by (etac otway.induct 1);
    48 by (Auto_tac());
    49 qed_spec_mp "not_Says_to_self";
    50 Addsimps [not_Says_to_self];
    51 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    52 
    53 
    54 (** For reasoning about the encrypted portion of messages **)
    55 
    56 goal thy "!!evs. Says S B {|X, X'|} : set_of_list evs ==> \
    57 \                X : analz (sees lost Spy evs)";
    58 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    59 qed "OR4_analz_sees_Spy";
    60 
    61 goal thy "!!evs. Says B' A (Crypt {|N,Agent A,B,K|} K') : set_of_list evs ==> \
    62 \                K : parts (sees lost Spy evs)";
    63 by (fast_tac (!claset addSEs partsEs
    64                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    65 qed "Reveal_parts_sees_Spy";
    66 
    67 (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    68   argument as for the Fake case.  This is possible for most, but not all,
    69   proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    70   messages originate from the Spy. *)
    71 
    72 bind_thm ("OR4_parts_sees_Spy",
    73           OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    74 
    75 (*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
    76   harder to complete, since simplification does less for us.*)
    77 val parts_Fake_tac = 
    78     forw_inst_tac [("lost","lost")] OR4_parts_sees_Spy 6 THEN
    79     forw_inst_tac [("lost","lost")] Reveal_parts_sees_Spy 7;
    80 
    81 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    82 fun parts_induct_tac i = SELECT_GOAL
    83     (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
    84 	     (*Fake message*)
    85 	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    86 					   impOfSubs Fake_parts_insert]
    87                                     addss (!simpset)) 2)) THEN
    88      (*Base case*)
    89      fast_tac (!claset addss (!simpset)) 1 THEN
    90      ALLGOALS Asm_simp_tac) i;
    91 
    92 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    93     sends messages containing X! **)
    94 
    95 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    96 goal thy 
    97  "!!evs. [| evs : otway lost;  A ~: lost |]    \
    98 \        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
    99 by (parts_induct_tac 1);
   100 by (Auto_tac());
   101 qed "Spy_not_see_shrK";
   102 
   103 bind_thm ("Spy_not_analz_shrK",
   104           [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
   105 
   106 Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
   107 
   108 (*We go to some trouble to preserve R in the 3rd and 4th subgoals
   109   As usual fast_tac cannot be used because it uses the equalities too soon*)
   110 val major::prems = 
   111 goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
   112 \             evs : otway lost;                                 \
   113 \             A:lost ==> R                                  \
   114 \           |] ==> R";
   115 by (rtac ccontr 1);
   116 by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
   117 by (swap_res_tac prems 2);
   118 by (ALLGOALS (fast_tac (!claset addIs prems)));
   119 qed "Spy_see_shrK_E";
   120 
   121 bind_thm ("Spy_analz_shrK_E", 
   122           analz_subset_parts RS subsetD RS Spy_see_shrK_E);
   123 
   124 AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
   125 
   126 
   127 (*** Future keys can't be seen or used! ***)
   128 
   129 (*Nobody can have SEEN keys that will be generated in the future.
   130   This has to be proved anew for each protocol description,
   131   but should go by similar reasoning every time.  Hardest case is the
   132   standard Fake rule.  
   133       The Union over C is essential for the induction! *)
   134 goal thy "!!evs. evs : otway lost ==> \
   135 \                length evs <= length evs' --> \
   136 \                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
   137 by (parts_induct_tac 1);
   138 by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   139                                            impOfSubs parts_insert_subset_Un,
   140                                            Suc_leD]
   141                                     addss (!simpset))));
   142 val lemma = result();
   143 
   144 (*Variant needed for the main theorem below*)
   145 goal thy 
   146  "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
   147 \        ==> Key (newK evs') ~: parts (sees lost C evs)";
   148 by (fast_tac (!claset addDs [lemma]) 1);
   149 qed "new_keys_not_seen";
   150 Addsimps [new_keys_not_seen];
   151 
   152 (*Another variant: old messages must contain old keys!*)
   153 goal thy 
   154  "!!evs. [| Says A B X : set_of_list evs;  \
   155 \           Key (newK evt) : parts {X};    \
   156 \           evs : otway lost                 \
   157 \        |] ==> length evt < length evs";
   158 by (rtac ccontr 1);
   159 by (dtac leI 1);
   160 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   161                       addIs  [impOfSubs parts_mono]) 1);
   162 qed "Says_imp_old_keys";
   163 
   164 
   165 (*** Future nonces can't be seen or used! [proofs resemble those above] ***)
   166 
   167 goal thy "!!evs. evs : otway lost ==> \
   168 \                length evs <= length evt --> \
   169 \                Nonce (newN evt) ~: (UN C. parts (sees lost C evs))";
   170 by (etac otway.induct 1);
   171 (*auto_tac does not work here, as it performs safe_tac first*)
   172 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert2]
   173                                      addcongs [disj_cong])));
   174 by (REPEAT_FIRST (fast_tac (!claset 
   175                               addSEs partsEs
   176                               addSDs  [Says_imp_sees_Spy RS parts.Inj]
   177                               addDs  [impOfSubs analz_subset_parts,
   178                                       impOfSubs parts_insert_subset_Un,
   179                                       Suc_leD]
   180                               addss (!simpset))));
   181 val lemma = result();
   182 
   183 (*Variant needed for the main theorem below*)
   184 goal thy 
   185  "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
   186 \        ==> Nonce (newN evs') ~: parts (sees lost C evs)";
   187 by (fast_tac (!claset addDs [lemma]) 1);
   188 qed "new_nonces_not_seen";
   189 Addsimps [new_nonces_not_seen];
   190 
   191 (*Another variant: old messages must contain old nonces!*)
   192 goal thy 
   193  "!!evs. [| Says A B X : set_of_list evs;  \
   194 \           Nonce (newN evt) : parts {X};    \
   195 \           evs : otway lost                 \
   196 \        |] ==> length evt < length evs";
   197 by (rtac ccontr 1);
   198 by (dtac leI 1);
   199 by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
   200                       addIs  [impOfSubs parts_mono]) 1);
   201 qed "Says_imp_old_nonces";
   202 
   203 
   204 (*Nobody can have USED keys that will be generated in the future.
   205   ...very like new_keys_not_seen*)
   206 goal thy "!!evs. evs : otway lost ==> \
   207 \                length evs <= length evs' --> \
   208 \                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
   209 by (parts_induct_tac 1);
   210 (*OR1 and OR3*)
   211 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   212 (*Fake, OR2, OR4: these messages send unknown (X) components*)
   213 by (EVERY 
   214     (map
   215      (best_tac
   216       (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   217                       impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   218                       Suc_leD]
   219                addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   220                addss (!simpset)))
   221      [3,2,1]));
   222 (*Reveal: dummy message*)
   223 by (best_tac (!claset addEs  [new_keys_not_seen RSN(2,rev_notE)]
   224                       addIs  [less_SucI, impOfSubs keysFor_mono]
   225                       addss (!simpset addsimps [le_def])) 1);
   226 val lemma = result();
   227 
   228 goal thy 
   229  "!!evs. [| evs : otway lost;  length evs <= length evs' |]    \
   230 \        ==> newK evs' ~: keysFor (parts (sees lost C evs))";
   231 by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1);
   232 qed "new_keys_not_used";
   233 
   234 bind_thm ("new_keys_not_analzd",
   235           [analz_subset_parts RS keysFor_mono,
   236            new_keys_not_used] MRS contra_subsetD);
   237 
   238 Addsimps [new_keys_not_used, new_keys_not_analzd];
   239 
   240 
   241 
   242 (*** Proofs involving analz ***)
   243 
   244 (*Describes the form of Key K when the following message is sent.  The use of
   245   "parts" strengthens the induction hyp for proving the Fake case.  The
   246   assumption A ~: lost prevents its being a Faked message.  (Based
   247   on NS_Shared/Says_S_message_form) *)
   248 goal thy
   249  "!!evs. evs: otway lost ==>                                           \
   250 \        Crypt {|N, Agent A, B, Key K|} (shrK A) : parts (sees lost Spy evs)  \
   251 \        --> A ~: lost --> (EX evt: otway lost. K = newK evt)";
   252 by (parts_induct_tac 1);
   253 by (Auto_tac());
   254 qed_spec_mp "Reveal_message_lemma";
   255 
   256 (*EITHER describes the form of Key K when the following message is sent, 
   257   OR     reduces it to the Fake case.*)
   258 
   259 goal thy 
   260  "!!evs. [| Says B' A (Crypt {|N, Agent A, B, Key K|} (shrK A)) \
   261 \            : set_of_list evs;                                 \
   262 \           evs : otway lost |]                                 \
   263 \        ==> (EX evt: otway lost. K = newK evt)                 \
   264 \          | Key K : analz (sees lost Spy evs)";
   265 br (Reveal_message_lemma RS disjCI) 1;
   266 ba 1;
   267 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   268                       addDs [impOfSubs analz_subset_parts]) 1);
   269 by (fast_tac (!claset addSDs [Says_Crypt_lost]) 1);
   270 qed "Reveal_message_form";
   271 
   272 
   273 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   274 val analz_Fake_tac = 
   275     dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   276     forw_inst_tac [("lost","lost")] Reveal_message_form 7;
   277 
   278 
   279 (****
   280  The following is to prove theorems of the form
   281 
   282           Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   283           Key K : analz (sees lost Spy evs)
   284 
   285  A more general formula must be proved inductively.
   286 
   287 ****)
   288 
   289 
   290 (*NOT useful in this form, but it says that session keys are not used
   291   to encrypt messages containing other keys, in the actual protocol.
   292   We require that agents should behave like this subsequently also.*)
   293 goal thy 
   294  "!!evs. evs : otway lost ==> \
   295 \        (Crypt X (newK evt)) : parts (sees lost Spy evs) & \
   296 \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
   297 by (etac otway.induct 1);
   298 by parts_Fake_tac;
   299 by (ALLGOALS Asm_simp_tac);
   300 (*Deals with Faked messages*)
   301 by (best_tac (!claset addSEs partsEs
   302                       addDs [impOfSubs parts_insert_subset_Un]
   303                       addss (!simpset)) 2);
   304 (*Base case and Reveal*)
   305 by (Auto_tac());
   306 result();
   307 
   308 
   309 (** Session keys are not used to encrypt other session keys **)
   310 
   311 (*The equality makes the induction hypothesis easier to apply*)
   312 goal thy  
   313  "!!evs. evs : otway lost ==> \
   314 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   315 \           (K : newK``E | Key K : analz (sees lost Spy evs))";
   316 by (etac otway.induct 1);
   317 by analz_Fake_tac;
   318 by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   319 by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
   320 by (ALLGOALS (*Takes 28 secs*)
   321     (asm_simp_tac 
   322      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   323                          @ pushes)
   324                setloop split_tac [expand_if])));
   325 (** LEVEL 5 **)
   326 (*Reveal case 2, OR4, OR2, Fake*) 
   327 by (EVERY (map spy_analz_tac [6, 4, 2]));
   328 (*Reveal case 1, OR3, Base*)
   329 by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   330 qed_spec_mp "analz_image_newK";
   331 
   332 
   333 goal thy
   334  "!!evs. evs : otway lost ==>                               \
   335 \        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   336 \        (K = newK evt | Key K : analz (sees lost Spy evs))";
   337 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   338                                    insert_Key_singleton]) 1);
   339 by (Fast_tac 1);
   340 qed "analz_insert_Key_newK";
   341 
   342 
   343 (*** The Key K uniquely identifies the Server's  message. **)
   344 
   345 fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   346 
   347 goal thy 
   348  "!!evs. evs : otway lost ==>                      \
   349 \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   350 \       Says Server B \
   351 \         {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   352 \           Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs  \
   353 \       --> A=A' & B=B' & NA=NA' & NB=NB'";
   354 by (etac otway.induct 1);
   355 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   356 by (Step_tac 1);
   357 (*Remaining cases: OR3 and OR4*)
   358 by (ex_strip_tac 2);
   359 by (Fast_tac 2);
   360 by (expand_case_tac "K = ?y" 1);
   361 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   362 (*...we assume X is a very new message, and handle this case by contradiction*)
   363 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   364                       delrules [conjI]    (*prevent split-up into 4 subgoals*)
   365                       addss (!simpset addsimps [parts_insertI])) 1);
   366 val lemma = result();
   367 
   368 
   369 goal thy 
   370 "!!evs. [| Says Server B                                           \
   371 \            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),         \
   372 \              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|}        \
   373 \           : set_of_list evs;                                     \
   374 \          Says Server B'                                          \
   375 \            {|Crypt {|NA', Agent A', Agent B', K|} (shrK A'),     \
   376 \              Crypt {|NB', Agent A', Agent B', K|} (shrK B')|}    \
   377 \           : set_of_list evs;                                     \
   378 \          evs : otway lost |]                                     \
   379 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   380 by (dtac lemma 1);
   381 by (REPEAT (etac exE 1));
   382 (*Duplicate the assumption*)
   383 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   384 by (fast_tac (!claset addSDs [spec]) 1);
   385 qed "unique_session_keys";
   386 
   387 
   388 
   389 (**** Authenticity properties relating to NA ****)
   390 
   391 (*If the encrypted message appears then it originated with the Server!*)
   392 goal thy 
   393  "!!evs. [| A ~: lost;  evs : otway lost |]                 \
   394 \ ==> Crypt {|NA, Agent A, Agent B, Key K|} (shrK A)        \
   395 \      : parts (sees lost Spy evs)                          \
   396 \     --> (EX NB. Says Server B                                     \
   397 \                  {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   398 \                    Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   399 \                  : set_of_list evs)";
   400 by (parts_induct_tac 1);
   401 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   402 (*OR3*)
   403 by (Fast_tac 1);
   404 qed_spec_mp "NA_Crypt_imp_Server_msg";
   405 
   406 
   407 (*Corollary: if A receives B's OR4 message and the nonce NA agrees
   408   then the key really did come from the Server!  CANNOT prove this of the
   409   bad form of this protocol, even though we can prove
   410   Spy_not_see_encrypted_key*)
   411 goal thy 
   412  "!!evs. [| Says B' A (Crypt {|NA, Agent A, Agent B, Key K|} (shrK A))  \
   413 \            : set_of_list evs;                                         \
   414 \           A ~: lost;  evs : otway lost |]                             \
   415 \        ==> EX NB. Says Server B                                       \
   416 \                    {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),  \
   417 \                      Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \
   418 \                   : set_of_list evs";
   419 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   420                       addEs  partsEs
   421                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   422 qed "A_trust_OR4";
   423 
   424 
   425 (*Describes the form of K and NA when the Server sends this message.*)
   426 goal thy 
   427  "!!evs. [| Says Server B \
   428 \           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   429 \             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   430 \           evs : otway lost |]                                        \
   431 \        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
   432 \            (EX i. NA = Nonce i) &                  \
   433 \            (EX j. NB = Nonce j)";
   434 by (etac rev_mp 1);
   435 by (etac otway.induct 1);
   436 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   437 qed "Says_Server_message_form";
   438 
   439 
   440 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   441     Does not in itself guarantee security: an attack could violate 
   442     the premises, e.g. by having A=Spy **)
   443 
   444 goal thy 
   445  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost;  evt : otway lost |] \
   446 \        ==> Says Server B                                                 \
   447 \             {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),            \
   448 \               Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}           \
   449 \            : set_of_list evs -->                                         \
   450 \            Says A Spy {|NA, Key K|} ~: set_of_list evs -->               \
   451 \            Key K ~: analz (sees lost Spy evs)";
   452 by (etac otway.induct 1);
   453 by analz_Fake_tac;
   454 by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   455 by (ALLGOALS
   456     (asm_full_simp_tac 
   457      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   458                           analz_insert_Key_newK] @ pushes)
   459                setloop split_tac [expand_if])));
   460 (** LEVEL 4 **)
   461 (*OR3*)
   462 by (fast_tac (!claset addSIs [parts_insertI]
   463                       addEs [Says_imp_old_keys RS less_irrefl]
   464                       addss (!simpset addsimps [parts_insert2])) 2);
   465 (*Reveal case 2, OR4, Fake*) 
   466 by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   467 (*Reveal case 1*) (** LEVEL 6 **)
   468 by (excluded_middle_tac "Aa : lost" 1);
   469 (*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
   470 by (dtac (Says_imp_sees_Spy RS analz.Inj) 2);
   471 by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 2);
   472 (*So now we have  Aa ~: lost *)
   473 by (dtac A_trust_OR4 1);
   474 by (REPEAT (assume_tac 1));
   475 by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   476 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   477 
   478 goal thy 
   479  "!!evs. [| Says Server B \
   480 \           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   481 \             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   482 \           Says A Spy {|NA, K|} ~: set_of_list evs;                     \
   483 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   484 \        ==> K ~: analz (sees lost Spy evs)";
   485 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   486 by (fast_tac (!claset addSEs [lemma]) 1);
   487 qed "Spy_not_see_encrypted_key";
   488 
   489 
   490 goal thy 
   491  "!!evs. [| C ~: {A,B,Server};                                           \
   492 \           Says Server B \
   493 \           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   494 \             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   495 \           Says A Spy {|NA, K|} ~: set_of_list evs;                     \
   496 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   497 \        ==> K ~: analz (sees lost C evs)";
   498 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   499 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   500 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   501 by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
   502 qed "Agent_not_see_encrypted_key";
   503 
   504 
   505 (**** Authenticity properties relating to NB ****)
   506 
   507 (*If the encrypted message appears then it originated with the Server!*)
   508 goal thy 
   509  "!!evs. [| B ~: lost;  evs : otway lost |]                   \
   510 \    ==> Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)       \
   511 \         : parts (sees lost Spy evs)                         \
   512 \        --> (EX NA. Says Server B                                          \
   513 \                     {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   514 \                       Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   515 \                     : set_of_list evs)";
   516 by (parts_induct_tac 1);
   517 by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   518 (*OR3*)
   519 by (Fast_tac 1);
   520 qed_spec_mp "NB_Crypt_imp_Server_msg";
   521 
   522 
   523 (*Guarantee for B: if it gets a message with matching NB then the Server
   524   has sent the correct message.*)
   525 goal thy 
   526  "!!evs. [| B ~: lost;  evs : otway lost;               \
   527 \           Says S B {|X, Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \
   528 \            : set_of_list evs |]                                  \
   529 \        ==> EX NA. Says Server B                                          \
   530 \                     {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),     \
   531 \                       Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}    \
   532 \                     : set_of_list evs";
   533 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   534                       addEs  partsEs
   535                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   536 qed "B_trust_OR3";