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