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