src/HOL/Auth/Yahalom.ML
author paulson
Wed Sep 17 16:37:40 1997 +0200 (1997-09-17)
changeset 3679 8df171ccdbd8
parent 3674 65ec38fbb265
child 3683 aafe719dff14
permissions -rw-r--r--
Fixed comments
     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  (*17 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 (*Base*)
   394 by (Blast_tac 1);
   395 (*Fake*) 
   396 by (spy_analz_tac 1);
   397 (*YM4*)  (** LEVEL 7 **)
   398 by (not_lost_tac "A" 1);
   399 by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
   400     THEN REPEAT (assume_tac 1));
   401 by (blast_tac (!claset addIs [KeyWithNonceI]) 1);
   402 qed_spec_mp "Nonce_secrecy";
   403 
   404 
   405 (*Version required below: if NB can be decrypted using a session key then it
   406   was distributed with that key.  The more general form above is required
   407   for the induction to carry through.*)
   408 goal thy 
   409  "!!evs. [| Says Server A                                                 \
   410 \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}    \
   411 \           : set evs;                                                    \
   412 \           NB ~= NB';  KAB ~: range shrK;  evs : yahalom |]         \
   413 \        ==> (Nonce NB : analz (insert (Key KAB) (sees Spy evs))) =  \
   414 \            (Nonce NB : analz (sees Spy evs))";
   415 by (asm_simp_tac (analz_image_freshK_ss addsimps 
   416 		  [Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
   417 qed "single_Nonce_secrecy";
   418 
   419 
   420 (*** The Nonce NB uniquely identifies B's message. ***)
   421 
   422 goal thy 
   423  "!!evs. evs : yahalom ==>                                            \
   424 \   EX NA' A' B'. ALL NA A B.                                              \
   425 \      Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(sees Spy evs) \
   426 \      --> B ~: lost --> NA = NA' & A = A' & B = B'";
   427 by (parts_induct_tac 1);
   428 (*Fake*)
   429 by (REPEAT (etac (exI RSN (2,exE)) 1)   (*stripping EXs makes proof faster*)
   430     THEN Fake_parts_insert_tac 1);
   431 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
   432 (*YM2: creation of new Nonce.  Move assertion into global context*)
   433 by (expand_case_tac "nb = ?y" 1);
   434 by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1));
   435 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   436 val lemma = result();
   437 
   438 goal thy 
   439  "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|}        \
   440 \                  : parts (sees Spy evs);            \
   441 \          Crypt (shrK B') {|Agent A', Nonce NA', nb|}     \
   442 \                  : parts (sees Spy evs);            \
   443 \          evs : yahalom;  B ~: lost;  B' ~: lost |]  \
   444 \        ==> NA' = NA & A' = A & B' = B";
   445 by (prove_unique_tac lemma 1);
   446 qed "unique_NB";
   447 
   448 
   449 (*Variant useful for proving secrecy of NB: the Says... form allows 
   450   not_lost_tac to remove the assumption B' ~: lost.*)
   451 goal thy 
   452  "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}    \
   453 \            : set evs;          B ~: lost;                               \
   454 \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
   455 \            : set evs;                                                   \
   456 \          nb ~: analz (sees Spy evs);  evs : yahalom |]        \
   457 \        ==> NA' = NA & A' = A & B' = B";
   458 by (not_lost_tac "B'" 1);
   459 by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   460                        addSEs [MPair_parts]
   461                        addDs  [unique_NB]) 1);
   462 qed "Says_unique_NB";
   463 
   464 
   465 (** A nonce value is never used both as NA and as NB **)
   466 
   467 goal thy 
   468  "!!evs. [| B ~: lost;  evs : yahalom  |]            \
   469 \ ==> Nonce NB ~: analz (sees Spy evs) -->           \
   470 \     Crypt (shrK B') {|Agent A', Nonce NB, nb'|}    \
   471 \       : parts(sees Spy evs)                        \
   472 \ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
   473 \       ~: parts(sees Spy evs)";
   474 by (parts_induct_tac 1);
   475 by (Fake_parts_insert_tac 1);
   476 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]
   477                        addSIs [parts_insertI]
   478                        addSEs partsEs) 1);
   479 bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
   480 
   481 (*The Server sends YM3 only in response to YM2.*)
   482 goal thy 
   483  "!!evs. [| Says Server A                                                \
   484 \            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs;     \
   485 \           evs : yahalom |]                                             \
   486 \        ==> EX B'. Says B' Server                                       \
   487 \                      {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |} \
   488 \                   : set evs";
   489 by (etac rev_mp 1);
   490 by (etac yahalom.induct 1);
   491 by (ALLGOALS Asm_simp_tac);
   492 by (ALLGOALS Blast_tac);
   493 qed "Says_Server_imp_YM2";
   494 
   495 
   496 (*A vital theorem for B, that nonce NB remains secure from the Spy.*)
   497 goal thy 
   498  "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom |]  \
   499 \ ==> Says B Server                                                    \
   500 \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
   501 \     : set evs -->                                                    \
   502 \     (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs) -->     \
   503 \     Nonce NB ~: analz (sees Spy evs)";
   504 by (etac yahalom.induct 1);
   505 by analz_sees_tac;
   506 by (ALLGOALS
   507     (asm_simp_tac 
   508      (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
   509                setloop split_tac [expand_if])));
   510 (*Prove YM3 by showing that no NB can also be an NA*)
   511 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
   512 	               addSEs [MPair_parts]
   513 		       addDs  [no_nonce_YM1_YM2, Says_unique_NB]) 4
   514     THEN flexflex_tac);
   515 (*YM2: similar freshness reasoning*) 
   516 by (blast_tac (!claset addSEs partsEs
   517 		       addDs  [Says_imp_sees_Spy RS analz.Inj,
   518 			       impOfSubs analz_subset_parts]) 3);
   519 (*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*)
   520 by (blast_tac (!claset addSIs [parts_insertI]
   521                        addSEs sees_Spy_partsEs) 2);
   522 (*Fake*)
   523 by (spy_analz_tac 1);
   524 (** LEVEL 7: YM4 and Oops remain **)
   525 (*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
   526 by (REPEAT (Safe_step_tac 1));
   527 by (not_lost_tac "Aa" 1);
   528 by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1);
   529 by (forward_tac [Says_Server_message_form] 3);
   530 by (forward_tac [Says_Server_imp_YM2] 4);
   531 by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE]));
   532 (*  use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *)
   533 by (blast_tac (!claset addDs [Says_unique_NB, Spy_not_see_encrypted_key,
   534 			      impOfSubs Fake_analz_insert]) 1);
   535 (** LEVEL 14 **)
   536 (*Oops case: if the nonce is betrayed now, show that the Oops event is 
   537   covered by the quantified Oops assumption.*)
   538 by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   539 by (step_tac (!claset delrules [disjE, conjI]) 1);
   540 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1);
   541 by (expand_case_tac "NB = NBa" 1);
   542 (*If NB=NBa then all other components of the Oops message agree*)
   543 by (blast_tac (!claset addDs [Says_unique_NB]) 1 THEN flexflex_tac);
   544 (*case NB ~= NBa*)
   545 by (asm_simp_tac (!simpset addsimps [single_Nonce_secrecy]) 1);
   546 by (blast_tac (!claset addSEs [MPair_parts]
   547 		       addDs  [Says_imp_sees_Spy RS parts.Inj, 
   548 			       no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1);
   549 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
   550 
   551 
   552 (*B's session key guarantee from YM4.  The two certificates contribute to a
   553   single conclusion about the Server's message.  Note that the "Says A Spy"
   554   assumption must quantify over ALL POSSIBLE keys instead of our particular K.
   555   If this run is broken and the spy substitutes a certificate containing an
   556   old key, B has no means of telling.*)
   557 goal thy 
   558  "!!evs. [| Says B Server                                                   \
   559 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   560 \             : set evs;                                                    \
   561 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   562 \                       Crypt K (Nonce NB)|} : set evs;                     \
   563 \           ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs;         \
   564 \           A ~: lost;  B ~: lost;  evs : yahalom |]       \
   565 \         ==> Says Server A                                                 \
   566 \                     {|Crypt (shrK A) {|Agent B, Key K,                    \
   567 \                               Nonce NA, Nonce NB|},                       \
   568 \                       Crypt (shrK B) {|Agent A, Key K|}|}                 \
   569 \               : set evs";
   570 by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   571 by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN
   572     dtac B_trusts_YM4_shrK 1);
   573 by (dtac B_trusts_YM4_newK 3);
   574 by (REPEAT_FIRST (eresolve_tac [asm_rl, exE]));
   575 by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1);
   576 by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1));
   577 by (blast_tac (!claset addDs [Says_unique_NB]) 1);
   578 qed "B_trusts_YM4";
   579 
   580 
   581 
   582 (*** Authenticating B to A ***)
   583 
   584 (*The encryption in message YM2 tells us it cannot be faked.*)
   585 goal thy 
   586  "!!evs. evs : yahalom                                            \
   587 \  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|}                   \
   588 \        : parts (sees Spy evs) -->                               \
   589 \      B ~: lost -->                                              \
   590 \      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   591 \         : set evs";
   592 by (parts_induct_tac 1);
   593 by (Fake_parts_insert_tac 1);
   594 bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
   595 
   596 (*If the server sends YM3 then B sent YM2*)
   597 goal thy 
   598  "!!evs. evs : yahalom                                                      \
   599 \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   600 \         : set evs -->                                                     \
   601 \      B ~: lost -->                                                        \
   602 \      Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}  \
   603 \                 : set evs";
   604 by (etac yahalom.induct 1);
   605 by (ALLGOALS Asm_simp_tac);
   606 (*YM4*)
   607 by (Blast_tac 2);
   608 (*YM3*)
   609 by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_sees_Spy RS parts.Inj]
   610 		      addSEs [MPair_parts]) 1);
   611 val lemma = result() RSN (2, rev_mp) RS mp |> standard;
   612 
   613 (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
   614 goal thy
   615  "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
   616 \             : set evs;                                                    \
   617 \           A ~: lost;  B ~: lost;  evs : yahalom |]                        \
   618 \   ==> Says B Server {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, nb|}|} \
   619 \         : set evs";
   620 by (blast_tac (!claset addSDs [A_trusts_YM3, lemma]
   621 		       addEs sees_Spy_partsEs) 1);
   622 qed "YM3_auth_B_to_A";
   623 
   624 
   625 (*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***)
   626 
   627 (*Assuming the session key is secure, if both certificates are present then
   628   A has said NB.  We can't be sure about the rest of A's message, but only
   629   NB matters for freshness.*)  
   630 goal thy 
   631  "!!evs. evs : yahalom                                             \
   632 \        ==> Key K ~: analz (sees Spy evs) -->                     \
   633 \            Crypt K (Nonce NB) : parts (sees Spy evs) -->         \
   634 \            Crypt (shrK B) {|Agent A, Key K|}                     \
   635 \              : parts (sees Spy evs) -->                          \
   636 \            B ~: lost -->                                         \
   637 \             (EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs)";
   638 by (parts_induct_tac 1);
   639 (*Fake*)
   640 by (Fake_parts_insert_tac 1);
   641 (*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*)
   642 by (fast_tac (!claset addSDs [Crypt_imp_invKey_keysFor] addss (!simpset)) 1); 
   643 (*YM4: was Crypt K (Nonce NB) the very last message?  If not, use ind. hyp.*)
   644 by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1);
   645 (*yes: apply unicity of session keys*)
   646 by (not_lost_tac "Aa" 1);
   647 by (blast_tac (!claset addSEs [MPair_parts]
   648                        addSDs [A_trusts_YM3, B_trusts_YM4_shrK]
   649 		       addDs  [Says_imp_sees_Spy RS parts.Inj,
   650 			       unique_session_keys]) 1);
   651 val lemma = normalize_thm [RSspec, RSmp] (result()) |> standard;
   652 
   653 (*If B receives YM4 then A has used nonce NB (and therefore is alive).
   654   Moreover, A associates K with NB (thus is talking about the same run).
   655   Other premises guarantee secrecy of K.*)
   656 goal thy 
   657  "!!evs. [| Says B Server                                                   \
   658 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \
   659 \             : set evs;                                                    \
   660 \           Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
   661 \                       Crypt K (Nonce NB)|} : set evs;                     \
   662 \           (ALL NA k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set evs);    \
   663 \           A ~: lost;  B ~: lost;  evs : yahalom |]       \
   664 \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   665 by (dtac B_trusts_YM4 1);
   666 by (REPEAT_FIRST (eresolve_tac [asm_rl, spec]));
   667 by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1);
   668 by (rtac lemma 1);
   669 by (rtac Spy_not_see_encrypted_key 2);
   670 by (REPEAT_FIRST assume_tac);
   671 by (blast_tac (!claset addSEs [MPair_parts]
   672 	       	       addDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   673 qed_spec_mp "YM4_imp_A_Said_YM3";