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