src/HOL/Auth/Yahalom.ML
author paulson
Tue Sep 16 13:58:02 1997 +0200 (1997-09-16)
changeset 3674 65ec38fbb265
parent 3543 82f33248d89d
child 3679 8df171ccdbd8
permissions -rw-r--r--
Deleted the redundant simprule not_parts_not_analz
     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 (sees Spy evs)";
    48 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    49 qed "YM4_analz_sees_Spy";
    50 
    51 bind_thm ("YM4_parts_sees_Spy",
    52           YM4_analz_sees_Spy 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 (sees Spy evs)";
    57 by (blast_tac (!claset addSEs partsEs
    58                       addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    59 qed "YM4_Key_parts_sees_Spy";
    60 
    61 (*For proving the easier theorems about X ~: parts (sees Spy evs).*)
    62 fun parts_sees_tac i = 
    63     forward_tac [YM4_Key_parts_sees_Spy] (i+6) THEN
    64     forward_tac [YM4_parts_sees_Spy] (i+5)     THEN
    65     prove_simple_subgoals_tac  i;
    66 
    67 (*Induction for regularity theorems.  If induction formula has the form
    68    X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
    69    needless information about analz (insert X (sees Spy evs))  *)
    70 fun parts_induct_tac i = 
    71     etac yahalom.induct i
    72     THEN 
    73     REPEAT (FIRSTGOAL analz_mono_contra_tac)
    74     THEN  parts_sees_tac i;
    75 
    76 
    77 (** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
    78     sends messages containing X! **)
    79 
    80 (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    81 goal thy 
    82  "!!evs. evs : yahalom ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)";
    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 (sees Spy evs)) = (A : lost)";
    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 (sees Spy evs);       \
    96 \                  evs : yahalom |] ==> A:lost";
    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 (sees Spy evs))";
   107 by (parts_induct_tac 1);
   108 (*YM4: Key K is not fresh!*)
   109 by (blast_tac (!claset addSEs sees_Spy_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_sees_tac = 
   143     forward_tac [YM4_analz_sees_Spy] 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) (sees Spy evs)) ==>
   152   Key K : analz (sees Spy 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 (sees Spy evs))) = \
   163 \            (K : KK | Key K : analz (sees Spy evs))";
   164 by (etac yahalom.induct 1);
   165 by analz_sees_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) (sees Spy evs)) =       \
   178 \        (K = KAB | Key K : analz (sees Spy 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 sees_Spy_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|}        \
   207 \           : set evs;                                              \
   208 \          Says Server A'                                           \
   209 \           {|Crypt (shrK A') {|Agent B', Key K, na', nb'|}, X'|}   \
   210 \           : set evs;                                              \
   211 \          evs : yahalom |]                                    \
   212 \       ==> A=A' & B=B' & na=na' & nb=nb'";
   213 by (prove_unique_tac lemma 1);
   214 qed "unique_session_keys";
   215 
   216 
   217 (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
   218 
   219 goal thy 
   220  "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom |]         \
   221 \        ==> Says Server A                                        \
   222 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   223 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   224 \             : set evs -->                                       \
   225 \            Says A Spy {|na, nb, Key K|} ~: set evs -->          \
   226 \            Key K ~: analz (sees Spy evs)";
   227 by (etac yahalom.induct 1);
   228 by analz_sees_tac;
   229 by (ALLGOALS
   230     (asm_simp_tac 
   231      (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
   232                setloop split_tac [expand_if])));
   233 (*Oops*)
   234 by (blast_tac (!claset addDs [unique_session_keys]) 3);
   235 (*YM3*)
   236 by (blast_tac (!claset delrules [impCE]
   237                        addSEs sees_Spy_partsEs
   238                        addIs [impOfSubs analz_subset_parts]) 2);
   239 (*Fake*) 
   240 by (spy_analz_tac 1);
   241 val lemma = result() RS mp RS mp RSN(2,rev_notE);
   242 
   243 
   244 (*Final version*)
   245 goal thy 
   246  "!!evs. [| Says Server A                                         \
   247 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
   248 \                Crypt (shrK B) {|Agent A, Key K|}|}              \
   249 \             : set evs;                                          \
   250 \           Says A Spy {|na, nb, Key K|} ~: set evs;              \
   251 \           A ~: lost;  B ~: lost;  evs : yahalom |]         \
   252 \        ==> Key K ~: analz (sees Spy evs)";
   253 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   254 by (blast_tac (!claset addSEs [lemma]) 1);
   255 qed "Spy_not_see_encrypted_key";
   256 
   257 
   258 (** Security Guarantee for A upon receiving YM3 **)
   259 
   260 (*If the encrypted message appears then it originated with the Server*)
   261 goal thy
   262  "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|}                  \
   263 \            : parts (sees Spy evs);                              \
   264 \           A ~: lost;  evs : yahalom |]                          \
   265 \         ==> Says Server A                                            \
   266 \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},            \
   267 \                Crypt (shrK B) {|Agent A, Key K|}|}                   \
   268 \             : set evs";
   269 by (etac rev_mp 1);
   270 by (parts_induct_tac 1);
   271 by (Fake_parts_insert_tac 1);
   272 qed "A_trusts_YM3";
   273 
   274 
   275 (** Security Guarantees for B upon receiving YM4 **)
   276 
   277 (*B knows, by the first part of A's message, that the Server distributed 
   278   the key for A and B.  But this part says nothing about nonces.*)
   279 goal thy 
   280  "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (sees Spy evs);   \
   281 \           B ~: lost;  evs : yahalom |]                                \
   282 \        ==> EX NA NB. Says Server A                                    \
   283 \                        {|Crypt (shrK A) {|Agent B, Key K,             \
   284 \                                           Nonce NA, Nonce NB|},       \
   285 \                          Crypt (shrK B) {|Agent A, Key K|}|}          \
   286 \                       : set evs";
   287 by (etac rev_mp 1);
   288 by (parts_induct_tac 1);
   289 by (Fake_parts_insert_tac 1);
   290 (*YM3*)
   291 by (Blast_tac 1);
   292 qed "B_trusts_YM4_shrK";
   293 
   294 (*B knows, by the second part of A's message, that the Server distributed 
   295   the key quoting nonce NB.  This part says nothing about agent names. 
   296   Secrecy of NB is crucial.*)
   297 goal thy 
   298  "!!evs. evs : yahalom                                             \
   299 \        ==> Nonce NB ~: analz (sees Spy evs) -->                  \
   300 \            Crypt K (Nonce NB) : parts (sees Spy evs) -->         \
   301 \            (EX A B NA. Says Server A                             \
   302 \                        {|Crypt (shrK A) {|Agent B, Key K,        \
   303 \                                  Nonce NA, Nonce NB|},           \
   304 \                          Crypt (shrK B) {|Agent A, Key K|}|}     \
   305 \                       : set evs)";
   306 by (parts_induct_tac 1);
   307 (*YM3 & Fake*)
   308 by (Blast_tac 2);
   309 by (Fake_parts_insert_tac 1);
   310 (*YM4*)
   311 by (Step_tac 1);
   312 (*A is uncompromised because NB is secure*)
   313 by (not_lost_tac "A" 1);
   314 (*A's certificate guarantees the existence of the Server message*)
   315 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS
   316 			      A_trusts_YM3]) 1);
   317 bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
   318 
   319 
   320 (**** Towards proving secrecy of Nonce NB ****)
   321 
   322 (** Lemmas about the predicate KeyWithNonce **)
   323 
   324 goalw thy [KeyWithNonce_def]
   325  "!!evs. Says Server A                                              \
   326 \            {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
   327 \          : set evs ==> KeyWithNonce K NB evs";
   328 by (Blast_tac 1);
   329 qed "KeyWithNonceI";
   330 
   331 goalw thy [KeyWithNonce_def]
   332    "KeyWithNonce K NB (Says S A X # evs) =                                    \
   333 \    (Server = S &                                                            \
   334 \     (EX B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|}) \
   335 \    | KeyWithNonce K NB evs)";
   336 by (Simp_tac 1);
   337 by (Blast_tac 1);
   338 qed "KeyWithNonce_Says";
   339 Addsimps [KeyWithNonce_Says];
   340 
   341 (*A fresh key cannot be associated with any nonce 
   342   (with respect to a given trace). *)
   343 goalw thy [KeyWithNonce_def]
   344  "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
   345 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   346 qed "fresh_not_KeyWithNonce";
   347 
   348 (*The Server message associates K with NB' and therefore not with any 
   349   other nonce NB.*)
   350 goalw thy [KeyWithNonce_def]
   351  "!!evs. [| Says Server A                                                \
   352 \                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
   353 \             : set evs;                                                 \
   354 \           NB ~= NB';  evs : yahalom |]                            \
   355 \        ==> ~ KeyWithNonce K NB evs";
   356 by (blast_tac (!claset addDs [unique_session_keys]) 1);
   357 qed "Says_Server_KeyWithNonce";
   358 
   359 
   360 (*The only nonces that can be found with the help of session keys are
   361   those distributed as nonce NB by the Server.  The form of the theorem
   362   recalls analz_image_freshK, but it is much more complicated.*)
   363 
   364 
   365 (*As with analz_image_freshK, we take some pains to express the property
   366   as a logical equivalence so that the simplifier can apply it.*)
   367 goal thy  
   368  "!!evs. P --> (X : analz (G Un H)) --> (X : analz H)  ==> \
   369 \        P --> (X : analz (G Un H)) = (X : analz H)";
   370 by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
   371 val lemma = result();
   372 
   373 goal thy 
   374  "!!evs. evs : yahalom ==>                                         \
   375 \        (ALL KK. KK <= Compl (range shrK) -->                          \
   376 \             (ALL K: KK. ~ KeyWithNonce K NB evs)   -->                \
   377 \             (Nonce NB : analz (Key``KK Un (sees Spy evs))) =     \
   378 \             (Nonce NB : analz (sees Spy evs)))";
   379 by (etac yahalom.induct 1);
   380 by analz_sees_tac;
   381 by (REPEAT_FIRST (resolve_tac [impI RS allI]));
   382 by (REPEAT_FIRST (rtac lemma));
   383 (*For Oops, simplification proves NBa~=NB.  By Says_Server_KeyWithNonce,
   384   we get (~ KeyWithNonce K NB evsa); then simplification can apply the
   385   induction hypothesis with KK = {K}.*)
   386 by (ALLGOALS  (*22 seconds*)
   387     (asm_simp_tac 
   388      (analz_image_freshK_ss addsimps
   389         ([all_conj_distrib, analz_image_freshK,
   390 	  KeyWithNonce_Says, fresh_not_KeyWithNonce, 
   391 	  imp_disj_not1,  (*Moves NBa~=NB to the front*)
   392 	  Says_Server_KeyWithNonce] 
   393 	 @ pushes))));
   394 (*Base*)
   395 by (Blast_tac 1);
   396 (*Fake*) 
   397 by (spy_analz_tac 1);
   398 (*YM4*)  (** LEVEL 7 **)
   399 by (not_lost_tac "A" 1);
   400 by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   401     THEN REPEAT (assume_tac 1));
   402 by (blast_tac (!claset addIs [KeyWithNonceI]) 1);
   403 qed_spec_mp "Nonce_secrecy";
   404 
   405 
   406 (*Version required below: if NB can be decrypted using a session key then it
   407   was distributed with that key.  The more general form above is required
   408   for the induction to carry through.*)
   409 goal thy 
   410  "!!evs. [| Says Server A                                                 \
   411 \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}    \
   412 \           : set evs;                                                    \
   413 \           NB ~= NB';  KAB ~: range shrK;  evs : yahalom |]         \
   414 \        ==> (Nonce NB : analz (insert (Key KAB) (sees Spy evs))) =  \
   415 \            (Nonce NB : analz (sees Spy evs))";
   416 by (asm_simp_tac (analz_image_freshK_ss addsimps 
   417 		  [Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
   418 qed "single_Nonce_secrecy";
   419 
   420 
   421 (*** The Nonce NB uniquely identifies B's message. ***)
   422 
   423 goal thy 
   424  "!!evs. evs : yahalom ==>                                            \
   425 \   EX NA' A' B'. ALL NA A B.                                              \
   426 \      Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(sees Spy evs) \
   427 \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
   428 by (parts_induct_tac 1);
   429 (*Fake*)
   430 by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
   431     THEN Fake_parts_insert_tac 1);
   432 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   433 (*YM2: creation of new Nonce.  Move assertion into global context*)
   434 by (expand_case_tac "nb = ?y" 1);
   435 by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
   436 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   437 val lemma = result();
   438 
   439 goal thy 
   440  "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|}        \
   441 \                  : parts (sees Spy evs);            \
   442 \          Crypt (shrK B') {|Agent A', Nonce NA', nb|}     \
   443 \                  : parts (sees Spy evs);            \
   444 \          evs : yahalom;  B ~: lost;  B' ~: lost |]  \
   445 \        ==> NA' = NA & A' = A & B' = B";
   446 by (prove_unique_tac lemma 1);
   447 qed "unique_NB";
   448 
   449 
   450 (*Variant useful for proving secrecy of NB: the Says... form allows 
   451   not_lost_tac to remove the assumption B' ~: lost.*)
   452 goal thy 
   453  "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}    \
   454 \            : set evs;          B ~: lost;                               \
   455 \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
   456 \            : set evs;                                                   \
   457 \          nb ~: analz (sees Spy evs);  evs : yahalom |]        \
   458 \        ==> NA' = NA & A' = A & B' = B";
   459 by (not_lost_tac "B'" 1);
   460 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   461                        addSEs [MPair_parts]
   462                        addDs  [unique_NB]) 1);
   463 qed "Says_unique_NB";
   464 
   465 
   466 (** A nonce value is never used both as NA and as NB **)
   467 
   468 goal thy 
   469  "!!evs. [| B ~: lost;  evs : yahalom  |]            \
   470 \ ==> Nonce NB ~: analz (sees Spy evs) -->           \
   471 \     Crypt (shrK B') {|Agent A', Nonce NB, nb'|}    \
   472 \       : parts(sees Spy evs)                        \
   473 \ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
   474 \       ~: parts(sees Spy evs)";
   475 by (parts_induct_tac 1);
   476 by (Fake_parts_insert_tac 1);
   477 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
   478                        addSIs [parts_insertI]
   479                        addSEs partsEs) 1);
   480 bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
   481 
   482 (*The Server sends YM3 only in response to YM2.*)
   483 goal thy 
   484  "!!evs. [| Says Server A                                                \
   485 \            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs;     \
   486 \           evs : yahalom |]                                             \
   487 \        ==> EX B'. Says B' Server                                       \
   488 \                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
   489 \                   : set evs";
   490 by (etac rev_mp 1);
   491 by (etac yahalom.induct 1);
   492 by (ALLGOALS Asm_simp_tac);
   493 by (ALLGOALS Blast_tac);
   494 qed "Says_Server_imp_YM2";
   495 
   496 
   497 (*A vital theorem for B, that nonce NB remains secure from the Spy.*)
   498 goal thy 
   499  "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom |]  \
   500 \ ==> Says B Server                                                    \
   501 \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   502 \     : set evs -->                                                    \
   503 \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->     \
   504 \     Nonce NB ~: analz (sees Spy evs)";
   505 by (etac yahalom.induct 1);
   506 by analz_sees_tac;
   507 by (ALLGOALS
   508     (asm_simp_tac 
   509      (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes)
   510                setloop split_tac [expand_if])));
   511 (*Prove YM3 by showing that no NB can also be an NA*)
   512 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
   513 	               addSEs [MPair_parts]
   514 		       addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
   515     THEN flexflex_tac);
   516 (*YM2: similar freshness reasoning*) 
   517 by (blast_tac (!claset addSEs partsEs
   518 		       addDs  [Says_imp_sees_Spy RS analz.Inj,
   519 			       impOfSubs analz_subset_parts]) 3);
   520 (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
   521 by (blast_tac (!claset addSIs [parts_insertI]
   522                        addSEs sees_Spy_partsEs) 2);
   523 (*Fake*)
   524 by (spy_analz_tac 1);
   525 (** LEVEL 7: YM4 and Oops remain **)
   526 (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
   527 by (REPEAT (Safe_step_tac 1));
   528 by (not_lost_tac "Aa" 1);
   529 by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
   530 by (forward_tac [Says_Server_message_form] 3);
   531 by (forward_tac [Says_Server_imp_YM2] 4);
   532 by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
   533 (*  use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *)
   534 by (blast_tac (!claset addDs [Says_unique_NB, Spy_not_see_encrypted_key,
   535 			      impOfSubs Fake_analz_insert]) 1);
   536 (** LEVEL 14 **)
   537 (*Oops case: if the nonce is betrayed now, show that the Oops event is 
   538   covered by the quantified Oops assumption.*)
   539 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   540 by (step_tac (!claset delrules [disjE, conjI]) 1);
   541 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   542 by (expand_case_tac "NB = NBa" 1);
   543 (*If NB=NBa then all other components of the Oops message agree*)
   544 by (blast_tac (!claset addDs [Says_unique_NB]) 1 THEN flexflex_tac);
   545 (*case NB ~= NBa*)
   546 by (asm_simp_tac (!simpset addsimps [single_Nonce_secrecy]) 1);
   547 by (blast_tac (!claset addSEs [MPair_parts]
   548 		       addDs  [Says_imp_sees_Spy RS parts.Inj, 
   549 			       no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   550 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
   551 
   552 
   553 (*B's session key guarantee from YM4.  The two certificates contribute to a
   554   single conclusion about the Server's message.  Note that the "Says A Spy"
   555   assumption must quantify over ALL POSSIBLE keys instead of our particular K.
   556   If this run is broken and the spy substitutes a certificate containing an
   557   old key, B has no means of telling.*)
   558 goal thy 
   559  "!!evs. [| Says B Server                                                   \
   560 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   561 \             : set evs;                                                    \
   562 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   563 \                       Crypt K (Nonce NB)|} : set evs;                     \
   564 \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs;         \
   565 \           A ~: lost;  B ~: lost;  evs : yahalom |]       \
   566 \         ==> Says Server A                                                 \
   567 \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
   568 \                               Nonce NA, Nonce NB|},                       \
   569 \                       Crypt (shrK B) {|Agent A, Key K|}|}                 \
   570 \               : set evs";
   571 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   572 by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
   573     dtac B_trusts_YM4_shrK 1);
   574 by (dtac B_trusts_YM4_newK 3);
   575 by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   576 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   577 by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
   578 by (blast_tac (!claset addDs [Says_unique_NB]) 1);
   579 qed "B_trusts_YM4";
   580 
   581 
   582 
   583 (*** Authenticating B to A ***)
   584 
   585 (*The encryption in message YM2 tells us it cannot be faked.*)
   586 goal thy 
   587  "!!evs. evs : yahalom                                            \
   588 \  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|}                   \
   589 \        : parts (sees Spy evs) -->                               \
   590 \      B ~: lost -->                                              \
   591 \      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   592 \         : set evs";
   593 by (parts_induct_tac 1);
   594 by (Fake_parts_insert_tac 1);
   595 bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
   596 
   597 (*If the server sends YM3 then B sent YM2*)
   598 goal thy 
   599  "!!evs. evs : yahalom                                                      \
   600 \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   601 \         : set evs -->                                                     \
   602 \      B ~: lost -->                                                        \
   603 \      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   604 \                 : set evs";
   605 by (etac yahalom.induct 1);
   606 by (ALLGOALS Asm_simp_tac);
   607 (*YM4*)
   608 by (Blast_tac 2);
   609 (*YM3*)
   610 by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_sees_Spy RS parts.Inj]
   611 		      addSEs [MPair_parts]) 1);
   612 val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   613 
   614 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   615 goal thy
   616  "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   617 \             : set evs;                                                    \
   618 \           A ~: lost;  B ~: lost;  evs : yahalom |]                        \
   619 \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
   620 \         : set evs";
   621 by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
   622 		       addEs sees_Spy_partsEs) 1);
   623 qed "YM3_auth_B_to_A";
   624 
   625 
   626 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
   627 
   628 (*Assuming the session key is secure, if both certificates are present then
   629   A has said NB.  We can't be sure about the rest of A's message, but only
   630   NB matters for freshness.*)  
   631 goal thy 
   632  "!!evs. evs : yahalom                                             \
   633 \        ==> Key K ~: analz (sees Spy evs) -->                     \
   634 \            Crypt K (Nonce NB) : parts (sees Spy evs) -->         \
   635 \            Crypt (shrK B) {|Agent A, Key K|}                     \
   636 \              : parts (sees Spy evs) -->                          \
   637 \            B ~: lost -->                                         \
   638 \             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   639 by (parts_induct_tac 1);
   640 (*Fake*)
   641 by (Fake_parts_insert_tac 1);
   642 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   643 by (fast_tac (!claset addSDs [Crypt_imp_invKey_keysFor] addss (!simpset)) 1); 
   644 (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   645 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   646 (*yes: apply unicity of session keys*)
   647 by (not_lost_tac "Aa" 1);
   648 by (blast_tac (!claset addSEs [MPair_parts]
   649                        addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   650 		       addDs  [Says_imp_sees_Spy RS parts.Inj,
   651 			       unique_session_keys]) 1);
   652 val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   653 
   654 (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   655   Moreover, A associates K with NB (thus is talking about the same run).
   656   Other premises guarantee secrecy of K.*)
   657 goal thy 
   658  "!!evs. [| Says B Server                                                   \
   659 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   660 \             : set evs;                                                    \
   661 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   662 \                       Crypt K (Nonce NB)|} : set evs;                     \
   663 \           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs);    \
   664 \           A ~: lost;  B ~: lost;  evs : yahalom |]       \
   665 \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   666 by (dtac B_trusts_YM4 1);
   667 by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
   668 by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
   669 by (rtac lemma 1);
   670 by (rtac Spy_not_see_encrypted_key 2);
   671 by (REPEAT_FIRST assume_tac);
   672 by (blast_tac (!claset addSEs [MPair_parts]
   673 	       	       addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   674 qed_spec_mp "YM4_imp_A_Said_YM3";