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