src/HOL/Auth/TLS.ML
author wenzelm
Fri Dec 19 10:28:33 1997 +0100 (1997-12-19)
changeset 4449 df30e75f670f
parent 4423 a129b817b58a
child 4472 cfa3bd184bc1
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOL/Auth/TLS
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 Protocol goals: 
     7 * M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
     8      parties (though A is not necessarily authenticated).
     9 
    10 * B upon receiving CertVerify knows that A is present (But this
    11     message is optional!)
    12 
    13 * A upon receiving ServerFinished knows that B is present
    14 
    15 * Each party who has received a FINISHED message can trust that the other
    16   party agrees on all message components, including PA and PB (thus foiling
    17   rollback attacks).
    18 *)
    19 
    20 open TLS;
    21 
    22 set proof_timing;
    23 HOL_quantifiers := false;
    24 
    25 (*Automatically unfold the definition of "certificate"*)
    26 Addsimps [certificate_def];
    27 
    28 (*Injectiveness of key-generating functions*)
    29 AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq];
    30 
    31 (* invKey(sessionK x) = sessionK x*)
    32 Addsimps [isSym_sessionK, rewrite_rule [isSymKey_def] isSym_sessionK];
    33 
    34 
    35 (*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
    36 
    37 goal thy "pubK A ~= sessionK arg";
    38 by (rtac notI 1);
    39 by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    40 by (Full_simp_tac 1);
    41 qed "pubK_neq_sessionK";
    42 
    43 goal thy "priK A ~= sessionK arg";
    44 by (rtac notI 1);
    45 by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    46 by (Full_simp_tac 1);
    47 qed "priK_neq_sessionK";
    48 
    49 val keys_distinct = [pubK_neq_sessionK, priK_neq_sessionK];
    50 AddIffs (keys_distinct @ (keys_distinct RL [not_sym]));
    51 
    52 
    53 (**** Protocol Proofs ****)
    54 
    55 (*Possibility properties state that some traces run the protocol to the end.
    56   Four paths and 12 rules are considered.*)
    57 
    58 
    59 (** These proofs assume that the Nonce_supply nonces 
    60 	(which have the form  @ N. Nonce N ~: used evs)
    61     lie outside the range of PRF.  It seems reasonable, but as it is needed
    62     only for the possibility theorems, it is not taken as an axiom.
    63 **)
    64 
    65 
    66 (*Possibility property ending with ClientAccepts.*)
    67 goal thy 
    68  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    69 \           A ~= B |]            \
    70 \  ==> EX SID M. EX evs: tls.    \
    71 \        Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
    72 by (REPEAT (resolve_tac [exI,bexI] 1));
    73 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
    74 	  tls.ClientKeyExch RS tls.ClientFinished RS tls.ServerFinished RS
    75 	  tls.ClientAccepts) 2);
    76 by possibility_tac;
    77 by (REPEAT (Blast_tac 1));
    78 result();
    79 
    80 (*And one for ServerAccepts.  Either FINISHED message may come first.*)
    81 goal thy 
    82  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    83 \           A ~= B |]                        \
    84 \  ==> EX SID NA PA NB PB M. EX evs: tls.    \
    85 \        Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
    86 by (REPEAT (resolve_tac [exI,bexI] 1));
    87 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
    88 	  tls.ClientKeyExch RS tls.ServerFinished RS tls.ClientFinished RS
    89 	  tls.ServerAccepts) 2);
    90 by possibility_tac;
    91 by (REPEAT (Blast_tac 1));
    92 result();
    93 
    94 (*Another one, for CertVerify (which is optional)*)
    95 goal thy 
    96  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    97 \           A ~= B |]                       \
    98 \  ==> EX NB PMS. EX evs: tls.   \
    99 \  Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) : set evs";
   100 by (REPEAT (resolve_tac [exI,bexI] 1));
   101 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
   102 	  tls.ClientKeyExch RS tls.CertVerify) 2);
   103 by possibility_tac;
   104 by (REPEAT (Blast_tac 1));
   105 result();
   106 
   107 (*Another one, for session resumption (both ServerResume and ClientResume) *)
   108 goal thy 
   109  "!!A B. [| evs0 : tls;     \
   110 \           Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
   111 \           Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
   112 \           ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
   113 \           A ~= B |] ==> EX NA PA NB PB X. EX evs: tls.    \
   114 \      X = Hash{|Number SID, Nonce M,             \
   115 \                       Nonce NA, Number PA, Agent A,      \
   116 \                       Nonce NB, Number PB, Agent B|}  &  \
   117 \      Says A B (Crypt (clientK(NA,NB,M)) X) : set evs  &  \
   118 \      Says B A (Crypt (serverK(NA,NB,M)) X) : set evs";
   119 by (REPEAT (resolve_tac [exI,bexI] 1));
   120 by (etac (tls.ClientHello RS tls.ServerHello RS tls.ServerResume RS 
   121 	  tls.ClientResume) 2);
   122 by possibility_tac;
   123 by (REPEAT (Blast_tac 1));
   124 result();
   125 
   126 
   127 
   128 (**** Inductive proofs about tls ****)
   129 
   130 (*Nobody sends themselves messages*)
   131 goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
   132 by (etac tls.induct 1);
   133 by (Auto_tac());
   134 qed_spec_mp "not_Says_to_self";
   135 Addsimps [not_Says_to_self];
   136 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   137 
   138 
   139 (*Induction for regularity theorems.  If induction formula has the form
   140    X ~: analz (spies evs) --> ... then it shortens the proof by discarding
   141    needless information about analz (insert X (spies evs))  *)
   142 fun parts_induct_tac i = 
   143     etac tls.induct i
   144     THEN 
   145     REPEAT (FIRSTGOAL analz_mono_contra_tac)
   146     THEN 
   147     fast_tac (claset() addss (simpset())) i THEN
   148     ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if]));
   149 
   150 
   151 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
   152     sends messages containing X! **)
   153 
   154 (*Spy never sees another agent's private key! (unless it's bad at start)*)
   155 goal thy 
   156  "!!evs. evs : tls ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
   157 by (parts_induct_tac 1);
   158 by (Fake_parts_insert_tac 1);
   159 qed "Spy_see_priK";
   160 Addsimps [Spy_see_priK];
   161 
   162 goal thy 
   163  "!!evs. evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
   164 by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
   165 qed "Spy_analz_priK";
   166 Addsimps [Spy_analz_priK];
   167 
   168 goal thy  "!!A. [| Key (priK A) : parts (spies evs);  evs : tls |] ==> A:bad";
   169 by (blast_tac (claset() addDs [Spy_see_priK]) 1);
   170 qed "Spy_see_priK_D";
   171 
   172 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
   173 AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
   174 
   175 
   176 (*This lemma says that no false certificates exist.  One might extend the
   177   model to include bogus certificates for the agents, but there seems
   178   little point in doing so: the loss of their private keys is a worse
   179   breach of security.*)
   180 goalw thy [certificate_def]
   181  "!!evs. [| certificate B KB : parts (spies evs);  evs : tls |]  \
   182 \        ==> pubK B = KB";
   183 by (etac rev_mp 1);
   184 by (parts_induct_tac 1);
   185 by (Fake_parts_insert_tac 1);
   186 qed "certificate_valid";
   187 
   188 
   189 (*Replace key KB in ClientKeyExch by (pubK B) *)
   190 val ClientKeyExch_tac = 
   191     forward_tac [Says_imp_spies RS parts.Inj RS certificate_valid]
   192     THEN' assume_tac
   193     THEN' hyp_subst_tac;
   194 
   195 fun analz_induct_tac i = 
   196     etac tls.induct i   THEN
   197     ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
   198     ALLGOALS (asm_simp_tac 
   199               (simpset() addcongs [if_weak_cong]
   200                          addsimps (expand_ifs@pushes)
   201                          addsplits [expand_if]))  THEN
   202     (*Remove instances of pubK B:  the Spy already knows all public keys.
   203       Combining the two simplifier calls makes them run extremely slowly.*)
   204     ALLGOALS (asm_simp_tac 
   205               (simpset() addcongs [if_weak_cong]
   206 			 addsimps [insert_absorb]
   207                          addsplits [expand_if]));
   208 
   209 
   210 (*** Properties of items found in Notes ***)
   211 
   212 goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
   213 \                ==> Crypt (pubK B) X : parts (spies evs)";
   214 by (etac rev_mp 1);
   215 by (analz_induct_tac 1);
   216 by (blast_tac (claset() addIs [parts_insertI]) 1);
   217 qed "Notes_Crypt_parts_spies";
   218 
   219 (*C may be either A or B*)
   220 goal thy
   221  "!!evs. [| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs; \
   222 \           evs : tls     \
   223 \        |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)";
   224 by (etac rev_mp 1);
   225 by (parts_induct_tac 1);
   226 by (ALLGOALS Clarify_tac);
   227 (*Fake*)
   228 by (blast_tac (claset() addIs [parts_insertI]) 1);
   229 (*Client, Server Accept*)
   230 by (REPEAT (blast_tac (claset() addSEs spies_partsEs
   231                                 addSDs [Notes_Crypt_parts_spies]) 1));
   232 qed "Notes_master_imp_Crypt_PMS";
   233 
   234 (*Compared with the theorem above, both premise and conclusion are stronger*)
   235 goal thy
   236  "!!evs. [| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs;\
   237 \           evs : tls     \
   238 \        |] ==> Notes A {|Agent B, Nonce PMS|} : set evs";
   239 by (etac rev_mp 1);
   240 by (parts_induct_tac 1);
   241 (*ServerAccepts*)
   242 by (Fast_tac 1);	(*Blast_tac's very slow here*)
   243 qed "Notes_master_imp_Notes_PMS";
   244 
   245 
   246 (*** Protocol goal: if B receives CertVerify, then A sent it ***)
   247 
   248 (*B can check A's signature if he has received A's certificate.*)
   249 goal thy
   250  "!!evs. [| X : parts (spies evs);                          \
   251 \           X = Crypt (priK A) (Hash{|nb, Agent B, pms|});  \
   252 \           evs : tls;  A ~: bad |]                         \
   253 \    ==> Says A B X : set evs";
   254 by (etac rev_mp 1);
   255 by (hyp_subst_tac 1);
   256 by (parts_induct_tac 1);
   257 by (Fake_parts_insert_tac 1);
   258 val lemma = result();
   259 
   260 (*Final version: B checks X using the distributed KA instead of priK A*)
   261 goal thy
   262  "!!evs. [| X : parts (spies evs);                            \
   263 \           X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \
   264 \           certificate A KA : parts (spies evs);             \
   265 \           evs : tls;  A ~: bad |]                           \
   266 \    ==> Says A B X : set evs";
   267 by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1);
   268 qed "TrustCertVerify";
   269 
   270 
   271 (*If CertVerify is present then A has chosen PMS.*)
   272 goal thy
   273  "!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \
   274 \             : parts (spies evs);                          \
   275 \           evs : tls;  A ~: bad |]                         \
   276 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
   277 by (etac rev_mp 1);
   278 by (parts_induct_tac 1);
   279 by (Fake_parts_insert_tac 1);
   280 val lemma = result();
   281 
   282 (*Final version using the distributed KA instead of priK A*)
   283 goal thy
   284  "!!evs. [| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}) \
   285 \             : parts (spies evs);                             \
   286 \           certificate A KA : parts (spies evs);              \
   287 \           evs : tls;  A ~: bad |]                            \
   288 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
   289 by (blast_tac (claset() addSDs [certificate_valid] addSIs [lemma]) 1);
   290 qed "UseCertVerify";
   291 
   292 
   293 goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
   294 by (parts_induct_tac 1);
   295 (*ClientKeyExch: PMS is assumed to differ from any PRF.*)
   296 by (Blast_tac 1);
   297 qed "no_Notes_A_PRF";
   298 Addsimps [no_Notes_A_PRF];
   299 
   300 
   301 goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (spies evs);  \
   302 \                   evs : tls |]  \
   303 \                ==> Nonce PMS : parts (spies evs)";
   304 by (etac rev_mp 1);
   305 by (parts_induct_tac 1);
   306 by (ALLGOALS (asm_simp_tac (simpset() addsimps [parts_insert_spies])));
   307 by (Fake_parts_insert_tac 1);
   308 (*Six others, all trivial or by freshness*)
   309 by (REPEAT (blast_tac (claset() addSDs [Notes_Crypt_parts_spies]
   310                                 addSEs spies_partsEs) 1));
   311 qed "MS_imp_PMS";
   312 AddSDs [MS_imp_PMS];
   313 
   314 
   315 
   316 (*** Unicity results for PMS, the pre-master-secret ***)
   317 
   318 (*PMS determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
   319 goal thy 
   320  "!!evs. [| Nonce PMS ~: analz (spies evs);  evs : tls |]   \
   321 \        ==> EX B'. ALL B.   \
   322 \              Crypt (pubK B) (Nonce PMS) : parts (spies evs) --> B=B'";
   323 by (etac rev_mp 1);
   324 by (parts_induct_tac 1);
   325 by (Fake_parts_insert_tac 1);
   326 (*ClientKeyExch*)
   327 by (ClientKeyExch_tac 1);
   328 by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1);
   329 by (expand_case_tac "PMS = ?y" 1 THEN
   330     blast_tac (claset() addSEs partsEs) 1);
   331 val lemma = result();
   332 
   333 goal thy 
   334  "!!evs. [| Crypt(pubK B)  (Nonce PMS) : parts (spies evs); \
   335 \           Crypt(pubK B') (Nonce PMS) : parts (spies evs); \
   336 \           Nonce PMS ~: analz (spies evs);                 \
   337 \           evs : tls |]                                          \
   338 \        ==> B=B'";
   339 by (prove_unique_tac lemma 1);
   340 qed "Crypt_unique_PMS";
   341 
   342 
   343 (** It is frustrating that we need two versions of the unicity results.
   344     But Notes A {|Agent B, Nonce PMS|} determines both A and B.  Sometimes
   345     we have only the weaker assertion Crypt(pubK B) (Nonce PMS), which 
   346     determines B alone, and only if PMS is secret.
   347 **)
   348 
   349 (*In A's internal Note, PMS determines A and B.*)
   350 goal thy "!!evs. evs : tls               \
   351 \                ==> EX A' B'. ALL A B.  \
   352 \                    Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
   353 by (parts_induct_tac 1);
   354 by (asm_simp_tac (simpset() addsimps [all_conj_distrib]) 1);
   355 (*ClientKeyExch: if PMS is fresh, then it can't appear in Notes A X.*)
   356 by (expand_case_tac "PMS = ?y" 1 THEN
   357     blast_tac (claset() addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1);
   358 val lemma = result();
   359 
   360 goal thy 
   361  "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
   362 \           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
   363 \           evs : tls |]                               \
   364 \        ==> A=A' & B=B'";
   365 by (prove_unique_tac lemma 1);
   366 qed "Notes_unique_PMS";
   367 
   368 
   369 
   370 (**** Secrecy Theorems ****)
   371 
   372 (*Key compromise lemma needed to prove analz_image_keys.
   373   No collection of keys can help the spy get new private keys.*)
   374 goal thy  
   375  "!!evs. evs : tls ==>                                      \
   376 \  ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
   377 \          (priK B : KK | B : bad)";
   378 by (etac tls.induct 1);
   379 by (ALLGOALS
   380     (asm_simp_tac (analz_image_keys_ss
   381 		   addsimps (certificate_def::keys_distinct))));
   382 (*Fake*) 
   383 by (spy_analz_tac 1);
   384 qed_spec_mp "analz_image_priK";
   385 
   386 
   387 (*slightly speeds up the big simplification below*)
   388 goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
   389 by (Blast_tac 1);
   390 val range_sessionkeys_not_priK = result();
   391 
   392 (*Lemma for the trivial direction of the if-and-only-if*)
   393 goal thy  
   394  "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
   395 \        (X : analz (G Un H))  =  (X : analz H)";
   396 by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
   397 val analz_image_keys_lemma = result();
   398 
   399 (** Strangely, the following version doesn't work:
   400 \    ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
   401 \           (Nonce N : analz (spies evs))";
   402 **)
   403 
   404 goal thy  
   405  "!!evs. evs : tls ==>                                    \
   406 \    ALL KK. KK <= range sessionK -->                     \
   407 \            (Nonce N : analz (Key``KK Un (spies evs))) = \
   408 \            (Nonce N : analz (spies evs))";
   409 by (etac tls.induct 1);
   410 by (ClientKeyExch_tac 7);
   411 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   412 by (REPEAT_FIRST (rtac analz_image_keys_lemma));
   413 by (ALLGOALS    (*18 seconds*)
   414     (asm_simp_tac (analz_image_keys_ss 
   415 		   addsimps (expand_ifs@pushes)
   416 		   addsimps [range_sessionkeys_not_priK, 
   417                              analz_image_priK, certificate_def])));
   418 by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
   419 (*Fake*) 
   420 by (spy_analz_tac 1);
   421 qed_spec_mp "analz_image_keys";
   422 
   423 (*Knowing some session keys is no help in getting new nonces*)
   424 goal thy
   425  "!!evs. evs : tls ==>          \
   426 \        Nonce N : analz (insert (Key (sessionK z)) (spies evs)) =  \
   427 \        (Nonce N : analz (spies evs))";
   428 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1);
   429 qed "analz_insert_key";
   430 Addsimps [analz_insert_key];
   431 
   432 
   433 (*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
   434 
   435 (** Some lemmas about session keys, comprising clientK and serverK **)
   436 
   437 
   438 (*Lemma: session keys are never used if PMS is fresh.  
   439   Nonces don't have to agree, allowing session resumption.
   440   Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
   441   THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
   442 goal thy 
   443  "!!evs. [| Nonce PMS ~: parts (spies evs);  \
   444 \           K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b);  \
   445 \           evs : tls |]             \
   446 \  ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
   447 by (etac rev_mp 1);
   448 by (hyp_subst_tac 1);
   449 by (analz_induct_tac 1);
   450 (*SpyKeys*)
   451 by (blast_tac (claset() addSEs spies_partsEs) 3);
   452 (*Fake*)
   453 by (simp_tac (simpset() addsimps [parts_insert_spies]) 2);
   454 by (Fake_parts_insert_tac 2);
   455 (** LEVEL 6 **)
   456 (*Oops*)
   457 by (fast_tac (claset() addSEs [MPair_parts]
   458 		       addDs  [Says_imp_spies RS parts.Inj]
   459 		       addss (simpset())) 6);
   460 by (REPEAT 
   461     (blast_tac (claset() addSDs [Notes_Crypt_parts_spies, 
   462 				 Notes_master_imp_Crypt_PMS]
   463                          addSEs spies_partsEs) 1));
   464 val lemma = result();
   465 
   466 goal thy 
   467  "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   468 \  ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)";
   469 by (blast_tac (claset() addDs [lemma]) 1);
   470 qed "PMS_sessionK_not_spied";
   471 bind_thm ("PMS_sessionK_spiedE", 
   472 	  PMS_sessionK_not_spied RSN (2,rev_notE));
   473 
   474 goal thy 
   475  "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   476 \  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
   477 by (blast_tac (claset() addDs [lemma]) 1);
   478 qed "PMS_Crypt_sessionK_not_spied";
   479 bind_thm ("PMS_Crypt_sessionK_spiedE", 
   480 	  PMS_Crypt_sessionK_not_spied RSN (2,rev_notE));
   481 
   482 (*Lemma: write keys are never sent if M (MASTER SECRET) is secure.  
   483   Converse doesn't hold; betraying M doesn't force the keys to be sent!
   484   The strong Oops condition can be weakened later by unicity reasoning, 
   485 	with some effort.*)
   486 goal thy 
   487  "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
   488 \           Nonce M ~: analz (spies evs);  evs : tls |]   \
   489 \        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
   490 by (etac rev_mp 1);
   491 by (etac rev_mp 1);
   492 by (analz_induct_tac 1);        (*17 seconds*)
   493 (*Oops*)
   494 by (Blast_tac 4);
   495 (*SpyKeys*)
   496 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 3);
   497 (*Fake*) 
   498 by (spy_analz_tac 2);
   499 (*Base*)
   500 by (Blast_tac 1);
   501 qed "sessionK_not_spied";
   502 Addsimps [sessionK_not_spied];
   503 
   504 
   505 (*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
   506 goal thy
   507  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
   508 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   509 \            Nonce PMS ~: analz (spies evs)";
   510 by (analz_induct_tac 1);   (*11 seconds*)
   511 (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
   512 by (REPEAT (fast_tac (claset() addss (simpset())) 6));
   513 (*ClientHello, ServerHello, ClientKeyExch, ServerResume: 
   514   mostly freshness reasoning*)
   515 by (REPEAT (blast_tac (claset() addSEs partsEs
   516 				addDs  [Notes_Crypt_parts_spies,
   517 					impOfSubs analz_subset_parts,
   518 					Says_imp_spies RS analz.Inj]) 3));
   519 (*SpyKeys*)
   520 by (fast_tac (claset() addss (simpset())) 2);
   521 (*Fake*)
   522 by (spy_analz_tac 1);
   523 bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
   524 
   525 
   526 (*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
   527   will stay secret.*)
   528 goal thy
   529  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
   530 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   531 \            Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
   532 by (analz_induct_tac 1);   (*13 seconds*)
   533 (*ClientAccepts and ServerAccepts: because PMS was already visible*)
   534 by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS, 
   535 				       Says_imp_spies RS analz.Inj,
   536 				       Notes_imp_spies RS analz.Inj]) 6));
   537 (*ClientHello*)
   538 by (Blast_tac 3);
   539 (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
   540 by (blast_tac (claset() addSDs [Spy_not_see_PMS, 
   541 				Says_imp_spies RS analz.Inj]) 2);
   542 (*Fake*)
   543 by (spy_analz_tac 1);
   544 (*ServerHello and ClientKeyExch: mostly freshness reasoning*)
   545 by (REPEAT (blast_tac (claset() addSEs partsEs
   546 				addDs  [Notes_Crypt_parts_spies,
   547 					impOfSubs analz_subset_parts,
   548 					Says_imp_spies RS analz.Inj]) 1));
   549 bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
   550 
   551 
   552 (*** Weakening the Oops conditions for leakage of clientK ***)
   553 
   554 (*If A created PMS then nobody other than the Spy would send a message
   555   using a clientK generated from that PMS.*)
   556 goal thy
   557  "!!evs. [| evs : tls;  A' ~= Spy |]                \
   558 \  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   559 \      Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
   560 \      A = A'";
   561 by (analz_induct_tac 1);	(*8 seconds*)
   562 by (ALLGOALS Clarify_tac);
   563 (*ClientFinished, ClientResume: by unicity of PMS*)
   564 by (REPEAT 
   565     (blast_tac (claset() addSDs [Notes_master_imp_Notes_PMS]
   566      	 	         addIs  [Notes_unique_PMS RS conjunct1]) 2));
   567 (*ClientKeyExch*)
   568 by (blast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]
   569 	                addSDs [Says_imp_spies RS parts.Inj]) 1);
   570 bind_thm ("Says_clientK_unique",
   571 	  result() RSN(2,rev_mp) RSN(2,rev_mp));
   572 
   573 
   574 (*If A created PMS and has not leaked her clientK to the Spy, 
   575   then nobody has.*)
   576 goal thy
   577  "!!evs. evs : tls                         \
   578 \  ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
   579 \      Notes A {|Agent B, Nonce PMS|} : set evs -->                   \
   580 \      (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) ";
   581 by (etac tls.induct 1);
   582 (*This roundabout proof sequence avoids looping in simplification*)
   583 by (ALLGOALS Simp_tac);
   584 by (ALLGOALS Clarify_tac);
   585 by (Fake_parts_insert_tac 1);
   586 by (ALLGOALS Asm_simp_tac);
   587 (*Oops*)
   588 by (blast_tac (claset() addIs [Says_clientK_unique]) 2);
   589 (*ClientKeyExch*)
   590 by (blast_tac (claset() addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1);
   591 qed_spec_mp "clientK_Oops_ALL";
   592 
   593 
   594 
   595 (*** Weakening the Oops conditions for leakage of serverK ***)
   596 
   597 (*If A created PMS for B, then nobody other than B or the Spy would
   598   send a message using a serverK generated from that PMS.*)
   599 goal thy
   600  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad;  B' ~= Spy |]                \
   601 \  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   602 \      Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
   603 \      B = B'";
   604 by (analz_induct_tac 1);	(*9 seconds*)
   605 by (ALLGOALS Clarify_tac);
   606 (*ServerResume, ServerFinished: by unicity of PMS*)
   607 by (REPEAT
   608     (blast_tac (claset() addSEs [MPair_parts]
   609 			 addSDs [Notes_master_imp_Crypt_PMS, 
   610 				 Says_imp_spies RS parts.Inj]
   611 			 addDs  [Spy_not_see_PMS, 
   612 				 Notes_Crypt_parts_spies,
   613 				 Crypt_unique_PMS]) 2));
   614 (*ClientKeyExch*)
   615 by (blast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]
   616 	                addSDs [Says_imp_spies RS parts.Inj]) 1);
   617 bind_thm ("Says_serverK_unique",
   618 	  result() RSN(2,rev_mp) RSN(2,rev_mp));
   619 
   620 (*If A created PMS for B, and B has not leaked his serverK to the Spy, 
   621   then nobody has.*)
   622 goal thy
   623  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                        \
   624 \  ==> Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
   625 \      Notes A {|Agent B, Nonce PMS|} : set evs -->                   \
   626 \      (ALL A. Says A Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) ";
   627 by (etac tls.induct 1);
   628 (*This roundabout proof sequence avoids looping in simplification*)
   629 by (ALLGOALS Simp_tac);
   630 by (ALLGOALS Clarify_tac);
   631 by (Fake_parts_insert_tac 1);
   632 by (ALLGOALS Asm_simp_tac);
   633 (*Oops*)
   634 by (blast_tac (claset() addIs [Says_serverK_unique]) 2);
   635 (*ClientKeyExch*)
   636 by (blast_tac (claset() addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1);
   637 qed_spec_mp "serverK_Oops_ALL";
   638 
   639 
   640 
   641 (*** Protocol goals: if A receives ServerFinished, then B is present 
   642      and has used the quoted values PA, PB, etc.  Note that it is up to A
   643      to compare PA with what she originally sent.
   644 ***)
   645 
   646 (*The mention of her name (A) in X assures A that B knows who she is.*)
   647 goal thy
   648  "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
   649 \                 (Hash{|Number SID, Nonce M,             \
   650 \                        Nonce Na, Number PA, Agent A,    \
   651 \                        Nonce Nb, Number PB, Agent B|}); \
   652 \           M = PRF(PMS,NA,NB);                           \
   653 \           evs : tls;  A ~: bad;  B ~: bad |]            \
   654 \        ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \
   655 \            Notes A {|Agent B, Nonce PMS|} : set evs --> \
   656 \            X : parts (spies evs) --> Says B A X : set evs";
   657 by (hyp_subst_tac 1);
   658 by (analz_induct_tac 1);        (*26 seconds*)
   659 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   660 (*proves ServerResume*)
   661 by (ALLGOALS Clarify_tac);
   662 (*ClientKeyExch: blast_tac gives PROOF FAILED*)
   663 by (fast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]) 2);
   664 (*Fake: the Spy doesn't have the critical session key!*)
   665 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   666 by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
   667 				      not_parts_not_analz]) 2);
   668 by (Fake_parts_insert_tac 1);
   669 val lemma = normalize_thm [RSmp] (result());
   670 
   671 (*Final version*)
   672 goal thy
   673  "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
   674 \                 (Hash{|Number SID, Nonce M,             \
   675 \                        Nonce Na, Number PA, Agent A,    \
   676 \                        Nonce Nb, Number PB, Agent B|}); \
   677 \           M = PRF(PMS,NA,NB);                           \
   678 \           X : parts (spies evs);                        \
   679 \           Notes A {|Agent B, Nonce PMS|} : set evs;     \
   680 \           Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   681 \           evs : tls;  A ~: bad;  B ~: bad |]          \
   682 \        ==> Says B A X : set evs";
   683 by (blast_tac (claset() addIs [lemma]
   684                         addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
   685 qed_spec_mp "TrustServerFinished";
   686 
   687 
   688 
   689 (*This version refers not to ServerFinished but to any message from B.
   690   We don't assume B has received CertVerify, and an intruder could
   691   have changed A's identity in all other messages, so we can't be sure
   692   that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   693   to bind A's identity with PMS, then we could replace A' by A below.*)
   694 goal thy
   695  "!!evs. [| M = PRF(PMS,NA,NB);  evs : tls;  A ~: bad;  B ~: bad |]     \
   696 \        ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \
   697 \            Notes A {|Agent B, Nonce PMS|} : set evs -->              \
   698 \            Crypt (serverK(Na,Nb,M)) Y : parts (spies evs)  -->  \
   699 \            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
   700 by (hyp_subst_tac 1);
   701 by (analz_induct_tac 1);	(*20 seconds*)
   702 by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
   703 by (ALLGOALS Clarify_tac);
   704 (*ServerResume, ServerFinished: by unicity of PMS*)
   705 by (REPEAT
   706     (blast_tac (claset() addSEs [MPair_parts]
   707 			 addSDs [Notes_master_imp_Crypt_PMS, 
   708 				 Says_imp_spies RS parts.Inj]
   709 			 addDs  [Spy_not_see_PMS, 
   710 				 Notes_Crypt_parts_spies,
   711 				 Crypt_unique_PMS]) 3));
   712 (*ClientKeyExch*)
   713 by (blast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]) 2);
   714 (*Fake: the Spy doesn't have the critical session key!*)
   715 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   716 by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
   717 				      not_parts_not_analz]) 2);
   718 by (Fake_parts_insert_tac 1);
   719 val lemma = normalize_thm [RSmp] (result());
   720 
   721 (*Final version*)
   722 goal thy
   723  "!!evs. [| M = PRF(PMS,NA,NB);                           \
   724 \           Crypt (serverK(Na,Nb,M)) Y : parts (spies evs); \
   725 \           Notes A {|Agent B, Nonce PMS|} : set evs;     \
   726 \           Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   727 \           evs : tls;  A ~: bad;  B ~: bad |]          \
   728 \        ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs";
   729 by (blast_tac (claset() addIs [lemma]
   730                         addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
   731 qed_spec_mp "TrustServerMsg";
   732 
   733 
   734 
   735 (*** Protocol goal: if B receives any message encrypted with clientK
   736      then A has sent it, ASSUMING that A chose PMS.  Authentication is
   737      assumed here; B cannot verify it.  But if the message is
   738      ClientFinished, then B can then check the quoted values PA, PB, etc.
   739 ***)
   740 
   741 goal thy
   742  "!!evs. [| M = PRF(PMS,NA,NB);  evs : tls;  A ~: bad;  B ~: bad |] \
   743 \    ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \
   744 \        Notes A {|Agent B, Nonce PMS|} : set evs -->               \
   745 \        Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) -->         \
   746 \        Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
   747 by (hyp_subst_tac 1);
   748 by (analz_induct_tac 1);	(*15 seconds*)
   749 by (ALLGOALS Clarify_tac);
   750 (*ClientFinished, ClientResume: by unicity of PMS*)
   751 by (REPEAT (blast_tac (claset() delrules [conjI]
   752 		                addSDs [Notes_master_imp_Notes_PMS]
   753 	 	                addDs  [Notes_unique_PMS]) 3));
   754 (*ClientKeyExch: blast_tac gives PROOF FAILED*)
   755 by (fast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]) 2);
   756 (*Fake: the Spy doesn't have the critical session key!*)
   757 by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   758 by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
   759 				      not_parts_not_analz]) 2);
   760 by (Fake_parts_insert_tac 1);
   761 val lemma = normalize_thm [RSmp] (result());
   762 
   763 (*Final version*)
   764 goal thy
   765  "!!evs. [| M = PRF(PMS,NA,NB);                           \
   766 \           Crypt (clientK(Na,Nb,M)) Y : parts (spies evs);  \
   767 \           Notes A {|Agent B, Nonce PMS|} : set evs;        \
   768 \           Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;  \
   769 \           evs : tls;  A ~: bad;  B ~: bad |]                         \
   770 \  ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
   771 by (blast_tac (claset() addIs [lemma]
   772                         addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1);
   773 qed "TrustClientMsg";
   774 
   775 
   776 
   777 (*** Protocol goal: if B receives ClientFinished, and if B is able to
   778      check a CertVerify from A, then A has used the quoted
   779      values PA, PB, etc.  Even this one requires A to be uncompromised.
   780  ***)
   781 goal thy
   782  "!!evs. [| M = PRF(PMS,NA,NB);                           \
   783 \           Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\
   784 \           Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \
   785 \           certificate A KA : parts (spies evs);       \
   786 \           Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\
   787 \             : set evs;                                                  \
   788 \        evs : tls;  A ~: bad;  B ~: bad |]                             \
   789 \     ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
   790 by (blast_tac (claset() addSIs [TrustClientMsg, UseCertVerify]
   791                         addDs  [Says_imp_spies RS parts.Inj]) 1);
   792 qed "AuthClientFinished";
   793 
   794 (*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)
   795 (*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*)
   796 (*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*)
   797 (*30/9/97: loads in 476s, after removing unused theorems*)
   798 (*30/9/97: loads in 448s, after fixing ServerResume*)