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