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