src/HOL/Auth/Yahalom.ML
author paulson
Tue Nov 05 11:20:52 1996 +0100 (1996-11-05)
changeset 2160 ad4382e546fc
parent 2156 9c361df93bd5
child 2170 c5e460f1ebb4
permissions -rw-r--r--
Simplified new_keys_not_seen, etc.: replaced the
union over all
agents by the Spy alone. Proofs run faster and they do not have to be
set up in terms of a previous lemma.
     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 (Nonce NB) K|} : 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 Y (shrK A), 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 {|B, K, NA, NB|} (shrK A), 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 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 {|b, Key (newK evs), na, nb|} K, 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 {|Agent B, K, NA, NB|} (shrK A), 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 X (newK evt)) : 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 {|Agent B, Key K, NA, NB|} (shrK A), 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 {|Agent B, Key K, NA, NB|} (shrK A), X|}        \
   292 \           : set_of_list evs;                                      \
   293 \          Says Server A'                                           \
   294 \           {|Crypt {|Agent B', Key K, NA', NB'|} (shrK A'), 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 {|Agent B, Key K, NA, NB|} (shrK A)                  \
   309 \            : parts (sees lost Spy evs);                              \
   310 \           A ~: lost;  evs : yahalom lost |]                          \
   311 \         ==> Says Server A                                            \
   312 \              {|Crypt {|Agent B, Key K, NA, NB|} (shrK A),            \
   313 \                Crypt {|Agent A, Key K|} (shrK B)|}                   \
   314 \             : set_of_list evs";
   315 by (etac rev_mp 1);
   316 by (parts_induct_tac 1);
   317 qed "A_trust_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 {|Agent B, Key K, NA, NB|} (shrK A),       \
   326 \                Crypt {|Agent A, Key K|} (shrK B)|}              \
   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 ([analz_subset_parts RS contra_subsetD,
   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 (resolve_tac [conjI, impI] ORELSE' 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 {|Agent B, K, NA, NB|} (shrK A),                   \
   352 \              Crypt {|Agent A, K|} (shrK B)|} : 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 {|Agent B, K, NA, NB|} (shrK A),                   \
   365 \              Crypt {|Agent A, K|} (shrK B)|} : 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 {|Agent A, Key K|} (shrK B) : parts (sees lost Spy evs); \
   382 \           B ~: lost;  evs : yahalom lost |]                           \
   383 \        ==> EX NA NB. Says Server A                                    \
   384 \                        {|Crypt {|Agent B, Key K,                      \
   385 \                                  Nonce NA, Nonce NB|} (shrK A),       \
   386 \                          Crypt {|Agent A, Key K|} (shrK B)|}          \
   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                               addDs  [impOfSubs analz_subset_parts,
   405                                       impOfSubs parts_insert_subset_Un,
   406                                       Suc_leD]
   407                               addss (!simpset))));
   408 qed_spec_mp "new_nonces_not_seen";
   409 Addsimps [new_nonces_not_seen];
   410 
   411 (*Variant: old messages must contain old nonces!*)
   412 goal thy 
   413  "!!evs. [| Says A B X : set_of_list evs;      \
   414 \           Nonce (newN evt) : parts {X};      \
   415 \           evs : yahalom lost                 \
   416 \        |] ==> length evt < length evs";
   417 by (rtac ccontr 1);
   418 by (dtac leI 1);
   419 by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
   420                       addIs  [impOfSubs parts_mono]) 1);
   421 qed "Says_imp_old_nonces";
   422 
   423 
   424 (** The Nonce NB uniquely identifies B's message. **)
   425 
   426 val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
   427 
   428 goal thy 
   429  "!!evs. evs : yahalom lost ==> EX NA' A' B'. ALL NA A B. \
   430 \      Crypt {|Agent A, Nonce NA, NB|} (shrK B) : parts(sees lost Spy evs) \
   431 \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
   432 by (parts_induct_tac 1);  (*100 seconds??*)
   433 by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   434 (*YM2: creation of new Nonce.  Move assertion into global context*)
   435 by (expand_case_tac "NB = ?y" 1);
   436 by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1);
   437 val lemma = result();
   438 
   439 goal thy 
   440  "!!evs.[| Crypt {|Agent A, Nonce NA, NB|} (shrK B) \
   441 \                  : parts (sees lost Spy evs);         \
   442 \          Crypt {|Agent A', Nonce NA', NB|} (shrK B') \
   443 \                  : parts (sees lost Spy evs);         \
   444 \          evs : yahalom lost;  B ~: lost;  B' ~: lost |]  \
   445 \        ==> NA' = NA & A' = A & B' = B";
   446 by (dtac lemma 1);
   447 by (REPEAT (etac exE 1));
   448 (*Duplicate the assumption*)
   449 by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1);
   450 by (fast_tac (!claset addSDs [spec]) 1);
   451 qed "unique_NB";
   452 
   453 fun lost_tac s =
   454     case_tac ("(" ^ s ^ ") : lost") THEN'
   455     SELECT_GOAL 
   456       (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
   457        REPEAT_DETERM (etac MPair_analz 1) THEN
   458        dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN
   459        assume_tac 1 THEN Fast_tac 1);
   460 
   461 fun lost_tac s =
   462     case_tac ("(" ^ s ^ ") : lost") THEN'
   463     SELECT_GOAL 
   464       (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN
   465        REPEAT_DETERM (etac MPair_analz 1) THEN
   466        THEN_BEST_FIRST 
   467          (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1)
   468  	 (has_fewer_prems 1, size_of_thm)
   469 	 (Step_tac 1));
   470 
   471 
   472 (*Variant useful for proving secrecy of NB*)
   473 goal thy 
   474  "!!evs.[| Says C D   {|X,  Crypt {|Agent A, Nonce NA, NB|} (shrK B)|} \
   475 \          : set_of_list evs;  B ~: lost;         \
   476 \          Says C' D' {|X', Crypt {|Agent A', Nonce NA', NB|} (shrK B')|} \
   477 \          : set_of_list evs;                           \
   478 \          NB ~: analz (sees lost Spy evs);             \
   479 \          evs : yahalom lost |]  \
   480 \        ==> NA' = NA & A' = A & B' = B";
   481 by (lost_tac "B'" 1);
   482 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   483                       addSEs [MPair_parts]
   484                       addDs  [unique_NB]) 1);
   485 qed "Says_unique_NB";
   486 
   487 goal thy 
   488  "!!evs. [| B ~: lost;  evs : yahalom lost  |]               \
   489 \ ==>  Nonce NB ~: analz (sees lost Spy evs) -->  \
   490 \      Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B) : parts (sees lost Spy evs) \
   491 \ --> Crypt {|Agent A', Nonce NB, NB'|} (shrK B') ~: parts (sees lost Spy evs)";
   492 by (etac yahalom.induct 1);
   493 by parts_Fake_tac;
   494 by (REPEAT_FIRST 
   495     (rtac impI THEN' 
   496      dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
   497      mp_tac));
   498 by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   499 			     impOfSubs Fake_parts_insert]
   500 	              addss (!simpset)) 2);
   501 by (ALLGOALS Asm_simp_tac);
   502 by (fast_tac (!claset addss (!simpset)) 1);
   503 by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
   504 	              addSIs [parts_insertI]
   505                       addSEs partsEs
   506                       addEs [Says_imp_old_nonces RS less_irrefl]
   507                       addss (!simpset)) 1);
   508 val no_nonce_YM1_YM2 = standard (result() RS mp RSN (2, rev_mp) RS notE);
   509 
   510 
   511 
   512 (**** Towards proving secrecy of Nonce NB ****)
   513 
   514 (*B knows, by the second part of A's message, that the Server distributed 
   515   the key quoting nonce NB.  This part says nothing about agent names. 
   516   Secrecy of NB is crucial.*)
   517 goal thy 
   518  "!!evs. evs : yahalom lost                                             \
   519 \        ==> Nonce NB ~: analz (sees lost Spy evs) -->                  \
   520 \            Crypt (Nonce NB) K : parts (sees lost Spy evs) -->         \
   521 \            (EX A B NA. Says Server A                                  \
   522 \                        {|Crypt {|Agent B, Key K,                      \
   523 \                                  Nonce NA, Nonce NB|} (shrK A),       \
   524 \                          Crypt {|Agent A, Key K|} (shrK B)|}          \
   525 \                       : set_of_list evs)";
   526 by (etac yahalom.induct 1);
   527 by parts_Fake_tac;
   528 by (fast_tac (!claset addss (!simpset)) 1);
   529 by (REPEAT_FIRST
   530     (rtac impI THEN'
   531      dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
   532 by (ALLGOALS Asm_simp_tac);
   533 (*Fake, YM3, YM4*)
   534 by (Fast_tac 2);
   535 by (fast_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   536                       addDs [impOfSubs analz_subset_parts]
   537                       addss (!simpset)) 1);
   538 (*YM4*)
   539 by (Step_tac 1);
   540 by (lost_tac "A" 1);
   541 by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
   542 			     A_trust_YM3]) 1);
   543 val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
   544 
   545 
   546 (*This is the original version of the result above.  But it is of little
   547   value because it assumes secrecy of K, which we cannot be assured of
   548   until we know that K is fresh -- which we do not know at the point this
   549   result is applied.*)
   550 goal thy 
   551  "!!evs. evs : yahalom lost                                             \
   552 \        ==> Key K ~: analz (sees lost Spy evs) -->                     \
   553 \            Crypt (Nonce NB) K : parts (sees lost Spy evs) -->         \
   554 \            (EX A B NA. Says Server A                                  \
   555 \                        {|Crypt {|Agent B, Key K,                      \
   556 \                                  Nonce NA, Nonce NB|} (shrK A),       \
   557 \                          Crypt {|Agent A, Key K|} (shrK B)|}          \
   558 \                       : set_of_list evs)";
   559 by (etac yahalom.induct 1);
   560 by parts_Fake_tac;
   561 by (fast_tac (!claset addss (!simpset)) 1);
   562 by (TRYALL (rtac impI));
   563 by (REPEAT_FIRST
   564     (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD)));
   565 by (ALLGOALS Asm_simp_tac);
   566 (*Fake, YM3, YM4*)
   567 by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert]
   568                       addDs  [impOfSubs analz_subset_parts]) 1);
   569 by (Fast_tac 1);
   570 (*YM4*)
   571 by (Step_tac 1);
   572 by (lost_tac "A" 1);
   573 by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
   574 			     A_trust_YM3]) 1);
   575 result() RS mp RSN (2, rev_mp);
   576 
   577 
   578 (*YM3 can only be triggered by YM2*)
   579 goal thy 
   580  "!!evs. [| Says Server A                                           \
   581 \            {|Crypt {|Agent B, k, na, nb|} (shrK A), X|} : set_of_list evs; \
   582 \           evs : yahalom lost |]                                        \
   583 \        ==> EX B'. Says B' Server                                       \
   584 \                      {| Agent B, Crypt {|Agent A, na, nb|} (shrK B) |} \
   585 \                   : set_of_list evs";
   586 by (etac rev_mp 1);
   587 by (etac yahalom.induct 1);
   588 by (ALLGOALS Asm_simp_tac);
   589 by (ALLGOALS Fast_tac);
   590 qed "Says_Server_imp_YM2";
   591 
   592 
   593 (** Dedicated tactics for the nonce secrecy proofs **)
   594 
   595 val no_nonce_tac = SELECT_GOAL
   596    (REPEAT (resolve_tac [impI, notI] 1) THEN
   597     REPEAT (hyp_subst_tac 1) THEN
   598     etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS no_nonce_YM1_YM2) 1
   599     THEN
   600     etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd) 4
   601     THEN 
   602     REPEAT_FIRST assume_tac);
   603 
   604 val not_analz_insert = subset_insertI RS analz_mono RS contra_subsetD;
   605 
   606 fun grind_tac i = 
   607  SELECT_GOAL
   608   (REPEAT_FIRST 
   609    (Safe_step_tac ORELSE' (dtac spec THEN' mp_tac) ORELSE'
   610     assume_tac ORELSE'
   611     depth_tac (!claset delrules [conjI]
   612 		       addSIs [exI, impOfSubs (subset_insertI RS analz_mono),
   613 			       impOfSubs (Un_upper2 RS analz_mono)]) 2)) i;
   614 
   615 (*The only nonces that can be found with the help of session keys are
   616   those distributed as nonce NB by the Server.  The form of the theorem
   617   recalls analz_image_newK, but it is much more complicated.*)
   618 goal thy 
   619  "!!evs. evs : yahalom lost ==>                                           \
   620 \     ALL E. Nonce NB : analz (Key``(newK``E) Un (sees lost Spy evs)) --> \
   621 \     (EX K: newK``E. EX A B na X.                                        \
   622 \            Says Server A                                                \
   623 \                {|Crypt {|Agent B, Key K, na, Nonce NB|} (shrK A), X|}   \
   624 \            : set_of_list evs)  |  Nonce NB : analz (sees lost Spy evs)";
   625 by (etac yahalom.induct 1);
   626 by analz_Fake_tac;
   627 by (ALLGOALS  (*28 seconds*)
   628     (asm_simp_tac 
   629      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   630                           analz_image_newK,
   631 			  insert_Key_singleton, insert_Key_image]
   632 			 @ pushes)
   633                setloop split_tac [expand_if])));
   634 (*Base*)
   635 by (fast_tac (!claset addss (!simpset)) 1);
   636 (*Fake*) (** LEVEL 4 **)
   637 by (spy_analz_tac 1);
   638 (*YM1-YM3*) (*29 seconds*)
   639 by (EVERY (map grind_tac [3,2,1]));
   640 (*Oops*)
   641 by (Full_simp_tac 2);
   642 by (REPEAT ((eresolve_tac [bexE] ORELSE' hyp_subst_tac) 2));
   643 by (simp_tac (!simpset addsimps [insert_Key_image]) 2);
   644 by (grind_tac 2);
   645 by (fast_tac (!claset delrules [bexI] 
   646 		      addDs [unique_session_keys]
   647 	              addss (!simpset)) 2);
   648 (*YM4*)
   649 (** LEVEL 11 **)
   650 br (impI RS allI) 1;
   651 by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1 THEN 
   652     Fast_tac 1);
   653 by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
   654 by (asm_simp_tac (!simpset addsimps [analz_image_newK]
   655 	                   setloop split_tac [expand_if]) 1);
   656 (** LEVEL 15 **)
   657 by (grind_tac 1);
   658 by (REPEAT (dtac not_analz_insert 1));
   659 by (lost_tac "A" 1);
   660 by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trust_YM3) 1
   661     THEN REPEAT (assume_tac 1));
   662 by (fast_tac (!claset delrules [allE, conjI] addSIs [bexI, exI]) 1);
   663 by (fast_tac (!claset delrules [conjI]
   664 	              addIs [impOfSubs (subset_insertI RS analz_mono)]
   665 		      addss (!simpset)) 1);
   666 val Nonce_secrecy = result() RS spec RSN (2, rev_mp) |> standard;
   667 
   668 
   669 (*Version required below: if NB can be decrypted using a session key then it
   670   was distributed with that key.  The more general form above is required
   671   for the induction to carry through.*)
   672 goal thy 
   673  "!!evs. [| Says Server A                                                     \
   674 \            {|Crypt {|Agent B, Key (newK evt), na, Nonce NB'|} (shrK A), X|} \
   675 \           : set_of_list evs;                                                \
   676 \           Nonce NB : analz (insert (Key (newK evt)) (sees lost Spy evs));   \
   677 \           evs : yahalom lost |]                                             \
   678 \ ==> Nonce NB : analz (sees lost Spy evs) | NB = NB'";
   679 by (asm_full_simp_tac (HOL_ss addsimps [insert_Key_singleton]) 1);
   680 by (dtac Nonce_secrecy 1 THEN assume_tac 1);
   681 by (fast_tac (!claset addDs [unique_session_keys]
   682 	              addss (!simpset)) 1);
   683 val single_Nonce_secrecy = result();
   684 
   685 
   686 goal thy 
   687  "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
   688 \ ==> Says B Server                                                    \
   689 \          {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|} \
   690 \     : set_of_list evs -->                               \
   691 \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) -->  \
   692 \     Nonce NB ~: analz (sees lost Spy evs)";
   693 by (etac yahalom.induct 1);
   694 by analz_Fake_tac;
   695 by (ALLGOALS
   696     (asm_simp_tac 
   697      (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   698                           analz_insert_Key_newK] @ pushes)
   699                setloop split_tac [expand_if])));
   700 by (fast_tac (!claset addSIs [parts_insertI]
   701                       addSEs partsEs
   702                       addEs [Says_imp_old_nonces RS less_irrefl]
   703                       addss (!simpset)) 2);
   704 (*Proof of YM2*) (** LEVEL 5 **)
   705 by (REPEAT (Safe_step_tac 2 ORELSE Fast_tac 2)); 
   706 by (fast_tac (!claset addIs [parts_insertI]
   707                       addSEs partsEs
   708                       addEs [Says_imp_old_nonces RS less_irrefl]
   709                       addss (!simpset)) 3);
   710 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 2);
   711 (*Prove YM3 by showing that no NB can also be an NA*)
   712 by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2));
   713 by (deepen_tac (!claset addDs [Says_unique_NB]) 1 2);
   714 (*Fake*) (** LEVEL 10 **)
   715 by (SELECT_GOAL (REPEAT (Safe_step_tac 1 ORELSE spy_analz_tac 1)) 1);
   716 (*YM4*)
   717 by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1);
   718 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
   719 by (SELECT_GOAL (REPEAT_FIRST (Safe_step_tac ORELSE' spy_analz_tac)) 1);
   720 (** LEVEL 14 **)
   721 by (lost_tac "Aa" 1);
   722 bd (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trust_YM3) 1;
   723 by (forward_tac [Says_Server_message_form] 3);
   724 by (forward_tac [Says_Server_imp_YM2] 4);
   725 by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE])));
   726 by (Full_simp_tac 1);
   727 (** LEVEL 20 **)
   728 by (REPEAT_FIRST hyp_subst_tac);
   729 by (lost_tac "Ba" 1);
   730 bd (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1;
   731 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   732                       addSEs [MPair_parts]) 1);
   733 by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1)); 
   734 bd Spy_not_see_encrypted_key 1;
   735 by (REPEAT (assume_tac 1 ORELSE Fast_tac 1)); 
   736 by (spy_analz_tac 1);
   737 (*Oops case*) (** LEVEL 28 **)
   738 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   739 by (step_tac (!claset delrules [disjE, conjI]) 1);
   740 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   741 by (expand_case_tac "NB = NBa" 1);
   742 by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1);
   743 br conjI 1;
   744 by (no_nonce_tac 1);
   745 (** LEVEL 35 **)
   746 by (thin_tac "?PP|?QQ" 1);  (*subsumption!*)
   747 by (fast_tac (!claset addSDs [single_Nonce_secrecy]) 1);
   748 val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) |> standard;
   749 
   750 
   751 (*What can B deduce from receipt of YM4?  Note how the two components of
   752   the message contribute to a single conclusion about the Server's message.
   753   It's annoying that the "Says A Spy" assumption must quantify over 
   754   ALL POSSIBLE keys instead of our particular K (though at least the
   755   nonces are forced to agree with NA and NB). *)
   756 goal thy 
   757  "!!evs. [| Says B Server                                        \
   758 \            {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (shrK B)|}  \
   759 \           : set_of_list evs;       \
   760 \           Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
   761 \                       Crypt (Nonce NB) K|} : set_of_list evs;         \
   762 \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
   763 \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]   \
   764 \         ==> Says Server A                                       \
   765 \                     {|Crypt {|Agent B, Key K,                         \
   766 \                               Nonce NA, Nonce NB|} (shrK A),          \
   767 \                       Crypt {|Agent A, Key K|} (shrK B)|}             \
   768 \                   : set_of_list evs";
   769 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   770 by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
   771     dtac B_trusts_YM4_shrK 1);
   772 bd B_trusts_YM4_newK 3;
   773 by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   774 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   775 by (dresolve_tac [unique_session_keys] 1 THEN REPEAT (assume_tac 1));
   776 by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1);
   777 qed "B_trust_YM4";
   778 
   779 
   780