src/HOL/Auth/Yahalom.ML
author paulson
Thu Sep 25 12:13:18 1997 +0200 (1997-09-25)
changeset 3708 56facaebf3e3
parent 3683 aafe719dff14
child 3919 c036caebfc75
permissions -rw-r--r--
Changed some proofs to use Clarify_tac
     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 (ALLGOALS Clarify_tac);
   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 by (ALLGOALS Clarify_tac);
   305 (*YM3 & Fake*)
   306 by (Blast_tac 2);
   307 by (Fake_parts_insert_tac 1);
   308 (*YM4*)
   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 by (ALLGOALS Clarify_tac);
   519 (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
   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 (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   533 by (expand_case_tac "NB = NBa" 1);
   534 (*If NB=NBa then all other components of the Oops message agree*)
   535 by (blast_tac (!claset addDs [Says_unique_NB]) 1 THEN flexflex_tac);
   536 (*case NB ~= NBa*)
   537 by (asm_simp_tac (!simpset addsimps [single_Nonce_secrecy]) 1);
   538 by (blast_tac (!claset addSEs [MPair_parts]
   539 		       addDs  [Says_imp_spies RS parts.Inj, 
   540 			       no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   541 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
   542 
   543 
   544 (*B's session key guarantee from YM4.  The two certificates contribute to a
   545   single conclusion about the Server's message.  Note that the "Says A Spy"
   546   assumption must quantify over ALL POSSIBLE keys instead of our particular K.
   547   If this run is broken and the spy substitutes a certificate containing an
   548   old key, B has no means of telling.*)
   549 goal thy 
   550  "!!evs. [| Says B Server                                                   \
   551 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   552 \             : set evs;                                                    \
   553 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   554 \                       Crypt K (Nonce NB)|} : set evs;                     \
   555 \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs;         \
   556 \           A ~: bad;  B ~: bad;  evs : yahalom |]       \
   557 \         ==> Says Server A                                                 \
   558 \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
   559 \                               Nonce NA, Nonce NB|},                       \
   560 \                       Crypt (shrK B) {|Agent A, Key K|}|}                 \
   561 \               : set evs";
   562 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   563 by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1 THEN
   564     dtac B_trusts_YM4_shrK 1);
   565 by (dtac B_trusts_YM4_newK 3);
   566 by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   567 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   568 by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
   569 by (blast_tac (!claset addDs [Says_unique_NB]) 1);
   570 qed "B_trusts_YM4";
   571 
   572 
   573 
   574 (*** Authenticating B to A ***)
   575 
   576 (*The encryption in message YM2 tells us it cannot be faked.*)
   577 goal thy 
   578  "!!evs. evs : yahalom                                            \
   579 \  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs) --> \
   580 \      B ~: bad -->                                              \
   581 \      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   582 \         : set evs";
   583 by (parts_induct_tac 1);
   584 by (Fake_parts_insert_tac 1);
   585 bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
   586 
   587 (*If the server sends YM3 then B sent YM2*)
   588 goal thy 
   589  "!!evs. evs : yahalom                                                      \
   590 \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   591 \         : set evs -->                                                     \
   592 \      B ~: bad -->                                                        \
   593 \      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   594 \                 : set evs";
   595 by (etac yahalom.induct 1);
   596 by (ALLGOALS Asm_simp_tac);
   597 (*YM4*)
   598 by (Blast_tac 2);
   599 (*YM3*)
   600 by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
   601 		      addSEs [MPair_parts]) 1);
   602 val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   603 
   604 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   605 goal thy
   606  "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   607 \             : set evs;                                                    \
   608 \           A ~: bad;  B ~: bad;  evs : yahalom |]                        \
   609 \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
   610 \         : set evs";
   611 by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
   612 		       addEs spies_partsEs) 1);
   613 qed "YM3_auth_B_to_A";
   614 
   615 
   616 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
   617 
   618 (*Assuming the session key is secure, if both certificates are present then
   619   A has said NB.  We can't be sure about the rest of A's message, but only
   620   NB matters for freshness.*)  
   621 goal thy 
   622  "!!evs. evs : yahalom                                             \
   623 \        ==> Key K ~: analz (spies evs) -->                     \
   624 \            Crypt K (Nonce NB) : parts (spies evs) -->         \
   625 \            Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs) --> \
   626 \            B ~: bad -->                                         \
   627 \            (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   628 by (parts_induct_tac 1);
   629 (*Fake*)
   630 by (Fake_parts_insert_tac 1);
   631 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   632 by (fast_tac (!claset addSDs [Crypt_imp_invKey_keysFor] addss (!simpset)) 1); 
   633 (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   634 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   635 (*yes: apply unicity of session keys*)
   636 by (not_bad_tac "Aa" 1);
   637 by (blast_tac (!claset addSEs [MPair_parts]
   638                        addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   639 		       addDs  [Says_imp_spies RS parts.Inj,
   640 			       unique_session_keys]) 1);
   641 val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   642 
   643 (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   644   Moreover, A associates K with NB (thus is talking about the same run).
   645   Other premises guarantee secrecy of K.*)
   646 goal thy 
   647  "!!evs. [| Says B Server                                                   \
   648 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   649 \             : set evs;                                                    \
   650 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   651 \                       Crypt K (Nonce NB)|} : set evs;                     \
   652 \           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs);    \
   653 \           A ~: bad;  B ~: bad;  evs : yahalom |]       \
   654 \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   655 by (dtac B_trusts_YM4 1);
   656 by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
   657 by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
   658 by (rtac lemma 1);
   659 by (rtac Spy_not_see_encrypted_key 2);
   660 by (REPEAT_FIRST assume_tac);
   661 by (blast_tac (!claset addSEs [MPair_parts]
   662 	       	       addDs [Says_imp_spies RS parts.Inj]) 1);
   663 qed_spec_mp "YM4_imp_A_Said_YM3";