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