src/HOL/Auth/OtwayRees.ML
author paulson
Fri Dec 06 10:36:31 1996 +0100 (1996-12-06)
changeset 2328 e984c12ce5b4
parent 2284 80ebd1a213fd
child 2375 14539397fc04
permissions -rw-r--r--
Minor renamings
     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 Pretty.setdepth 15;
    20 
    21 
    22 (*A "possibility property": there are traces that reach the end*)
    23 goal thy 
    24  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    25 \        ==> EX K. EX NA. EX evs: otway lost.          \
    26 \               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    27 \                 : set_of_list evs";
    28 by (REPEAT (resolve_tac [exI,bexI] 1));
    29 by (rtac (otway.Nil RS otway.OR1 RS otway.OR2 RS otway.OR3 RS otway.OR4) 2);
    30 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    31 by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    32 by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
    33 result();
    34 
    35 
    36 (**** Inductive proofs about otway ****)
    37 
    38 (*Monotonicity*)
    39 goal thy "!!evs. lost' <= lost ==> otway lost' <= otway lost";
    40 by (rtac subsetI 1);
    41 by (etac otway.induct 1);
    42 by (REPEAT_FIRST
    43     (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    44                               :: otway.intrs))));
    45 qed "otway_mono";
    46 
    47 (*Nobody sends themselves messages*)
    48 goal thy "!!evs. evs : otway lost ==> ALL A X. Says A A X ~: set_of_list evs";
    49 by (etac otway.induct 1);
    50 by (Auto_tac());
    51 qed_spec_mp "not_Says_to_self";
    52 Addsimps [not_Says_to_self];
    53 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    54 
    55 
    56 (** For reasoning about the encrypted portion of messages **)
    57 
    58 goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs \
    59 \                ==> X : analz (sees lost Spy evs)";
    60 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    61 qed "OR2_analz_sees_Spy";
    62 
    63 goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs \
    64 \                ==> X : analz (sees lost Spy evs)";
    65 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    66 qed "OR4_analz_sees_Spy";
    67 
    68 goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \
    69 \                 ==> K : parts (sees lost Spy evs)";
    70 by (fast_tac (!claset addSEs partsEs
    71                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    72 qed "Oops_parts_sees_Spy";
    73 
    74 (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    75   argument as for the Fake case.  This is possible for most, but not all,
    76   proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    77   messages originate from the Spy. *)
    78 
    79 bind_thm ("OR2_parts_sees_Spy",
    80           OR2_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    81 bind_thm ("OR4_parts_sees_Spy",
    82           OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    83 
    84 (*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
    85   harder to complete, since simplification does less for us.*)
    86 val parts_Fake_tac = 
    87     let val tac = forw_inst_tac [("lost","lost")] 
    88     in  tac OR2_parts_sees_Spy 4 THEN 
    89         tac OR4_parts_sees_Spy 6 THEN
    90         tac Oops_parts_sees_Spy 7
    91     end;
    92 
    93 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    94 fun parts_induct_tac i = SELECT_GOAL
    95     (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
    96              (*Fake message*)
    97              TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    98                                            impOfSubs Fake_parts_insert]
    99                                     addss (!simpset)) 2)) THEN
   100      (*Base case*)
   101      fast_tac (!claset addss (!simpset)) 1 THEN
   102      ALLGOALS Asm_simp_tac) i;
   103 
   104 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
   105     sends messages containing X! **)
   106 
   107 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
   108 goal thy 
   109  "!!evs. evs : otway lost \
   110 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
   111 by (parts_induct_tac 1);
   112 by (Auto_tac());
   113 qed "Spy_see_shrK";
   114 Addsimps [Spy_see_shrK];
   115 
   116 goal thy 
   117  "!!evs. evs : otway lost \
   118 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
   119 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   120 qed "Spy_analz_shrK";
   121 Addsimps [Spy_analz_shrK];
   122 
   123 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   124 \                  evs : otway lost |] ==> A:lost";
   125 by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
   126 qed "Spy_see_shrK_D";
   127 
   128 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   129 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   130 
   131 
   132 (*** Future keys can't be seen or used! ***)
   133 
   134 (*Nobody can have SEEN keys that will be generated in the future. *)
   135 goal thy "!!evs. evs : otway lost ==> \
   136 \                length evs <= length evs' --> \
   137 \                Key (newK evs') ~: parts (sees lost Spy evs)";
   138 by (parts_induct_tac 1);
   139 by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
   140                                     addDs [impOfSubs analz_subset_parts,
   141                                            impOfSubs parts_insert_subset_Un,
   142                                            Suc_leD]
   143                                     addss (!simpset))));
   144 qed_spec_mp "new_keys_not_seen";
   145 Addsimps [new_keys_not_seen];
   146 
   147 (*Variant: old messages must contain old keys!*)
   148 goal thy 
   149  "!!evs. [| Says A B X : set_of_list evs;  \
   150 \           Key (newK evt) : parts {X};    \
   151 \           evs : otway lost                 \
   152 \        |] ==> length evt < length evs";
   153 by (rtac ccontr 1);
   154 by (dtac leI 1);
   155 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   156                       addIs  [impOfSubs parts_mono]) 1);
   157 qed "Says_imp_old_keys";
   158 
   159 
   160 (*** Future nonces can't be seen or used! ***)
   161 
   162 goal thy "!!evs. evs : otway lost ==> \
   163 \                length evs <= length evt --> \
   164 \                Nonce (newN evt) ~: parts (sees lost Spy evs)";
   165 by (parts_induct_tac 1);
   166 by (REPEAT_FIRST (fast_tac (!claset 
   167                               addSEs partsEs
   168                               addSDs  [Says_imp_sees_Spy RS parts.Inj]
   169                               addEs [leD RS notE]
   170                               addDs  [impOfSubs analz_subset_parts,
   171                                       impOfSubs parts_insert_subset_Un,
   172                                       Suc_leD]
   173                               addss (!simpset))));
   174 qed_spec_mp "new_nonces_not_seen";
   175 Addsimps [new_nonces_not_seen];
   176 
   177 (*Variant: old messages must contain old nonces!*)
   178 goal thy "!!evs. [| Says A B X : set_of_list evs;    \
   179 \                   Nonce (newN evt) : parts {X};    \
   180 \                   evs : otway lost                 \
   181 \                |] ==> length evt < length evs";
   182 by (rtac ccontr 1);
   183 by (dtac leI 1);
   184 by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
   185                       addIs  [impOfSubs parts_mono]) 1);
   186 qed "Says_imp_old_nonces";
   187 
   188 
   189 (*Nobody can have USED keys that will be generated in the future.
   190   ...very like new_keys_not_seen*)
   191 goal thy "!!evs. evs : otway lost ==>          \
   192 \                length evs <= length evs' --> \
   193 \                newK evs' ~: keysFor (parts (sees lost Spy evs))";
   194 by (parts_induct_tac 1);
   195 (*OR1 and OR3*)
   196 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   197 (*Fake, OR2, OR4: these messages send unknown (X) components*)
   198 by (REPEAT
   199     (best_tac
   200       (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   201                       impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   202                       Suc_leD]
   203                addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
   204                addss (!simpset)) 1));
   205 qed_spec_mp "new_keys_not_used";
   206 
   207 bind_thm ("new_keys_not_analzd",
   208           [analz_subset_parts RS keysFor_mono,
   209            new_keys_not_used] MRS contra_subsetD);
   210 
   211 Addsimps [new_keys_not_used, new_keys_not_analzd];
   212 
   213 
   214 
   215 (*** Proofs involving analz ***)
   216 
   217 (*Describes the form of K and NA when the Server sends this message.  Also
   218   for Oops case.*)
   219 goal thy 
   220  "!!evs. [| Says Server B \
   221 \            {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs;  \
   222 \           evs : otway lost |]                                   \
   223 \        ==> (EX evt: otway lost. K = Key(newK evt)) &            \
   224 \            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   225 by (etac rev_mp 1);
   226 by (etac otway.induct 1);
   227 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   228 qed "Says_Server_message_form";
   229 
   230 
   231 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   232 val analz_Fake_tac = 
   233     dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN 
   234     dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   235     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   236     assume_tac 7 THEN Full_simp_tac 7 THEN
   237     REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
   238 
   239 
   240 (****
   241  The following is to prove theorems of the form
   242 
   243           Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   244           Key K : analz (sees lost Spy evs)
   245 
   246  A more general formula must be proved inductively.
   247 ****)
   248 
   249 
   250 (** Session keys are not used to encrypt other session keys **)
   251 
   252 (*The equality makes the induction hypothesis easier to apply*)
   253 goal thy  
   254  "!!evs. evs : otway lost ==> \
   255 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   256 \           (K : newK``E | Key K : analz (sees lost Spy evs))";
   257 by (etac otway.induct 1);
   258 by analz_Fake_tac;
   259 by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   260 by (ALLGOALS (*Takes 14 secs*)
   261     (asm_simp_tac 
   262      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   263                          @ pushes)
   264                setloop split_tac [expand_if])));
   265 (*OR4, OR2, Fake*) 
   266 by (EVERY (map spy_analz_tac [5,3,2]));
   267 (*Oops, OR3, Base*)
   268 by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   269 qed_spec_mp "analz_image_newK";
   270 
   271 
   272 goal thy
   273  "!!evs. evs : otway lost ==>                               \
   274 \        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   275 \        (K = newK evt | Key K : analz (sees lost Spy evs))";
   276 by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   277                                    insert_Key_singleton]) 1);
   278 by (Fast_tac 1);
   279 qed "analz_insert_Key_newK";
   280 
   281 
   282 (*** The Key K uniquely identifies the Server's  message. **)
   283 
   284 goal thy 
   285  "!!evs. evs : otway lost ==>                                                 \
   286 \   EX B' NA' NB' X'. ALL B NA NB X.                                          \
   287 \     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set_of_list evs --> \
   288 \     B=B' & NA=NA' & NB=NB' & X=X'";
   289 by (etac otway.induct 1);
   290 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   291 by (Step_tac 1);
   292 (*Remaining cases: OR3 and OR4*)
   293 by (ex_strip_tac 2);
   294 by (Fast_tac 2);
   295 by (expand_case_tac "K = ?y" 1);
   296 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   297 (*...we assume X is a very new message, and handle this case by contradiction*)
   298 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   299                       delrules [conjI]    (*prevent split-up into 4 subgoals*)
   300                       addss (!simpset addsimps [parts_insertI])) 1);
   301 val lemma = result();
   302 
   303 goal thy 
   304  "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}      \
   305 \            : set_of_list evs;                                    \ 
   306 \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|}    \
   307 \            : set_of_list evs;                                    \
   308 \           evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
   309 by (dtac lemma 1);
   310 by (REPEAT (etac exE 1));
   311 (*Duplicate the assumption*)
   312 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   313 by (fast_tac (!claset addSDs [spec]) 1);
   314 qed "unique_session_keys";
   315 
   316 
   317 
   318 (**** Authenticity properties relating to NA ****)
   319 
   320 (*Only OR1 can have caused such a part of a message to appear.*)
   321 goal thy 
   322  "!!evs. [| A ~: lost;  evs : otway lost |]                        \
   323 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}               \
   324 \             : parts (sees lost Spy evs) -->                      \
   325 \            Says A B {|NA, Agent A, Agent B,                      \
   326 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
   327 \             : set_of_list evs";
   328 by (parts_induct_tac 1);
   329 qed_spec_mp "Crypt_imp_OR1";
   330 
   331 
   332 (** The Nonce NA uniquely identifies A's message. **)
   333 
   334 goal thy 
   335  "!!evs. [| evs : otway lost; A ~: lost |]               \
   336 \ ==> EX B'. ALL B.    \
   337 \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
   338 \        --> B = B'";
   339 by (parts_induct_tac 1);
   340 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   341 (*OR1: creation of new Nonce.  Move assertion into global context*)
   342 by (expand_case_tac "NA = ?y" 1);
   343 by (best_tac (!claset addSEs partsEs
   344                       addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
   345 val lemma = result();
   346 
   347 goal thy 
   348  "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts(sees lost Spy evs); \
   349 \          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \
   350 \          evs : otway lost;  A ~: lost |]                                    \
   351 \        ==> B = C";
   352 by (dtac lemma 1);
   353 by (assume_tac 1);
   354 by (etac exE 1);
   355 (*Duplicate the assumption*)
   356 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   357 by (fast_tac (!claset addSDs [spec]) 1);
   358 qed "unique_NA";
   359 
   360 
   361 val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
   362 
   363 (*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   364   OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   365   over-simplified version of this protocol: see OtwayRees_Bad.*)
   366 goal thy 
   367  "!!evs. [| A ~: lost;  evs : otway lost |]                      \
   368 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}             \
   369 \             : parts (sees lost Spy evs) -->                    \
   370 \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
   371 \             ~: parts (sees lost Spy evs)";
   372 by (parts_induct_tac 1);
   373 by (REPEAT (fast_tac (!claset addSEs (partsEs@[nonce_not_seen_now])
   374                               addSDs  [impOfSubs parts_insert_subset_Un]
   375                               addss (!simpset)) 1));
   376 qed_spec_mp"no_nonce_OR1_OR2";
   377 
   378 
   379 (*Crucial property: If the encrypted message appears, and A has used NA
   380   to start a run, then it originated with the Server!*)
   381 goal thy 
   382  "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                 \
   383 \    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs)      \
   384 \        --> Says A B {|NA, Agent A, Agent B,                          \
   385 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
   386 \             : set_of_list evs -->                                    \
   387 \            (EX NB. Says Server B                                     \
   388 \                 {|NA,                                                \
   389 \                   Crypt (shrK A) {|NA, Key K|},                      \
   390 \                   Crypt (shrK B) {|NB, Key K|}|}                     \
   391 \                   : set_of_list evs)";
   392 by (parts_induct_tac 1);
   393 (*OR1: it cannot be a new Nonce, contradiction.*)
   394 by (fast_tac (!claset addSIs [parts_insertI]
   395                       addSEs partsEs
   396                       addEs [Says_imp_old_nonces RS less_irrefl]
   397                       addss (!simpset)) 1);
   398 (*OR3 and OR4*) 
   399 (*OR4*)
   400 by (REPEAT (Safe_step_tac 2));
   401 by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
   402 by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   403                       addEs  partsEs
   404                       addDs [Says_imp_sees_Spy RS parts.Inj]) 2);
   405 (*OR3*)  (** LEVEL 5 **)
   406 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   407 by (step_tac (!claset delrules [disjCI, impCE]) 1);
   408 by (fast_tac (!claset addSEs [MPair_parts]
   409                       addSDs [Says_imp_sees_Spy RS parts.Inj]
   410                       addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   411                       delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   412 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   413                       addSEs [MPair_parts]
   414                       addEs  [unique_NA]) 1);
   415 qed_spec_mp "NA_Crypt_imp_Server_msg";
   416 
   417 
   418 (*Corollary: if A receives B's OR4 message and the nonce NA agrees
   419   then the key really did come from the Server!  CANNOT prove this of the
   420   bad form of this protocol, even though we can prove
   421   Spy_not_see_encrypted_key*)
   422 goal thy 
   423  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   424 \            : set_of_list evs;                                    \
   425 \           Says A B {|NA, Agent A, Agent B,                       \
   426 \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   427 \            : set_of_list evs;                                    \
   428 \           A ~: lost;  A ~= Spy;  evs : otway lost |]             \
   429 \        ==> EX NB. Says Server B                                  \
   430 \                     {|NA,                                        \
   431 \                       Crypt (shrK A) {|NA, Key K|},              \
   432 \                       Crypt (shrK B) {|NB, Key K|}|}             \
   433 \                       : set_of_list evs";
   434 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   435                       addEs  partsEs
   436                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   437 qed "A_trusts_OR4";
   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 |]                    \
   446 \        ==> Says Server B                                                 \
   447 \              {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   448 \                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs -->      \
   449 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   450 \            Key K ~: analz (sees lost Spy evs)";
   451 by (etac otway.induct 1);
   452 by analz_Fake_tac;
   453 by (ALLGOALS
   454     (asm_full_simp_tac 
   455      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   456                           analz_insert_Key_newK] @ pushes)
   457                setloop split_tac [expand_if])));
   458 (*OR3*)
   459 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   460                       addss (!simpset addsimps [parts_insert2])) 3);
   461 (*OR4, OR2, Fake*) 
   462 by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   463 (*Oops*) (** LEVEL 5 **)
   464 by (fast_tac (!claset delrules [disjE]
   465                       addDs [unique_session_keys] addss (!simpset)) 1);
   466 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   467 
   468 goal thy 
   469  "!!evs. [| Says Server B \
   470 \            {|NA, Crypt (shrK A) {|NA, K|},                             \
   471 \                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;         \
   472 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   473 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   474 \        ==> K ~: analz (sees lost Spy evs)";
   475 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   476 by (fast_tac (!claset addSEs [lemma]) 1);
   477 qed "Spy_not_see_encrypted_key";
   478 
   479 
   480 goal thy 
   481  "!!evs. [| C ~: {A,B,Server};                                           \
   482 \           Says Server B                                                \
   483 \            {|NA, Crypt (shrK A) {|NA, K|},                             \
   484 \                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;         \
   485 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   486 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   487 \        ==> K ~: analz (sees lost C evs)";
   488 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   489 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   490 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   491 by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
   492 qed "Agent_not_see_encrypted_key";
   493 
   494 
   495 (**** Authenticity properties relating to NB ****)
   496 
   497 (*Only OR2 can have caused such a part of a message to appear.  We do not
   498   know anything about X: it does NOT have to have the right form.*)
   499 goal thy 
   500  "!!evs. [| B ~: lost;  evs : otway lost |]                    \
   501 \        ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
   502 \             : parts (sees lost Spy evs) -->                  \
   503 \            (EX X. Says B Server                              \
   504 \             {|NA, Agent A, Agent B, X,                       \
   505 \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   506 \             : set_of_list evs)";
   507 by (parts_induct_tac 1);
   508 by (auto_tac (!claset, !simpset addcongs [conj_cong]));
   509 bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
   510 
   511 
   512 (** The Nonce NB uniquely identifies B's  message. **)
   513 
   514 goal thy 
   515  "!!evs. [| evs : otway lost; B ~: lost |]               \
   516 \ ==> EX NA' A'. ALL NA A.                               \
   517 \      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \
   518 \      --> NA = NA' & A = A'";
   519 by (parts_induct_tac 1);
   520 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   521 (*OR2: creation of new Nonce.  Move assertion into global context*)
   522 by (expand_case_tac "NB = ?y" 1);
   523 by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
   524 val lemma = result();
   525 
   526 goal thy 
   527  "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
   528 \                  : parts(sees lost Spy evs);         \
   529 \          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \
   530 \                  : parts(sees lost Spy evs);         \
   531 \          evs : otway lost;  B ~: lost |]             \
   532 \        ==> NC = NA & C = A";
   533 by (dtac lemma 1);
   534 by (assume_tac 1);
   535 by (REPEAT (etac exE 1));
   536 (*Duplicate the assumption*)
   537 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   538 by (fast_tac (!claset addSDs [spec]) 1);
   539 qed "unique_NB";
   540 
   541 
   542 (*If the encrypted message appears, and B has used Nonce NB,
   543   then it originated with the Server!*)
   544 goal thy 
   545  "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost |]                   \
   546 \    ==> Crypt (shrK B) {|NB, Key K|} : parts (sees lost Spy evs)        \
   547 \        --> (ALL X'. Says B Server                                      \
   548 \                       {|NA, Agent A, Agent B, X',                      \
   549 \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   550 \             : set_of_list evs                                          \
   551 \             --> Says Server B                                          \
   552 \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
   553 \                        Crypt (shrK B) {|NB, Key K|}|}                  \
   554 \                   : set_of_list evs)";
   555 by (parts_induct_tac 1);
   556 (*OR1: it cannot be a new Nonce, contradiction.*)
   557 by (fast_tac (!claset addSIs [parts_insertI]
   558                       addSEs partsEs
   559                       addEs [Says_imp_old_nonces RS less_irrefl]
   560                       addss (!simpset)) 1);
   561 (*OR4*)
   562 by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   563 (*OR3*)
   564 by (step_tac (!claset delrules [disjCI, impCE]) 1);
   565 by (fast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
   566 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   567                       addSEs [MPair_parts]
   568                       addDs  [unique_NB]) 2);
   569 by (fast_tac (!claset addSEs [MPair_parts]
   570                       addSDs [Says_imp_sees_Spy RS parts.Inj]
   571                       addSEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   572                       delrules [conjI, impCE] (*stop split-up*)) 1);
   573 qed_spec_mp "NB_Crypt_imp_Server_msg";
   574 
   575 
   576 (*Guarantee for B: if it gets a message with matching NB then the Server
   577   has sent the correct message.*)
   578 goal thy 
   579  "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
   580 \           Says S B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}       \
   581 \            : set_of_list evs;                                    \
   582 \           Says B Server {|NA, Agent A, Agent B, X',              \
   583 \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   584 \            : set_of_list evs |]                                  \
   585 \        ==> Says Server B                                         \
   586 \                 {|NA,                                            \
   587 \                   Crypt (shrK A) {|NA, Key K|},                  \
   588 \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   589 \                   : set_of_list evs";
   590 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   591                       addEs  partsEs
   592                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   593 qed "B_trusts_OR3";
   594 
   595 
   596 B_trusts_OR3 RS Spy_not_see_encrypted_key;
   597 
   598 
   599 goal thy 
   600  "!!evs. [| B ~: lost;  evs : otway lost |]                           \
   601 \        ==> Says Server B                                            \
   602 \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   603 \                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
   604 \            (EX X. Says B Server {|NA, Agent A, Agent B, X,          \
   605 \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   606 \            : set_of_list evs)";
   607 by (etac otway.induct 1);
   608 by (Auto_tac());
   609 by (dtac (Says_imp_sees_Spy RS parts.Inj) 1);
   610 by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 1);
   611 bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
   612 
   613 
   614 (*After getting and checking OR4, agent A can trust that B has been active.
   615   We could probably prove that X has the expected form, but that is not
   616   strictly necessary for authentication.*)
   617 goal thy 
   618  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   619 \            : set_of_list evs;                                    \
   620 \           Says A B {|NA, Agent A, Agent B,                       \
   621 \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   622 \            : set_of_list evs;                                    \
   623 \           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |] \
   624 \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
   625 \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   626 \            : set_of_list evs";
   627 by (fast_tac (!claset addSDs  [A_trusts_OR4]
   628                       addSEs [OR3_imp_OR2]) 1);
   629 qed "A_auths_B";