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