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