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