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