src/HOL/Auth/OtwayRees.ML
author paulson
Mon Dec 16 11:08:11 1996 +0100 (1996-12-16)
changeset 2417 95f275c8476e
parent 2375 14539397fc04
child 2451 ce85a2aafc7a
permissions -rw-r--r--
New tactic: prove_unique_tac
     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 (prove_unique_tac lemma 1);
   310 qed "unique_session_keys";
   311 
   312 
   313 
   314 (**** Authenticity properties relating to NA ****)
   315 
   316 (*Only OR1 can have caused such a part of a message to appear.*)
   317 goal thy 
   318  "!!evs. [| A ~: lost;  evs : otway lost |]                        \
   319 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}               \
   320 \             : parts (sees lost Spy evs) -->                      \
   321 \            Says A B {|NA, Agent A, Agent B,                      \
   322 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  \
   323 \             : set_of_list evs";
   324 by (parts_induct_tac 1);
   325 qed_spec_mp "Crypt_imp_OR1";
   326 
   327 
   328 (** The Nonce NA uniquely identifies A's message. **)
   329 
   330 goal thy 
   331  "!!evs. [| evs : otway lost; A ~: lost |]               \
   332 \ ==> EX B'. ALL B.    \
   333 \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \
   334 \        --> B = B'";
   335 by (parts_induct_tac 1);
   336 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   337 (*OR1: creation of new Nonce.  Move assertion into global context*)
   338 by (expand_case_tac "NA = ?y" 1);
   339 by (best_tac (!claset addSEs partsEs
   340                       addEs  [new_nonces_not_seen RSN(2,rev_notE)]) 1);
   341 val lemma = result();
   342 
   343 goal thy 
   344  "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts(sees lost Spy evs); \
   345 \          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts(sees lost Spy evs); \
   346 \          evs : otway lost;  A ~: lost |]                                    \
   347 \        ==> B = C";
   348 by (prove_unique_tac lemma 1);
   349 qed "unique_NA";
   350 
   351 
   352 val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
   353 
   354 (*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   355   OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   356   over-simplified version of this protocol: see OtwayRees_Bad.*)
   357 goal thy 
   358  "!!evs. [| A ~: lost;  evs : otway lost |]                      \
   359 \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|}             \
   360 \             : parts (sees lost Spy evs) -->                    \
   361 \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}       \
   362 \             ~: parts (sees lost Spy evs)";
   363 by (parts_induct_tac 1);
   364 by (REPEAT (fast_tac (!claset addSEs (partsEs@[nonce_not_seen_now])
   365                               addSDs  [impOfSubs parts_insert_subset_Un]
   366                               addss (!simpset)) 1));
   367 qed_spec_mp"no_nonce_OR1_OR2";
   368 
   369 
   370 (*Crucial property: If the encrypted message appears, and A has used NA
   371   to start a run, then it originated with the Server!*)
   372 goal thy 
   373  "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway lost |]                 \
   374 \    ==> Crypt (shrK A) {|NA, Key K|} : parts (sees lost Spy evs)      \
   375 \        --> Says A B {|NA, Agent A, Agent B,                          \
   376 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
   377 \             : set_of_list evs -->                                    \
   378 \            (EX NB. Says Server B                                     \
   379 \                 {|NA,                                                \
   380 \                   Crypt (shrK A) {|NA, Key K|},                      \
   381 \                   Crypt (shrK B) {|NB, Key K|}|}                     \
   382 \                   : set_of_list evs)";
   383 by (parts_induct_tac 1);
   384 (*OR1: it cannot be a new Nonce, contradiction.*)
   385 by (fast_tac (!claset addSIs [parts_insertI]
   386                       addSEs partsEs
   387                       addEs [Says_imp_old_nonces RS less_irrefl]
   388                       addss (!simpset)) 1);
   389 (*OR3 and OR4*) 
   390 (*OR4*)
   391 by (REPEAT (Safe_step_tac 2));
   392 by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
   393 by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   394                       addEs  partsEs
   395                       addDs [Says_imp_sees_Spy RS parts.Inj]) 2);
   396 (*OR3*)  (** LEVEL 5 **)
   397 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   398 by (step_tac (!claset delrules [disjCI, impCE]) 1);
   399 by (fast_tac (!claset addSEs [MPair_parts]
   400                       addSDs [Says_imp_sees_Spy RS parts.Inj]
   401                       addEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   402                       delrules [conjI] (*stop split-up into 4 subgoals*)) 2);
   403 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   404                       addSEs [MPair_parts]
   405                       addEs  [unique_NA]) 1);
   406 qed_spec_mp "NA_Crypt_imp_Server_msg";
   407 
   408 
   409 (*Corollary: if A receives B's OR4 message and the nonce NA agrees
   410   then the key really did come from the Server!  CANNOT prove this of the
   411   bad form of this protocol, even though we can prove
   412   Spy_not_see_encrypted_key*)
   413 goal thy 
   414  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   415 \            : set_of_list evs;                                    \
   416 \           Says A B {|NA, Agent A, Agent B,                       \
   417 \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   418 \            : set_of_list evs;                                    \
   419 \           A ~: lost;  A ~= Spy;  evs : otway lost |]             \
   420 \        ==> EX NB. Says Server B                                  \
   421 \                     {|NA,                                        \
   422 \                       Crypt (shrK A) {|NA, Key K|},              \
   423 \                       Crypt (shrK B) {|NB, Key K|}|}             \
   424 \                       : set_of_list evs";
   425 by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg]
   426                       addEs  partsEs
   427                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   428 qed "A_trusts_OR4";
   429 
   430 
   431 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   432     Does not in itself guarantee security: an attack could violate 
   433     the premises, e.g. by having A=Spy **)
   434 
   435 goal thy 
   436  "!!evs. [| A ~: lost;  B ~: lost;  evs : otway lost |]                    \
   437 \        ==> Says Server B                                                 \
   438 \              {|NA, Crypt (shrK A) {|NA, Key K|},                         \
   439 \                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs -->      \
   440 \            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   441 \            Key K ~: analz (sees lost Spy evs)";
   442 by (etac otway.induct 1);
   443 by analz_Fake_tac;
   444 by (ALLGOALS
   445     (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
   446 				       analz_insert_Key_newK] @ pushes)
   447 		            setloop split_tac [expand_if])));
   448 (*OR3*)
   449 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   450                       addss (!simpset addsimps [parts_insert2])) 3);
   451 (*OR4, OR2, Fake*) 
   452 by (REPEAT_FIRST spy_analz_tac);
   453 (*Oops*) (** LEVEL 5 **)
   454 by (fast_tac (!claset delrules [disjE]
   455                       addDs [unique_session_keys] addss (!simpset)) 1);
   456 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   457 
   458 goal thy 
   459  "!!evs. [| Says Server B \
   460 \            {|NA, Crypt (shrK A) {|NA, K|},                             \
   461 \                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;         \
   462 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   463 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   464 \        ==> K ~: analz (sees lost Spy evs)";
   465 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   466 by (fast_tac (!claset addSEs [lemma]) 1);
   467 qed "Spy_not_see_encrypted_key";
   468 
   469 
   470 goal thy 
   471  "!!evs. [| C ~: {A,B,Server};                                           \
   472 \           Says Server B                                                \
   473 \            {|NA, Crypt (shrK A) {|NA, K|},                             \
   474 \                  Crypt (shrK B) {|NB, K|}|} : set_of_list evs;         \
   475 \           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   476 \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   477 \        ==> K ~: analz (sees lost C evs)";
   478 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   479 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   480 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   481 by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
   482 qed "Agent_not_see_encrypted_key";
   483 
   484 
   485 (**** Authenticity properties relating to NB ****)
   486 
   487 (*Only OR2 can have caused such a part of a message to appear.  We do not
   488   know anything about X: it does NOT have to have the right form.*)
   489 goal thy 
   490  "!!evs. [| B ~: lost;  evs : otway lost |]                    \
   491 \        ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
   492 \             : parts (sees lost Spy evs) -->                  \
   493 \            (EX X. Says B Server                              \
   494 \             {|NA, Agent A, Agent B, X,                       \
   495 \               Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   496 \             : set_of_list evs)";
   497 by (parts_induct_tac 1);
   498 by (auto_tac (!claset, !simpset addcongs [conj_cong]));
   499 bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
   500 
   501 
   502 (** The Nonce NB uniquely identifies B's  message. **)
   503 
   504 goal thy 
   505  "!!evs. [| evs : otway lost; B ~: lost |]               \
   506 \ ==> EX NA' A'. ALL NA A.                               \
   507 \      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \
   508 \      --> NA = NA' & A = A'";
   509 by (parts_induct_tac 1);
   510 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   511 (*OR2: creation of new Nonce.  Move assertion into global context*)
   512 by (expand_case_tac "NB = ?y" 1);
   513 by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
   514 val lemma = result();
   515 
   516 goal thy 
   517  "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \
   518 \                  : parts(sees lost Spy evs);         \
   519 \          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} \
   520 \                  : parts(sees lost Spy evs);         \
   521 \          evs : otway lost;  B ~: lost |]             \
   522 \        ==> NC = NA & C = A";
   523 by (prove_unique_tac lemma 1);
   524 qed "unique_NB";
   525 
   526 
   527 (*If the encrypted message appears, and B has used Nonce NB,
   528   then it originated with the Server!*)
   529 goal thy 
   530  "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost |]                   \
   531 \    ==> Crypt (shrK B) {|NB, Key K|} : parts (sees lost Spy evs)        \
   532 \        --> (ALL X'. Says B Server                                      \
   533 \                       {|NA, Agent A, Agent B, X',                      \
   534 \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
   535 \             : set_of_list evs                                          \
   536 \             --> Says Server B                                          \
   537 \                  {|NA, Crypt (shrK A) {|NA, Key K|},                   \
   538 \                        Crypt (shrK B) {|NB, Key K|}|}                  \
   539 \                   : set_of_list evs)";
   540 by (parts_induct_tac 1);
   541 (*OR1: it cannot be a new Nonce, contradiction.*)
   542 by (fast_tac (!claset addSIs [parts_insertI]
   543                       addSEs partsEs
   544                       addEs [Says_imp_old_nonces RS less_irrefl]
   545                       addss (!simpset)) 1);
   546 (*OR4*)
   547 by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
   548 (*OR3*)
   549 by (step_tac (!claset delrules [disjCI, impCE]) 1);
   550 by (fast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
   551 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   552                       addSEs [MPair_parts]
   553                       addDs  [unique_NB]) 2);
   554 by (fast_tac (!claset addSEs [MPair_parts]
   555                       addSDs [Says_imp_sees_Spy RS parts.Inj]
   556                       addSEs  [no_nonce_OR1_OR2 RSN (2, rev_notE)]
   557                       delrules [conjI, impCE] (*stop split-up*)) 1);
   558 qed_spec_mp "NB_Crypt_imp_Server_msg";
   559 
   560 
   561 (*Guarantee for B: if it gets a message with matching NB then the Server
   562   has sent the correct message.*)
   563 goal thy 
   564  "!!evs. [| B ~: lost;  B ~= Spy;  evs : otway lost;               \
   565 \           Says S B {|NA, X, Crypt (shrK B) {|NB, Key K|}|}       \
   566 \            : set_of_list evs;                                    \
   567 \           Says B Server {|NA, Agent A, Agent B, X',              \
   568 \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   569 \            : set_of_list evs |]                                  \
   570 \        ==> Says Server B                                         \
   571 \                 {|NA,                                            \
   572 \                   Crypt (shrK A) {|NA, Key K|},                  \
   573 \                   Crypt (shrK B) {|NB, Key K|}|}                 \
   574 \                   : set_of_list evs";
   575 by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg]
   576                       addEs  partsEs
   577                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   578 qed "B_trusts_OR3";
   579 
   580 
   581 B_trusts_OR3 RS Spy_not_see_encrypted_key;
   582 
   583 
   584 goal thy 
   585  "!!evs. [| B ~: lost;  evs : otway lost |]                           \
   586 \        ==> Says Server B                                            \
   587 \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   588 \                Crypt (shrK B) {|NB, Key K|}|} : set_of_list evs --> \
   589 \            (EX X. Says B Server {|NA, Agent A, Agent B, X,          \
   590 \                            Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   591 \            : set_of_list evs)";
   592 by (etac otway.induct 1);
   593 by (Auto_tac());
   594 by (dtac (Says_imp_sees_Spy RS parts.Inj) 1);
   595 by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 1);
   596 bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
   597 
   598 
   599 (*After getting and checking OR4, agent A can trust that B has been active.
   600   We could probably prove that X has the expected form, but that is not
   601   strictly necessary for authentication.*)
   602 goal thy 
   603  "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|}         \
   604 \            : set_of_list evs;                                    \
   605 \           Says A B {|NA, Agent A, Agent B,                       \
   606 \                      Crypt (shrK A) {|NA, Agent A, Agent B|}|}   \
   607 \            : set_of_list evs;                                    \
   608 \           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |] \
   609 \        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
   610 \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
   611 \            : set_of_list evs";
   612 by (fast_tac (!claset addSDs  [A_trusts_OR4]
   613                       addSEs [OR3_imp_OR2]) 1);
   614 qed "A_auths_B";