src/HOL/Auth/Yahalom.ML
author paulson
Fri Dec 13 10:57:50 1996 +0100 (1996-12-13)
changeset 2377 ad9d2dedaeaa
parent 2322 fbe6dd4abddc
child 2451 ce85a2aafc7a
permissions -rw-r--r--
Streamlined many proofs
     1 (*  Title:      HOL/Auth/Yahalom
     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 Yahalom protocol.
     7 
     8 From page 257 of
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
    10   Proc. Royal Soc. 426 (1989)
    11 *)
    12 
    13 open Yahalom;
    14 
    15 proof_timing:=true;
    16 HOL_quantifiers := false;
    17 Pretty.setdepth 20;
    18 
    19 
    20 (*A "possibility property": there are traces that reach the end*)
    21 goal thy 
    22  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    23 \        ==> EX X NB K. EX evs: yahalom lost.          \
    24 \               Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
    25 by (REPEAT (resolve_tac [exI,bexI] 1));
    26 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2);
    27 by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    28 by (ALLGOALS Fast_tac);
    29 result();
    30 
    31 
    32 (**** Inductive proofs about yahalom ****)
    33 
    34 (*Monotonicity*)
    35 goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
    36 by (rtac subsetI 1);
    37 by (etac yahalom.induct 1);
    38 by (REPEAT_FIRST
    39     (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    40                               :: yahalom.intrs))));
    41 qed "yahalom_mono";
    42 
    43 
    44 (*Nobody sends themselves messages*)
    45 goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
    46 by (etac yahalom.induct 1);
    47 by (Auto_tac());
    48 qed_spec_mp "not_Says_to_self";
    49 Addsimps [not_Says_to_self];
    50 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    51 
    52 
    53 (** For reasoning about the encrypted portion of messages **)
    54 
    55 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    56 goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set_of_list evs ==> \
    57 \                X : analz (sees lost Spy evs)";
    58 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    59 qed "YM4_analz_sees_Spy";
    60 
    61 bind_thm ("YM4_parts_sees_Spy",
    62           YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    63 
    64 (*Relates to both YM4 and Oops*)
    65 goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \
    66 \                  : set_of_list evs ==> \
    67 \                K : parts (sees lost Spy evs)";
    68 by (fast_tac (!claset addSEs partsEs
    69                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    70 qed "YM4_Key_parts_sees_Spy";
    71 
    72 (*We instantiate the variable to "lost".  Leaving it as a Var makes proofs
    73   harder: the simplifier does less.*)
    74 val parts_Fake_tac = 
    75     forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN
    76     forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7;
    77 
    78 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    79 fun parts_induct_tac i = SELECT_GOAL
    80     (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN
    81              (*Fake message*)
    82              TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    83                                            impOfSubs Fake_parts_insert]
    84                                     addss (!simpset)) 2)) THEN
    85      (*Base case*)
    86      fast_tac (!claset addss (!simpset)) 1 THEN
    87      ALLGOALS Asm_simp_tac) i;
    88 
    89 
    90 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    91     sends messages containing X! **)
    92 
    93 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    94 goal thy 
    95  "!!evs. evs : yahalom lost \
    96 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    97 by (parts_induct_tac 1);
    98 by (Auto_tac());
    99 qed "Spy_see_shrK";
   100 Addsimps [Spy_see_shrK];
   101 
   102 goal thy 
   103  "!!evs. evs : yahalom lost \
   104 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
   105 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   106 qed "Spy_analz_shrK";
   107 Addsimps [Spy_analz_shrK];
   108 
   109 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   110 \                  evs : yahalom lost |] ==> A:lost";
   111 by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
   112 qed "Spy_see_shrK_D";
   113 
   114 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   115 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   116 
   117 
   118 (*** Future keys can't be seen or used! ***)
   119 
   120 (*Nobody can have SEEN keys that will be generated in the future. *)
   121 goal thy "!!evs. evs : yahalom lost ==> \
   122 \                length evs <= length evs' --> \
   123 \                Key (newK evs') ~: parts (sees lost Spy evs)";
   124 by (parts_induct_tac 1);
   125 by (REPEAT_FIRST (best_tac (!claset addEs [leD RS notE]
   126 				    addDs [impOfSubs analz_subset_parts,
   127                                            impOfSubs parts_insert_subset_Un,
   128                                            Suc_leD]
   129                                     addss (!simpset))));
   130 qed_spec_mp "new_keys_not_seen";
   131 Addsimps [new_keys_not_seen];
   132 
   133 (*Variant: old messages must contain old keys!*)
   134 goal thy 
   135  "!!evs. [| Says A B X : set_of_list evs;  \
   136 \           Key (newK evt) : parts {X};    \
   137 \           evs : yahalom lost                 \
   138 \        |] ==> length evt < length evs";
   139 by (rtac ccontr 1);
   140 by (dtac leI 1);
   141 by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
   142                       addIs  [impOfSubs parts_mono]) 1);
   143 qed "Says_imp_old_keys";
   144 
   145 
   146 (*Ready-made for the classical reasoner*)
   147 goal thy "!!evs. [| Says A B {|Crypt K {|b, Key (newK evs), na, nb|}, X|}  \
   148 \                   : set_of_list evs;  evs : yahalom lost |]              \
   149 \                ==> R";
   150 by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
   151                       addss (!simpset addsimps [parts_insertI])) 1);
   152 qed "Says_too_new_key";
   153 AddSEs [Says_too_new_key];
   154 
   155 
   156 (*Nobody can have USED keys that will be generated in the future.
   157   ...very like new_keys_not_seen*)
   158 goal thy "!!evs. evs : yahalom lost ==> \
   159 \                length evs <= length evs' --> \
   160 \                newK evs' ~: keysFor (parts (sees lost Spy evs))";
   161 by (parts_induct_tac 1);
   162 (*YM1, YM2 and YM3*)
   163 by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2]));
   164 (*Fake and Oops: these messages send unknown (X) components*)
   165 by (EVERY
   166     (map (fast_tac
   167           (!claset addDs [impOfSubs analz_subset_parts,
   168                           impOfSubs (analz_subset_parts RS keysFor_mono),
   169                           impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   170                           Suc_leD]
   171                    addss (!simpset))) [3,1]));
   172 (*YM4: if K was used then it had been seen, contradicting new_keys_not_seen*)
   173 by (fast_tac
   174       (!claset addSEs partsEs
   175                addSDs [Says_imp_sees_Spy RS parts.Inj]
   176                addEs [new_keys_not_seen RSN(2,rev_notE)]
   177                addDs [Suc_leD]) 1);
   178 qed_spec_mp "new_keys_not_used";
   179 
   180 bind_thm ("new_keys_not_analzd",
   181           [analz_subset_parts RS keysFor_mono,
   182            new_keys_not_used] MRS contra_subsetD);
   183 
   184 Addsimps [new_keys_not_used, new_keys_not_analzd];
   185 
   186 
   187 (*Describes the form of K when the Server sends this message.  Useful for
   188   Oops as well as main secrecy property.*)
   189 goal thy 
   190  "!!evs. [| Says Server A                                           \
   191 \            {|Crypt (shrK A) {|Agent B, K, NA, NB|}, X|} : set_of_list evs; \
   192 \           evs : yahalom lost |]                                   \
   193 \        ==> (EX evt: yahalom lost. K = Key(newK evt))";
   194 by (etac rev_mp 1);
   195 by (etac yahalom.induct 1);
   196 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   197 qed "Says_Server_message_form";
   198 
   199 
   200 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   201 val analz_Fake_tac = 
   202     forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
   203     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   204     assume_tac 7 THEN Full_simp_tac 7 THEN
   205     REPEAT ((etac bexE ORELSE' hyp_subst_tac) 7);
   206 
   207 
   208 (****
   209  The following is to prove theorems of the form
   210 
   211           Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) ==>
   212           Key K : analz (sees lost Spy evs)
   213 
   214  A more general formula must be proved inductively.
   215 
   216 ****)
   217 
   218 
   219 (*NOT useful in this form, but it says that session keys are not used
   220   to encrypt messages containing other keys, in the actual protocol.
   221   We require that agents should behave like this subsequently also.*)
   222 goal thy 
   223  "!!evs. evs : yahalom lost ==> \
   224 \        (Crypt (newK evt) X) : parts (sees lost Spy evs) & \
   225 \        Key K : parts {X} --> Key K : parts (sees lost Spy evs)";
   226 by (etac yahalom.induct 1);
   227 by parts_Fake_tac;
   228 by (ALLGOALS Asm_simp_tac);
   229 (*Deals with Faked messages*)
   230 by (best_tac (!claset addSEs partsEs
   231                       addDs [impOfSubs parts_insert_subset_Un]
   232                       addss (!simpset)) 2);
   233 (*Base case*)
   234 by (Auto_tac());
   235 result();
   236 
   237 
   238 (** Session keys are not used to encrypt other session keys **)
   239 
   240 goal thy  
   241  "!!evs. evs : yahalom lost ==> \
   242 \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   243 \           (K : newK``E | Key K : analz (sees lost Spy evs))";
   244 by (etac yahalom.induct 1);
   245 by analz_Fake_tac;
   246 by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
   247 by (ALLGOALS
   248     (asm_simp_tac 
   249      (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   250                          @ pushes)
   251                setloop split_tac [expand_if])));
   252 (** LEVEL 5 **)
   253 (*YM4, Fake*) 
   254 by (EVERY (map spy_analz_tac [4, 2]));
   255 (*Oops, YM3, Base*)
   256 by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   257 qed_spec_mp "analz_image_newK";
   258 
   259 goal thy
   260  "!!evs. evs : yahalom lost ==>                               \
   261 \        Key K : analz (insert (Key (newK evt)) (sees lost Spy evs)) = \
   262 \        (K = newK evt | Key K : analz (sees lost Spy evs))";
   263 by (asm_simp_tac (HOL_ss addsimps [analz_image_newK, 
   264                                    insert_Key_singleton]) 1);
   265 by (Fast_tac 1);
   266 qed "analz_insert_Key_newK";
   267 
   268 
   269 (*** The Key K uniquely identifies the Server's  message. **)
   270 
   271 goal thy 
   272  "!!evs. evs : yahalom lost ==>                                     \
   273 \      EX A' B' NA' NB' X'. ALL A B NA NB X.                             \
   274 \          Says Server A                                            \
   275 \           {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|}        \
   276 \          : set_of_list evs --> A=A' & B=B' & NA=NA' & NB=NB' & X=X'";
   277 by (etac yahalom.induct 1);
   278 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   279 by (Step_tac 1);
   280 by (ex_strip_tac 2);
   281 by (Fast_tac 2);
   282 (*Remaining case: YM3*)
   283 by (expand_case_tac "K = ?y" 1);
   284 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   285 (*...we assume X is a very new message, and handle this case by contradiction*)
   286 by (Fast_tac 1);  (*uses Says_too_new_key*)
   287 val lemma = result();
   288 
   289 goal thy 
   290 "!!evs. [| Says Server A                                            \
   291 \           {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|}        \
   292 \           : set_of_list evs;                                      \
   293 \          Says Server A'                                           \
   294 \           {|Crypt (shrK A') {|Agent B', Key K, NA', NB'|}, X'|}   \
   295 \           : set_of_list evs;                                      \
   296 \          evs : yahalom lost |]                                    \
   297 \       ==> A=A' & B=B' & NA=NA' & NB=NB'";
   298 by (dtac lemma 1);
   299 by (REPEAT (etac exE 1));
   300 (*Duplicate the assumption*)
   301 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   302 by (fast_tac (!claset addSDs [spec]) 1);
   303 qed "unique_session_keys";
   304 
   305 
   306 (*If the encrypted message appears then it originated with the Server*)
   307 goal thy
   308  "!!evs. [| Crypt (shrK A) {|Agent B, Key K, NA, NB|}                  \
   309 \            : parts (sees lost Spy evs);                              \
   310 \           A ~: lost;  evs : yahalom lost |]                          \
   311 \         ==> Says Server A                                            \
   312 \              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},            \
   313 \                Crypt (shrK B) {|Agent A, Key K|}|}                   \
   314 \             : set_of_list evs";
   315 by (etac rev_mp 1);
   316 by (parts_induct_tac 1);
   317 qed "A_trusts_YM3";
   318 
   319 
   320 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   321 
   322 goal thy 
   323  "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   324 \        ==> Says Server A                                        \
   325 \              {|Crypt (shrK A) {|Agent B, Key K, NA, NB|},       \
   326 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   327 \             : set_of_list evs -->                               \
   328 \            Says A Spy {|NA, NB, Key K|} ~: set_of_list evs -->  \
   329 \            Key K ~: analz (sees lost Spy evs)";
   330 by (etac yahalom.induct 1);
   331 by analz_Fake_tac;
   332 by (ALLGOALS
   333     (asm_simp_tac 
   334      (!simpset addsimps ([not_parts_not_analz,
   335                           analz_insert_Key_newK] @ pushes)
   336                setloop split_tac [expand_if])));
   337 (*YM3*)
   338 by (Fast_tac 2);  (*uses Says_too_new_key*)
   339 (*OR4, Fake*) 
   340 by (REPEAT_FIRST spy_analz_tac);
   341 (*Oops*) (** LEVEL 6 **)
   342 by (fast_tac (!claset delrules [disjE] 
   343                       addDs [unique_session_keys]
   344                       addss (!simpset)) 1);
   345 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   346 
   347 
   348 (*Final version: Server's message in the most abstract form*)
   349 goal thy 
   350  "!!evs. [| Says Server A                                               \
   351 \            {|Crypt (shrK A) {|Agent B, K, NA, NB|},                   \
   352 \              Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs;       \
   353 \           Says A Spy {|NA, NB, K|} ~: set_of_list evs;                \
   354 \           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
   355 \     K ~: analz (sees lost Spy evs)";
   356 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   357 by (fast_tac (!claset addSEs [lemma]) 1);
   358 qed "Spy_not_see_encrypted_key";
   359 
   360 
   361 goal thy 
   362  "!!evs. [| C ~: {A,B,Server};                                          \
   363 \           Says Server A                                               \
   364 \            {|Crypt (shrK A) {|Agent B, K, NA, NB|},                   \
   365 \              Crypt (shrK B) {|Agent A, K|}|} : set_of_list evs;       \
   366 \           Says A Spy {|NA, NB, K|} ~: set_of_list evs;                \
   367 \           A ~: lost;  B ~: lost;  evs : yahalom lost |] ==>           \
   368 \     K ~: analz (sees lost C evs)";
   369 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   370 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   371 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   372 by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD])));
   373 qed "Agent_not_see_encrypted_key";
   374 
   375 
   376 (*** Security Guarantee for B upon receiving YM4 ***)
   377 
   378 (*B knows, by the first part of A's message, that the Server distributed 
   379   the key for A and B.  But this part says nothing about nonces.*)
   380 goal thy 
   381  "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees lost Spy evs); \
   382 \           B ~: lost;  evs : yahalom lost |]                           \
   383 \        ==> EX NA NB. Says Server A                                    \
   384 \                        {|Crypt (shrK A) {|Agent B, Key K,                      \
   385 \                                  Nonce NA, Nonce NB|},       \
   386 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   387 \                       : set_of_list evs";
   388 by (etac rev_mp 1);
   389 by (parts_induct_tac 1);
   390 (*YM3*)
   391 by (Fast_tac 1);
   392 qed "B_trusts_YM4_shrK";
   393 
   394 
   395 (*** General properties of nonces ***)
   396 
   397 goal thy "!!evs. evs : yahalom lost ==> \
   398 \                length evs <= length evt --> \
   399 \                Nonce (newN evt) ~: parts (sees lost Spy evs)";
   400 by (parts_induct_tac 1);
   401 by (REPEAT_FIRST (fast_tac (!claset 
   402                               addSEs partsEs
   403                               addSDs  [Says_imp_sees_Spy RS parts.Inj]
   404                               addEs  [leD RS notE]
   405 			      addDs  [impOfSubs analz_subset_parts,
   406                                       impOfSubs parts_insert_subset_Un,
   407                                       Suc_leD]
   408                               addss (!simpset))));
   409 qed_spec_mp "new_nonces_not_seen";
   410 Addsimps [new_nonces_not_seen];
   411 
   412 (*Variant: old messages must contain old nonces!*)
   413 goal thy 
   414  "!!evs. [| Says A B X : set_of_list evs;      \
   415 \           Nonce (newN evt) : parts {X};      \
   416 \           evs : yahalom lost                 \
   417 \        |] ==> length evt < length evs";
   418 by (rtac ccontr 1);
   419 by (dtac leI 1);
   420 by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
   421                       addIs  [impOfSubs parts_mono]) 1);
   422 qed "Says_imp_old_nonces";
   423 
   424 
   425 (** The Nonce NB uniquely identifies B's message. **)
   426 
   427 val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
   428 
   429 goal thy 
   430  "!!evs. evs : yahalom lost ==> EX NA' A' B'. ALL NA A B. \
   431 \      Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \
   432 \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
   433 by (parts_induct_tac 1);  (*100 seconds??*)
   434 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   435 (*YM2: creation of new Nonce.  Move assertion into global context*)
   436 by (expand_case_tac "NB = ?y" 1);
   437 by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
   438 val lemma = result();
   439 
   440 goal thy 
   441  "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, NB|} \
   442 \                  : parts (sees lost Spy evs);         \
   443 \          Crypt (shrK B') {|Agent A', Nonce NA', NB|} \
   444 \                  : parts (sees lost Spy evs);         \
   445 \          evs : yahalom lost;  B ~: lost;  B' ~: lost |]  \
   446 \        ==> NA' = NA & A' = A & B' = B";
   447 by (dtac lemma 1);
   448 by (REPEAT (etac exE 1));
   449 (*Duplicate the assumption*)
   450 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   451 by (fast_tac (!claset addSDs [spec]) 1);
   452 qed "unique_NB";
   453 
   454 (*OLD VERSION
   455 fun lost_tac s =
   456     case_tac ("(" ^ s ^ ") : lost") THEN'
   457     SELECT_GOAL 
   458       (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
   459        REPEAT_DETERM (etac MPair_analz 1) THEN
   460        dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN
   461        assume_tac 1 THEN Fast_tac 1);
   462 *)
   463 
   464 fun lost_tac s =
   465     case_tac ("(" ^ s ^ ") : lost") THEN'
   466     SELECT_GOAL 
   467       (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
   468        REPEAT_DETERM (etac MPair_analz 1) THEN
   469        THEN_BEST_FIRST 
   470          (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
   471          (has_fewer_prems 1, size_of_thm)
   472          (Step_tac 1));
   473 
   474 
   475 (*Variant useful for proving secrecy of NB*)
   476 goal thy 
   477  "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, NB|}|} \
   478 \          : set_of_list evs;  B ~: lost;         \
   479 \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
   480 \          : set_of_list evs;                           \
   481 \          NB ~: analz (sees lost Spy evs);             \
   482 \          evs : yahalom lost |]  \
   483 \        ==> NA' = NA & A' = A & B' = B";
   484 by (lost_tac "B'" 1);
   485 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   486                       addSEs [MPair_parts]
   487                       addDs  [unique_NB]) 1);
   488 qed "Says_unique_NB";
   489 
   490 goal thy 
   491  "!!evs. [| B ~: lost;  evs : yahalom lost  |]               \
   492 \ ==>  Nonce NB ~: analz (sees lost Spy evs) -->  \
   493 \      Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} : parts (sees lost Spy evs) \
   494 \ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts (sees lost Spy evs)";
   495 by (etac yahalom.induct 1);
   496 by parts_Fake_tac;
   497 by (REPEAT_FIRST 
   498     (rtac impI THEN' 
   499      dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
   500      mp_tac));
   501 by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   502                              impOfSubs Fake_parts_insert]
   503                       addss (!simpset)) 2);
   504 by (ALLGOALS Asm_simp_tac);
   505 by (fast_tac (!claset addss (!simpset)) 1);
   506 by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
   507                       addSIs [parts_insertI]
   508                       addSEs partsEs
   509                       addEs [Says_imp_old_nonces RS less_irrefl]
   510                       addss (!simpset)) 1);
   511 val no_nonce_YM1_YM2 = standard (result() RS mp RSN (2, rev_mp) RS notE);
   512 
   513 
   514 
   515 (**** Towards proving secrecy of Nonce NB ****)
   516 
   517 (*B knows, by the second part of A's message, that the Server distributed 
   518   the key quoting nonce NB.  This part says nothing about agent names. 
   519   Secrecy of NB is crucial.*)
   520 goal thy 
   521  "!!evs. evs : yahalom lost                                             \
   522 \        ==> Nonce NB ~: analz (sees lost Spy evs) -->                  \
   523 \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   524 \            (EX A B NA. Says Server A                                  \
   525 \                        {|Crypt (shrK A) {|Agent B, Key K,                      \
   526 \                                  Nonce NA, Nonce NB|},       \
   527 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   528 \                       : set_of_list evs)";
   529 by (etac yahalom.induct 1);
   530 by parts_Fake_tac;
   531 by (fast_tac (!claset addss (!simpset)) 1);
   532 by (REPEAT_FIRST
   533     (rtac impI THEN'
   534      dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
   535 by (ALLGOALS Asm_simp_tac);
   536 (*Fake, YM3, YM4*)
   537 by (Fast_tac 2);
   538 by (fast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   539                       addDs [impOfSubs analz_subset_parts]
   540                       addss (!simpset)) 1);
   541 (*YM4*)
   542 by (Step_tac 1);
   543 by (lost_tac "A" 1);
   544 by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
   545                              A_trusts_YM3]) 1);
   546 val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
   547 
   548 
   549 (*This is the original version of the result above.  But it is of little
   550   value because it assumes secrecy of K, which we cannot be assured of
   551   until we know that K is fresh -- which we do not know at the point this
   552   result is applied.*)
   553 goal thy 
   554  "!!evs. evs : yahalom lost                                             \
   555 \        ==> Key K ~: analz (sees lost Spy evs) -->                     \
   556 \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   557 \            (EX A B NA. Says Server A                                  \
   558 \                        {|Crypt (shrK A) {|Agent B, Key K,                      \
   559 \                                  Nonce NA, Nonce NB|},       \
   560 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   561 \                       : set_of_list evs)";
   562 by (etac yahalom.induct 1);
   563 by parts_Fake_tac;
   564 by (fast_tac (!claset addss (!simpset)) 1);
   565 by (TRYALL (rtac impI));
   566 by (REPEAT_FIRST
   567     (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
   568 by (ALLGOALS Asm_simp_tac);
   569 (*Fake, YM3, YM4*)
   570 by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert]
   571                       addDs  [impOfSubs analz_subset_parts]) 1);
   572 by (Fast_tac 1);
   573 (*YM4*)
   574 by (Step_tac 1);
   575 by (lost_tac "A" 1);
   576 by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
   577                              A_trusts_YM3]) 1);
   578 result() RS mp RSN (2, rev_mp);
   579 
   580 
   581 (*YM3 can only be triggered by YM2*)
   582 goal thy 
   583  "!!evs. [| Says Server A                                           \
   584 \            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \
   585 \           evs : yahalom lost |]                                        \
   586 \        ==> EX B'. Says B' Server                                       \
   587 \                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
   588 \                   : set_of_list evs";
   589 by (etac rev_mp 1);
   590 by (etac yahalom.induct 1);
   591 by (ALLGOALS Asm_simp_tac);
   592 by (ALLGOALS Fast_tac);
   593 qed "Says_Server_imp_YM2";
   594 
   595 
   596 (** Dedicated tactics for the nonce secrecy proofs **)
   597 
   598 val no_nonce_tac = SELECT_GOAL
   599    (REPEAT (resolve_tac [impI, notI] 1) THEN
   600     REPEAT (hyp_subst_tac 1) THEN
   601     etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS no_nonce_YM1_YM2) 1
   602     THEN
   603     etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd) 4
   604     THEN 
   605     REPEAT_FIRST assume_tac);
   606 
   607 val not_analz_insert = subset_insertI RS analz_mono RS contra_subsetD;
   608 
   609 fun grind_tac i = 
   610  SELECT_GOAL
   611   (REPEAT_FIRST 
   612    (Safe_step_tac ORELSE' (dtac spec THEN' mp_tac) ORELSE'
   613     assume_tac ORELSE'
   614     depth_tac (!claset delrules [conjI]
   615                        addSIs [exI, analz_insertI,
   616                                impOfSubs (Un_upper2 RS analz_mono)]) 2)) i;
   617 
   618 (*The only nonces that can be found with the help of session keys are
   619   those distributed as nonce NB by the Server.  The form of the theorem
   620   recalls analz_image_newK, but it is much more complicated.*)
   621 goal thy 
   622  "!!evs. evs : yahalom lost ==>                                           \
   623 \     ALL E. Nonce NB : analz (Key``(newK``E) Un (sees lost Spy evs)) --> \
   624 \     (EX K: newK``E. EX A B na X.                                        \
   625 \            Says Server A                                                \
   626 \                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}   \
   627 \            : set_of_list evs)  |  Nonce NB : analz (sees lost Spy evs)";
   628 by (etac yahalom.induct 1);
   629 by analz_Fake_tac;
   630 by (ALLGOALS  (*28 seconds*)
   631     (asm_simp_tac 
   632      (!simpset addsimps ([not_parts_not_analz,
   633                           analz_image_newK,
   634                           insert_Key_singleton, insert_Key_image]
   635                          @ pushes)
   636                setloop split_tac [expand_if])));
   637 (*Base*)
   638 by (fast_tac (!claset addss (!simpset)) 1);
   639 (*Fake*) (** LEVEL 4 **)
   640 by (spy_analz_tac 1);
   641 (*YM1-YM3*) (*29 seconds*)
   642 by (EVERY (map grind_tac [3,2,1]));
   643 (*Oops*)
   644 by (Full_simp_tac 2);
   645 by (REPEAT ((etac bexE ORELSE' hyp_subst_tac) 2));
   646 by (simp_tac (!simpset addsimps [insert_Key_image]) 2);
   647 by (grind_tac 2);
   648 by (fast_tac (!claset delrules [bexI] 
   649                       addDs [unique_session_keys]
   650                       addss (!simpset)) 2);
   651 (*YM4*)
   652 (** LEVEL 11 **)
   653 by (rtac (impI RS allI) 1);
   654 by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1);
   655 by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
   656 by (asm_simp_tac (!simpset addsimps [analz_image_newK]
   657                            setloop split_tac [expand_if]) 1);
   658 (** LEVEL 15 **)
   659 by (grind_tac 1);
   660 by (REPEAT (dtac not_analz_insert 1));
   661 by (lost_tac "A" 1);
   662 by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   663     THEN REPEAT (assume_tac 1));
   664 by (fast_tac (!claset delrules [allE, conjI] addSIs [bexI, exI]) 1);
   665 by (fast_tac (!claset delrules [conjI]
   666                       addIs [analz_insertI]
   667                       addss (!simpset)) 1);
   668 val Nonce_secrecy = result() RS spec RSN (2, rev_mp) |> standard;
   669 
   670 
   671 (*Version required below: if NB can be decrypted using a session key then it
   672   was distributed with that key.  The more general form above is required
   673   for the induction to carry through.*)
   674 goal thy 
   675  "!!evs. [| Says Server A                                                     \
   676 \            {|Crypt (shrK A) {|Agent B, Key (newK evt), na, Nonce NB'|}, X|} \
   677 \           : set_of_list evs;                                                \
   678 \           Nonce NB : analz (insert (Key (newK evt)) (sees lost Spy evs));   \
   679 \           evs : yahalom lost |]                                             \
   680 \ ==> Nonce NB : analz (sees lost Spy evs) | NB = NB'";
   681 by (asm_full_simp_tac (HOL_ss addsimps [insert_Key_singleton]) 1);
   682 by (dtac Nonce_secrecy 1 THEN assume_tac 1);
   683 by (fast_tac (!claset addDs [unique_session_keys]
   684                       addss (!simpset)) 1);
   685 val single_Nonce_secrecy = result();
   686 
   687 
   688 goal thy 
   689  "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
   690 \ ==> Says B Server                                                    \
   691 \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   692 \     : set_of_list evs -->                               \
   693 \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) -->  \
   694 \     Nonce NB ~: analz (sees lost Spy evs)";
   695 by (etac yahalom.induct 1);
   696 by analz_Fake_tac;
   697 by (ALLGOALS
   698     (asm_simp_tac 
   699      (!simpset addsimps ([not_parts_not_analz,
   700                           analz_insert_Key_newK] @ pushes)
   701                setloop split_tac [expand_if])));
   702 by (fast_tac (!claset addSIs [parts_insertI]
   703                       addSEs partsEs
   704                       addEs [Says_imp_old_nonces RS less_irrefl]
   705                       addss (!simpset)) 2);
   706 (*Proof of YM2*) (** LEVEL 4 **)
   707 by (REPEAT (Safe_step_tac 2 ORELSE Fast_tac 2)); 
   708 by (fast_tac (!claset addIs [parts_insertI]
   709                       addSEs partsEs
   710                       addEs [Says_imp_old_nonces RS less_irrefl]
   711                       addss (!simpset)) 3);
   712 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 2);
   713 (*Prove YM3 by showing that no NB can also be an NA*)
   714 by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2));
   715 by (deepen_tac (!claset addDs [Says_unique_NB]) 1 2);
   716 (*Fake*)
   717 by (spy_analz_tac 1);
   718 (*YM4*) (** LEVEL 10 **)
   719 by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1);
   720 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   721 by (SELECT_GOAL (REPEAT_FIRST (spy_analz_tac ORELSE' Safe_step_tac)) 1);
   722 (** LEVEL 13 **)
   723 by (lost_tac "Aa" 1);
   724 by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
   725 by (forward_tac [Says_Server_message_form] 3);
   726 by (forward_tac [Says_Server_imp_YM2] 4);
   727 by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
   728 by (Full_simp_tac 1);
   729 by (REPEAT_FIRST hyp_subst_tac);
   730 (** LEVEL 20 **)
   731 by (lost_tac "Ba" 1);
   732 by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1);
   733 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   734                       addSEs [MPair_parts]) 1);
   735 by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1)); 
   736 by (dtac Spy_not_see_encrypted_key 1);
   737 by (REPEAT (assume_tac 1 ORELSE Fast_tac 1)); 
   738 by (spy_analz_tac 1);
   739 (*Oops case*) (** LEVEL 27 **)
   740 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   741 by (step_tac (!claset delrules [disjE, conjI]) 1);
   742 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   743 by (expand_case_tac "NB = NBa" 1);
   744 by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1);
   745 by (rtac conjI 1);
   746 by (no_nonce_tac 1);
   747 (** LEVEL 34 **)
   748 by (thin_tac "?PP|?QQ" 1);  (*subsumption!*)
   749 by (fast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
   750 val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) |> standard;
   751 
   752 
   753 (*What can B deduce from receipt of YM4?  Note how the two components of
   754   the message contribute to a single conclusion about the Server's message.
   755   It's annoying that the "Says A Spy" assumption must quantify over 
   756   ALL POSSIBLE keys instead of our particular K (though at least the
   757   nonces are forced to agree with NA and NB). *)
   758 goal thy 
   759  "!!evs. [| Says B Server                                        \
   760 \            {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}  \
   761 \           : set_of_list evs;       \
   762 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},              \
   763 \                       Crypt K (Nonce NB)|} : set_of_list evs;         \
   764 \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
   765 \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]   \
   766 \         ==> Says Server A                                       \
   767 \                     {|Crypt (shrK A) {|Agent B, Key K,                         \
   768 \                               Nonce NA, Nonce NB|},          \
   769 \                       Crypt (shrK B) {|Agent A, Key K|}|}             \
   770 \                   : set_of_list evs";
   771 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   772 by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
   773     dtac B_trusts_YM4_shrK 1);
   774 by (dtac B_trusts_YM4_newK 3);
   775 by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   776 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   777 by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
   778 by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
   779 qed "B_trusts_YM4";
   780