src/HOL/Auth/Yahalom.ML
author paulson
Thu Jun 19 11:28:55 1997 +0200 (1997-06-19)
changeset 3450 cd73bc206d87
parent 3444 919de2cb3487
child 3464 315694e22856
permissions -rw-r--r--
Proof tidying and variable renaming (NA->na, NB->nb when of type msg)
     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 "yahalom" 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 25;
    18 
    19 (*Replacing the variable by a constant improves speed*)
    20 val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy;
    21 
    22 
    23 (*A "possibility property": there are traces that reach the end*)
    24 goal thy 
    25  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    26 \        ==> EX X NB K. EX evs: yahalom lost.          \
    27 \               Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
    28 by (REPEAT (resolve_tac [exI,bexI] 1));
    29 by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
    30           yahalom.YM4) 2);
    31 by possibility_tac;
    32 result();
    33 
    34 
    35 (**** Inductive proofs about yahalom ****)
    36 
    37 (*Monotonicity*)
    38 goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost";
    39 by (rtac subsetI 1);
    40 by (etac yahalom.induct 1);
    41 by (REPEAT_FIRST
    42     (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono)
    43                               :: yahalom.intrs))));
    44 qed "yahalom_mono";
    45 
    46 
    47 (*Nobody sends themselves messages*)
    48 goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
    49 by (etac yahalom.induct 1);
    50 by (Auto_tac());
    51 qed_spec_mp "not_Says_to_self";
    52 Addsimps [not_Says_to_self];
    53 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    54 
    55 
    56 (** For reasoning about the encrypted portion of messages **)
    57 
    58 (*Lets us treat YM4 using a similar argument as for the Fake case.*)
    59 goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set_of_list evs ==> \
    60 \                X : analz (sees lost Spy evs)";
    61 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1);
    62 qed "YM4_analz_sees_Spy";
    63 
    64 bind_thm ("YM4_parts_sees_Spy",
    65           YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    66 
    67 (*Relates to both YM4 and Oops*)
    68 goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \
    69 \                  : set_of_list evs ==> \
    70 \                K : parts (sees lost Spy evs)";
    71 by (blast_tac (!claset addSEs partsEs
    72                       addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
    73 qed "YM4_Key_parts_sees_Spy";
    74 
    75 (*For proving the easier theorems about X ~: parts (sees lost Spy evs).
    76   We instantiate the variable to "lost" since leaving it as a Var would
    77   interfere with simplification.*)
    78 val parts_sees_tac = 
    79     forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6     THEN
    80     forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN
    81     prove_simple_subgoals_tac  1;
    82 
    83 val parts_induct_tac = 
    84     etac yahalom.induct 1 THEN parts_sees_tac;
    85 
    86 
    87 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    88     sends messages containing X! **)
    89 
    90 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    91 goal thy 
    92  "!!evs. evs : yahalom lost \
    93 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    94 by parts_induct_tac;
    95 by (Fake_parts_insert_tac 1);
    96 by (Blast_tac 1);
    97 qed "Spy_see_shrK";
    98 Addsimps [Spy_see_shrK];
    99 
   100 goal thy 
   101  "!!evs. evs : yahalom lost \
   102 \        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
   103 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   104 qed "Spy_analz_shrK";
   105 Addsimps [Spy_analz_shrK];
   106 
   107 goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
   108 \                  evs : yahalom lost |] ==> A:lost";
   109 by (blast_tac (!claset addDs [Spy_see_shrK]) 1);
   110 qed "Spy_see_shrK_D";
   111 
   112 bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
   113 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
   114 
   115 
   116 (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
   117 goal thy "!!evs. evs : yahalom lost ==>          \
   118 \         Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
   119 by parts_induct_tac;
   120 (*YM4: Key K is not fresh!*)
   121 by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   122 (*YM3*)
   123 by (Blast_tac 2);
   124 (*Fake*)
   125 by (best_tac
   126       (!claset addIs [impOfSubs analz_subset_parts]
   127                addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
   128                       impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   129                addss (!simpset)) 1);
   130 qed_spec_mp "new_keys_not_used";
   131 
   132 bind_thm ("new_keys_not_analzd",
   133           [analz_subset_parts RS keysFor_mono,
   134            new_keys_not_used] MRS contra_subsetD);
   135 
   136 Addsimps [new_keys_not_used, new_keys_not_analzd];
   137 
   138 
   139 (*Describes the form of K when the Server sends this message.  Useful for
   140   Oops as well as main secrecy property.*)
   141 goal thy 
   142  "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, NA, NB|}, X|} \
   143 \             : set_of_list evs;                                           \
   144 \           evs : yahalom lost |]                                          \
   145 \        ==> K ~: range shrK";
   146 by (etac rev_mp 1);
   147 by (etac yahalom.induct 1);
   148 by (ALLGOALS Asm_simp_tac);
   149 by (Blast_tac 1);
   150 qed "Says_Server_message_form";
   151 
   152 
   153 (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   154 val analz_sees_tac = 
   155     forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN
   156     forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   157     assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7);
   158 
   159 
   160 (****
   161  The following is to prove theorems of the form
   162 
   163   Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==>
   164   Key K : analz (sees lost Spy evs)
   165 
   166  A more general formula must be proved inductively.
   167 ****)
   168 
   169 (** Session keys are not used to encrypt other session keys **)
   170 
   171 goal thy  
   172  "!!evs. evs : yahalom lost ==> \
   173 \  ALL K KK. KK <= Compl (range shrK) -->                      \
   174 \            (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
   175 \            (K : KK | Key K : analz (sees lost Spy evs))";
   176 by (etac yahalom.induct 1);
   177 by analz_sees_tac;
   178 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   179 by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   180 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   181 (*Fake*) 
   182 by (spy_analz_tac 2);
   183 (*Base*)
   184 by (Blast_tac 1);
   185 qed_spec_mp "analz_image_freshK";
   186 
   187 goal thy
   188  "!!evs. [| evs : yahalom lost;  KAB ~: range shrK |] ==>             \
   189 \        Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
   190 \        (K = KAB | Key K : analz (sees lost Spy evs))";
   191 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
   192 qed "analz_insert_freshK";
   193 
   194 
   195 (*** The Key K uniquely identifies the Server's  message. **)
   196 
   197 goal thy 
   198  "!!evs. evs : yahalom lost ==>                                     \
   199 \      EX A' B' na' nb' X'. ALL A B na nb X.                             \
   200 \          Says Server A                                            \
   201 \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
   202 \          : set_of_list evs --> A=A' & B=B' & na=na' & nb=nb' & X=X'";
   203 by (etac yahalom.induct 1);
   204 by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   205 by (Step_tac 1);
   206 by (ex_strip_tac 2);
   207 by (Blast_tac 2);
   208 (*Remaining case: YM3*)
   209 by (expand_case_tac "K = ?y" 1);
   210 by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   211 (*...we assume X is a recent message and handle this case by contradiction*)
   212 by (blast_tac (!claset addSEs sees_Spy_partsEs
   213                       delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
   214 val lemma = result();
   215 
   216 goal thy 
   217 "!!evs. [| Says Server A                                            \
   218 \           {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}        \
   219 \           : set_of_list evs;                                      \
   220 \          Says Server A'                                           \
   221 \           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|}   \
   222 \           : set_of_list evs;                                      \
   223 \          evs : yahalom lost |]                                    \
   224 \       ==> A=A' & B=B' & na=na' & nb=nb'";
   225 by (prove_unique_tac lemma 1);
   226 qed "unique_session_keys";
   227 
   228 
   229 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   230 
   231 goal thy 
   232  "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   233 \        ==> Says Server A                                        \
   234 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   235 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   236 \             : set_of_list evs -->                               \
   237 \            Says A Spy {|na, nb, Key K|} ~: set_of_list evs -->  \
   238 \            Key K ~: analz (sees lost Spy evs)";
   239 by (etac yahalom.induct 1);
   240 by analz_sees_tac;
   241 by (ALLGOALS
   242     (asm_simp_tac 
   243      (!simpset addsimps [analz_insert_eq, not_parts_not_analz, 
   244 			 analz_insert_freshK]
   245                setloop split_tac [expand_if])));
   246 (*Oops*)
   247 by (blast_tac (!claset addDs [unique_session_keys]) 3);
   248 (*YM3*)
   249 by (blast_tac (!claset delrules [impCE]
   250                        addSEs sees_Spy_partsEs
   251                        addIs [impOfSubs analz_subset_parts]) 2);
   252 (*Fake*) 
   253 by (spy_analz_tac 1);
   254 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   255 
   256 
   257 (*Final version*)
   258 goal thy 
   259  "!!evs. [| Says Server A                                         \
   260 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   261 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   262 \             : set_of_list evs;                                  \
   263 \           Says A Spy {|na, nb, Key K|} ~: set_of_list evs;      \
   264 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   265 \        ==> Key K ~: analz (sees lost Spy evs)";
   266 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   267 by (blast_tac (!claset addSEs [lemma]) 1);
   268 qed "Spy_not_see_encrypted_key";
   269 
   270 
   271 (*And other agents don't see the key either.*)
   272 goal thy 
   273  "!!evs. [| C ~: {A,B,Server};                                    \
   274 \           Says Server A                                         \
   275 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   276 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   277 \             : set_of_list evs;                                  \
   278 \           Says A Spy {|na, nb, Key K|} ~: set_of_list evs;      \
   279 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]         \
   280 \        ==> Key K ~: analz (sees lost C evs)";
   281 by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   282 by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
   283 by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
   284 by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD])));
   285 qed "Agent_not_see_encrypted_key";
   286 
   287 
   288 (*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
   289   It simplifies the proof by discarding needless information about
   290 	analz (insert X (sees lost Spy evs)) 
   291 *)
   292 val analz_mono_parts_induct_tac = 
   293     etac yahalom.induct 1 
   294     THEN 
   295     REPEAT_FIRST  
   296       (rtac impI THEN' 
   297        dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
   298        mp_tac)  
   299     THEN  parts_sees_tac;
   300 
   301 
   302 (** Security Guarantee for A upon receiving YM3 **)
   303 
   304 (*If the encrypted message appears then it originated with the Server*)
   305 goal thy
   306  "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|}                  \
   307 \            : parts (sees lost Spy evs);                              \
   308 \           A ~: lost;  evs : yahalom lost |]                          \
   309 \         ==> Says Server A                                            \
   310 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},            \
   311 \                Crypt (shrK B) {|Agent A, Key K|}|}                   \
   312 \             : set_of_list evs";
   313 by (etac rev_mp 1);
   314 by parts_induct_tac;
   315 by (Fake_parts_insert_tac 1);
   316 qed "A_trusts_YM3";
   317 
   318 
   319 (** Security Guarantees for B upon receiving YM4 **)
   320 
   321 (*B knows, by the first part of A's message, that the Server distributed 
   322   the key for A and B.  But this part says nothing about nonces.*)
   323 goal thy 
   324  "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees lost Spy evs); \
   325 \           B ~: lost;  evs : yahalom lost |]                           \
   326 \        ==> EX NA NB. Says Server A                                    \
   327 \                        {|Crypt (shrK A) {|Agent B, Key K,             \
   328 \                                           Nonce NA, Nonce NB|},       \
   329 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   330 \                       : set_of_list evs";
   331 by (etac rev_mp 1);
   332 by parts_induct_tac;
   333 by (Fake_parts_insert_tac 1);
   334 (*YM3*)
   335 by (Blast_tac 1);
   336 qed "B_trusts_YM4_shrK";
   337 
   338 (*B knows, by the second part of A's message, that the Server distributed 
   339   the key quoting nonce NB.  This part says nothing about agent names. 
   340   Secrecy of NB is crucial.*)
   341 goal thy 
   342  "!!evs. evs : yahalom lost                                             \
   343 \        ==> Nonce NB ~: analz (sees lost Spy evs) -->                  \
   344 \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   345 \            (EX A B NA. Says Server A                                  \
   346 \                        {|Crypt (shrK A) {|Agent B, Key K,             \
   347 \                                  Nonce NA, Nonce NB|},                \
   348 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   349 \                       : set_of_list evs)";
   350 by analz_mono_parts_induct_tac;
   351 (*YM3 & Fake*)
   352 by (Blast_tac 2);
   353 by (Fake_parts_insert_tac 1);
   354 (*YM4*)
   355 by (Step_tac 1);
   356 (*A is uncompromised because NB is secure*)
   357 by (not_lost_tac "A" 1);
   358 (*A's certificate guarantees the existence of the Server message*)
   359 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS
   360 			      A_trusts_YM3]) 1);
   361 val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
   362 
   363 
   364 (**** Towards proving secrecy of Nonce NB ****)
   365 
   366 (** Lemmas about the predicate KeyWithNonce **)
   367 
   368 goalw thy [KeyWithNonce_def]
   369  "!!evs. Says Server A                                              \
   370 \            {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
   371 \          : set_of_list evs ==> KeyWithNonce K NB evs";
   372 by (Blast_tac 1);
   373 qed "KeyWithNonceI";
   374 
   375 goalw thy [KeyWithNonce_def]
   376    "KeyWithNonce K NB (Says S A X # evs) =                                    \
   377 \    (Server = S &                                                            \
   378 \     (EX B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|}) \
   379 \    | KeyWithNonce K NB evs)";
   380 by (Simp_tac 1);
   381 by (Blast_tac 1);
   382 qed "KeyWithNonce_Says";
   383 Addsimps [KeyWithNonce_Says];
   384 
   385 goalw thy [KeyWithNonce_def]
   386  "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
   387 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   388 qed "fresh_not_KeyWithNonce";
   389 
   390 (*The Server message associates K with NB' and therefore not with any 
   391   other nonce NB.*)
   392 goalw thy [KeyWithNonce_def]
   393  "!!evs. [| Says Server A                                                \
   394 \                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
   395 \             : set_of_list evs;                                         \
   396 \           NB ~= NB';  evs : yahalom lost |]                            \
   397 \        ==> ~ KeyWithNonce K NB evs";
   398 by (blast_tac (!claset addDs [unique_session_keys]) 1);
   399 qed "Says_Server_KeyWithNonce";
   400 
   401 
   402 (*The only nonces that can be found with the help of session keys are
   403   those distributed as nonce NB by the Server.  The form of the theorem
   404   recalls analz_image_freshK, but it is much more complicated.*)
   405 
   406 
   407 (*As with analz_image_freshK, we take some pains to express the property
   408   as a logical equivalence so that the simplifier can apply it.*)
   409 goal thy  
   410  "!!evs. P --> (X : analz (G Un H)) --> (X : analz H)  ==> \
   411 \        P --> (X : analz (G Un H)) = (X : analz H)";
   412 by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
   413 val lemma = result();
   414 
   415 goal thy 
   416  "!!evs. evs : yahalom lost ==>                                         \
   417 \        (ALL KK. KK <= Compl (range shrK) -->                          \
   418 \             (ALL K: KK. ~ KeyWithNonce K NB evs)   -->                \
   419 \             (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) =     \
   420 \             (Nonce NB : analz (sees lost Spy evs)))";
   421 by (etac yahalom.induct 1);
   422 by analz_sees_tac;
   423 by (REPEAT_FIRST (resolve_tac [impI RS allI]));
   424 by (REPEAT_FIRST (rtac lemma));
   425 (*For Oops, simplification proves NBa~=NB.  By Says_Server_KeyWithNonce,
   426   we get (~ KeyWithNonce K NB evsa); then simplification can apply the
   427   induction hypothesis with KK = {K}.*)
   428 by (ALLGOALS  (*22 seconds*)
   429     (asm_simp_tac 
   430      (analz_image_freshK_ss addsimps
   431         ([all_conj_distrib, not_parts_not_analz, analz_image_freshK,
   432 	  KeyWithNonce_Says, fresh_not_KeyWithNonce, 
   433 	  imp_disj_not1,  (*Moves NBa~=NB to the front*)
   434 	  Says_Server_KeyWithNonce] 
   435 	 @ pushes))));
   436 (*Base*)
   437 by (Blast_tac 1);
   438 (*Fake*) 
   439 by (spy_analz_tac 1);
   440 (*YM4*)  (** LEVEL 7 **)
   441 by (not_lost_tac "A" 1);
   442 by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   443     THEN REPEAT (assume_tac 1));
   444 by (blast_tac (!claset addIs [KeyWithNonceI]) 1);
   445 qed_spec_mp "Nonce_secrecy";
   446 
   447 
   448 (*Version required below: if NB can be decrypted using a session key then it
   449   was distributed with that key.  The more general form above is required
   450   for the induction to carry through.*)
   451 goal thy 
   452  "!!evs. [| Says Server A                                                 \
   453 \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}    \
   454 \           : set_of_list evs;                                            \
   455 \           NB ~= NB';  KAB ~: range shrK;  evs : yahalom lost |]         \
   456 \        ==> (Nonce NB : analz (insert (Key KAB) (sees lost Spy evs))) =  \
   457 \            (Nonce NB : analz (sees lost Spy evs))";
   458 by (asm_simp_tac (analz_image_freshK_ss addsimps 
   459 		  [Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
   460 qed "single_Nonce_secrecy";
   461 
   462 
   463 (*** The Nonce NB uniquely identifies B's message. ***)
   464 
   465 goal thy 
   466  "!!evs. evs : yahalom lost ==>                                            \
   467 \   EX NA' A' B'. ALL NA A B.                                              \
   468 \      Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \
   469 \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
   470 by parts_induct_tac;
   471 (*Fake*)
   472 by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
   473     THEN Fake_parts_insert_tac 1);
   474 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   475 (*YM2: creation of new Nonce.  Move assertion into global context*)
   476 by (expand_case_tac "NB = ?y" 1);
   477 by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
   478 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   479 val lemma = result();
   480 
   481 goal thy 
   482  "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, NB|}        \
   483 \                  : parts (sees lost Spy evs);            \
   484 \          Crypt (shrK B') {|Agent A', Nonce NA', NB|}     \
   485 \                  : parts (sees lost Spy evs);            \
   486 \          evs : yahalom lost;  B ~: lost;  B' ~: lost |]  \
   487 \        ==> NA' = NA & A' = A & B' = B";
   488 by (prove_unique_tac lemma 1);
   489 qed "unique_NB";
   490 
   491 
   492 (*Variant useful for proving secrecy of NB: the Says... form allows 
   493   not_lost_tac to remove the assumption B' ~: lost.*)
   494 goal thy 
   495  "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, NB|}|}    \
   496 \            : set_of_list evs;  B ~: lost;                               \
   497 \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', NB|}|} \
   498 \            : set_of_list evs;                                           \
   499 \          NB ~: analz (sees lost Spy evs);  evs : yahalom lost |]        \
   500 \        ==> NA' = NA & A' = A & B' = B";
   501 by (not_lost_tac "B'" 1);
   502 by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   503                        addSEs [MPair_parts]
   504                        addDs  [unique_NB]) 1);
   505 qed "Says_unique_NB";
   506 
   507 val Says_unique_NB' = read_instantiate [("lost","lost")] Says_unique_NB;
   508 
   509 
   510 (** A nonce value is never used both as NA and as NB **)
   511 
   512 goal thy 
   513  "!!evs. [| B ~: lost;  evs : yahalom lost  |]               \
   514 \ ==> Nonce NB ~: analz (sees lost Spy evs) -->              \
   515 \     Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}: parts(sees lost Spy evs)\
   516 \ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts(sees lost Spy evs)";
   517 by analz_mono_parts_induct_tac;
   518 by (Fake_parts_insert_tac 1);
   519 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]
   520                        addSIs [parts_insertI]
   521                        addSEs partsEs) 1);
   522 bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2, rev_mp) RS notE);
   523 
   524 (*YM3 can only be triggered by YM2*)
   525 goal thy 
   526  "!!evs. [| Says Server A                                           \
   527 \            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \
   528 \           evs : yahalom lost |]                                        \
   529 \        ==> EX B'. Says B' Server                                       \
   530 \                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
   531 \                   : set_of_list evs";
   532 by (etac rev_mp 1);
   533 by (etac yahalom.induct 1);
   534 by (ALLGOALS Asm_simp_tac);
   535 by (ALLGOALS Blast_tac);
   536 qed "Says_Server_imp_YM2";
   537 
   538 
   539 (*Basic theorem for B: Nonce NB remains secure from the Spy.
   540   Unusually, the Fake case requires Spy:lost.*)
   541 goal thy 
   542  "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
   543 \ ==> Says B Server                                                    \
   544 \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   545 \     : set_of_list evs -->                               \
   546 \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) -->  \
   547 \     Nonce NB ~: analz (sees lost Spy evs)";
   548 by (etac yahalom.induct 1);
   549 by analz_sees_tac;
   550 by (ALLGOALS
   551     (asm_simp_tac 
   552      (!simpset addsimps ([analz_insert_eq, not_parts_not_analz,
   553                           analz_insert_freshK] @ pushes)
   554                setloop split_tac [expand_if])));
   555 (*Prove YM3 by showing that no NB can also be an NA*)
   556 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj]
   557 	               addSEs [MPair_parts]
   558 		       addDs  [no_nonce_YM1_YM2, Says_unique_NB']) 4
   559     THEN flexflex_tac);
   560 (*YM2: similar freshness reasoning*) 
   561 by (blast_tac (!claset addSEs partsEs
   562 		       addDs  [Says_imp_sees_Spy' RS analz.Inj,
   563 			       impOfSubs analz_subset_parts]) 3);
   564 (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
   565 by (blast_tac (!claset addSIs [parts_insertI]
   566                        addSEs sees_Spy_partsEs) 2);
   567 (*Fake*)
   568 by (spy_analz_tac 1);
   569 (** LEVEL 7: YM4 and Oops remain **)
   570 (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
   571 by (REPEAT (Safe_step_tac 1));
   572 by (not_lost_tac "Aa" 1);
   573 by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
   574 by (forward_tac [Says_Server_message_form] 3);
   575 by (forward_tac [Says_Server_imp_YM2] 4);
   576 by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
   577 (*  use Says_unique_NB' to identify message components: Aa=A, Ba=B, NAa=NA *)
   578 by (blast_tac (!claset addDs [Says_unique_NB', Spy_not_see_encrypted_key,
   579 			      impOfSubs Fake_analz_insert]) 1);
   580 (** LEVEL 14 **)
   581 (*Oops case: if the nonce is betrayed now, show that the Oops event is 
   582   covered by the quantified Oops assumption.*)
   583 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   584 by (step_tac (!claset delrules [disjE, conjI]) 1);
   585 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   586 by (expand_case_tac "NB = NBa" 1);
   587 (*If NB=NBa then all other components of the Oops message agree*)
   588 by (blast_tac (!claset addDs [Says_unique_NB']) 1 THEN flexflex_tac);
   589 (*case NB ~= NBa*)
   590 by (asm_simp_tac (!simpset addsimps [single_Nonce_secrecy]) 1);
   591 by (blast_tac (!claset addSEs [MPair_parts]
   592 		       addDs  [Says_imp_sees_Spy' RS parts.Inj, 
   593 			       no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   594 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
   595 
   596 
   597 (*What can B deduce from receipt of YM4?  Note how the two components of
   598   the message contribute to a single conclusion about the Server's message.
   599   Note that the "Says A Spy" assumption must quantify over 
   600   ALL POSSIBLE keys instead of our particular K.  If this run is broken and
   601   the spy has a certificate for an old key, B has no means of telling.*)
   602 goal thy 
   603  "!!evs. [| Says B Server                                                   \
   604 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   605 \             : set_of_list evs;                                            \
   606 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   607 \                       Crypt K (Nonce NB)|} : set_of_list evs;             \
   608 \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs; \
   609 \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
   610 \         ==> Says Server A                                                 \
   611 \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
   612 \                               Nonce NA, Nonce NB|},                       \
   613 \                       Crypt (shrK B) {|Agent A, Key K|}|}                 \
   614 \               : set_of_list evs";
   615 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   616 by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1 THEN
   617     dtac B_trusts_YM4_shrK 1);
   618 by (dtac B_trusts_YM4_newK 3);
   619 by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   620 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   621 by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
   622 by (blast_tac (!claset addDs [Says_unique_NB']) 1);
   623 qed "B_trusts_YM4";
   624 
   625 
   626 
   627 (*** Authenticating B to A ***)
   628 
   629 (*The encryption in message YM2 tells us it cannot be faked.*)
   630 goal thy 
   631  "!!evs. evs : yahalom lost                                            \
   632 \  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|}                        \
   633 \        : parts (sees lost Spy evs) -->                               \
   634 \      B ~: lost -->                                                   \
   635 \      Says B Server {|Agent B,                                \
   636 \                          Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   637 \         : set_of_list evs";
   638 by parts_induct_tac;
   639 by (Fake_parts_insert_tac 1);
   640 bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
   641 
   642 (*If the server sends YM3 then B sent YM2*)
   643 goal thy 
   644  "!!evs. evs : yahalom lost                                       \
   645 \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   646 \         : set_of_list evs -->                                          \
   647 \      B ~: lost -->                                                     \
   648 \      Says B Server {|Agent B,                            \
   649 \                               Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}   \
   650 \                 : set_of_list evs";
   651 by (etac yahalom.induct 1);
   652 by (ALLGOALS Asm_simp_tac);
   653 (*YM4*)
   654 by (Blast_tac 2);
   655 (*YM3*)
   656 by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_sees_Spy' RS parts.Inj]
   657 		      addSEs [MPair_parts]) 1);
   658 val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   659 
   660 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   661 goal thy
   662  "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   663 \             : set_of_list evs;                                            \
   664 \           A ~: lost;  B ~: lost;  evs : yahalom lost |]                   \
   665 \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
   666 \         : set_of_list evs";
   667 by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
   668 		       addEs sees_Spy_partsEs) 1);
   669 qed "YM3_auth_B_to_A";
   670 
   671 
   672 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
   673 
   674 (*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
   675   It simplifies the proof by discarding needless information about
   676 	analz (insert X (sees lost Spy evs)) 
   677 *)
   678 val analz_mono_parts_induct_tac = 
   679     etac yahalom.induct 1 
   680     THEN 
   681     REPEAT_FIRST  
   682       (rtac impI THEN' 
   683        dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN'
   684        mp_tac)  
   685     THEN  parts_sees_tac;
   686 
   687 (*Assuming the session key is secure, if both certificates are present then
   688   A has said NB.  We can't be sure about the rest of A's message, but only
   689   NB matters for freshness.*)  
   690 goal thy 
   691  "!!evs. evs : yahalom lost                                             \
   692 \        ==> Key K ~: analz (sees lost Spy evs) -->                     \
   693 \            Crypt K (Nonce NB) : parts (sees lost Spy evs) -->         \
   694 \            Crypt (shrK B) {|Agent A, Key K|}                          \
   695 \              : parts (sees lost Spy evs) -->                          \
   696 \            B ~: lost -->                                              \
   697 \             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs)";
   698 by analz_mono_parts_induct_tac;
   699 (*Fake*)
   700 by (Fake_parts_insert_tac 1);
   701 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   702 by (fast_tac (!claset addSDs [Crypt_imp_invKey_keysFor] addss (!simpset)) 1); 
   703 (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   704 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   705 (*yes: apply unicity of session keys*)
   706 by (not_lost_tac "Aa" 1);
   707 by (blast_tac (!claset addSEs [MPair_parts]
   708                        addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   709 		       addDs  [Says_imp_sees_Spy' RS parts.Inj,
   710 			       unique_session_keys]) 1);
   711 val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   712 
   713 (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   714   Moreover, A associates K with NB (thus is talking about the same run).
   715   Other premises guarantee secrecy of K.*)
   716 goal thy 
   717  "!!evs. [| Says B Server                                                   \
   718 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   719 \             : set_of_list evs;                                            \
   720 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},       \
   721 \                       Crypt K (Nonce NB)|} : set_of_list evs;  \
   722 \           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|}    \
   723 \               ~: set_of_list evs);                             \
   724 \           A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]       \
   725 \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set_of_list evs";
   726 by (dtac B_trusts_YM4 1);
   727 by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
   728 by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1);
   729 by (rtac lemma 1);
   730 by (rtac Spy_not_see_encrypted_key 2);
   731 by (REPEAT_FIRST assume_tac);
   732 by (blast_tac (!claset addSEs [MPair_parts]
   733 	       	       addDs [Says_imp_sees_Spy' RS parts.Inj]) 1);
   734 qed_spec_mp "YM4_imp_A_Said_YM3";