src/HOL/Auth/OtwayRees.ML
author paulson
Fri Dec 13 10:20:55 1996 +0100 (1996-12-13)
changeset 2375 14539397fc04
parent 2328 e984c12ce5b4
child 2417 95f275c8476e
permissions -rw-r--r--
Streamlined some proofs
     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 12 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_simp_tac (!simpset addsimps ([not_parts_not_analz,
   455 				       analz_insert_Key_newK] @ pushes)
   456 		            setloop split_tac [expand_if])));
   457 (*OR3*)
   458 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   459                       addss (!simpset addsimps [parts_insert2])) 3);
   460 (*OR4, OR2, Fake*) 
   461 by (REPEAT_FIRST spy_analz_tac);
   462 (*Oops*) (** LEVEL 5 **)
   463 by (fast_tac (!claset delrules [disjE]
   464                       addDs [unique_session_keys] addss (!simpset)) 1);
   465 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   466 
   467 goal thy 
   468  "!!evs. [| Says Server B \
   469 \            {|NA, Crypt (shrK A) {|NA, K|},                             \
   470 \                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;         \
   471 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   472 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   473 \        ==> K ~: analz (sees lost Spy evs)";
   474 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   475 by (fast_tac (!claset addSEs [lemma]) 1);
   476 qed "Spy_not_see_encrypted_key";
   477 
   478 
   479 goal thy 
   480  "!!evs. [| C ~: {A,B,Server};                                           \
   481 \           Says Server B                                                \
   482 \            {|NA, Crypt (shrK A) {|NA, K|},                             \
   483 \                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;         \
   484 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   485 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   486 \        ==> K ~: analz (sees lost C evs)";
   487 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   488 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   489 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   490 by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
   491 qed "Agent_not_see_encrypted_key";
   492 
   493 
   494 (**** Authenticity properties relating to NB ****)
   495 
   496 (*Only OR2 can have caused such a part of a message to appear.  We do not
   497   know anything about X: it does NOT have to have the right form.*)
   498 goal thy 
   499  "!!evs. [| B ~: lost;  evs : otway lost |]                    \
   500 \        ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
   501 \             : parts (sees lost Spy evs) -->                  \
   502 \            (EX X. Says B Server                              \
   503 \             {|NA, Agent A, Agent B, X,                       \
   504 \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   505 \             : set_of_list evs)";
   506 by (parts_induct_tac 1);
   507 by (auto_tac (!claset, !simpset addcongs [conj_cong]));
   508 bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
   509 
   510 
   511 (** The Nonce NB uniquely identifies B's  message. **)
   512 
   513 goal thy 
   514  "!!evs. [| evs : otway lost; B ~: lost |]               \
   515 \ ==> EX NA' A'. ALL NA A.                               \
   516 \      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \
   517 \      --> NA = NA' & A = A'";
   518 by (parts_induct_tac 1);
   519 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   520 (*OR2: creation of new Nonce.  Move assertion into global context*)
   521 by (expand_case_tac "NB = ?y" 1);
   522 by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
   523 val lemma = result();
   524 
   525 goal thy 
   526  "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
   527 \                  : parts(sees lost Spy evs);         \
   528 \          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \
   529 \                  : parts(sees lost Spy evs);         \
   530 \          evs : otway lost;  B ~: lost |]             \
   531 \        ==> NC = NA & C = A";
   532 by (dtac lemma 1);
   533 by (assume_tac 1);
   534 by (REPEAT (etac exE 1));
   535 (*Duplicate the assumption*)
   536 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   537 by (fast_tac (!claset addSDs [spec]) 1);
   538 qed "unique_NB";
   539 
   540 
   541 (*If the encrypted message appears, and B has used Nonce NB,
   542   then it originated with the Server!*)
   543 goal thy 
   544  "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost |]                   \
   545 \    ==> Crypt (shrK B) {|NB, Key K|} : parts (sees lost Spy evs)        \
   546 \        --> (ALL X'. Says B Server                                      \
   547 \                       {|NA, Agent A, Agent B, X',                      \
   548 \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   549 \             : set_of_list evs                                          \
   550 \             --> Says Server B                                          \
   551 \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
   552 \                        Crypt (shrK B) {|NB, Key K|}|}                  \
   553 \                   : set_of_list evs)";
   554 by (parts_induct_tac 1);
   555 (*OR1: it cannot be a new Nonce, contradiction.*)
   556 by (fast_tac (!claset addSIs [parts_insertI]
   557                       addSEs partsEs
   558                       addEs [Says_imp_old_nonces RS less_irrefl]
   559                       addss (!simpset)) 1);
   560 (*OR4*)
   561 by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   562 (*OR3*)
   563 by (step_tac (!claset delrules [disjCI, impCE]) 1);
   564 by (fast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
   565 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   566                       addSEs [MPair_parts]
   567                       addDs  [unique_NB]) 2);
   568 by (fast_tac (!claset addSEs [MPair_parts]
   569                       addSDs [Says_imp_sees_Spy RS parts.Inj]
   570                       addSEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   571                       delrules [conjI, impCE] (*stop split-up*)) 1);
   572 qed_spec_mp "NB_Crypt_imp_Server_msg";
   573 
   574 
   575 (*Guarantee for B: if it gets a message with matching NB then the Server
   576   has sent the correct message.*)
   577 goal thy 
   578  "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
   579 \           Says S B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}       \
   580 \            : set_of_list evs;                                    \
   581 \           Says B Server {|NA, Agent A, Agent B, X',              \
   582 \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   583 \            : set_of_list evs |]                                  \
   584 \        ==> Says Server B                                         \
   585 \                 {|NA,                                            \
   586 \                   Crypt (shrK A) {|NA, Key K|},                  \
   587 \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   588 \                   : set_of_list evs";
   589 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   590                       addEs  partsEs
   591                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   592 qed "B_trusts_OR3";
   593 
   594 
   595 B_trusts_OR3 RS Spy_not_see_encrypted_key;
   596 
   597 
   598 goal thy 
   599  "!!evs. [| B ~: lost;  evs : otway lost |]                           \
   600 \        ==> Says Server B                                            \
   601 \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   602 \                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
   603 \            (EX X. Says B Server {|NA, Agent A, Agent B, X,          \
   604 \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   605 \            : set_of_list evs)";
   606 by (etac otway.induct 1);
   607 by (Auto_tac());
   608 by (dtac (Says_imp_sees_Spy RS parts.Inj) 1);
   609 by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 1);
   610 bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
   611 
   612 
   613 (*After getting and checking OR4, agent A can trust that B has been active.
   614   We could probably prove that X has the expected form, but that is not
   615   strictly necessary for authentication.*)
   616 goal thy 
   617  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   618 \            : set_of_list evs;                                    \
   619 \           Says A B {|NA, Agent A, Agent B,                       \
   620 \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   621 \            : set_of_list evs;                                    \
   622 \           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |] \
   623 \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
   624 \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   625 \            : set_of_list evs";
   626 by (fast_tac (!claset addSDs  [A_trusts_OR4]
   627                       addSEs [OR3_imp_OR2]) 1);
   628 qed "A_auths_B";