src/HOL/Auth/TLS.ML
author wenzelm
Mon Nov 03 12:24:13 1997 +0100 (1997-11-03)
changeset 4091 771b1f6422a8
parent 4006 84a5efc95dcf
child 4201 858b3ec2c9db
permissions -rw-r--r--
isatool fixclasimp;
     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 proof_timing:=true;
    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 br 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 br 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 be 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 2);
   384 (*Base*)
   385 by (Blast_tac 1);
   386 qed_spec_mp "analz_image_priK";
   387 
   388 
   389 (*slightly speeds up the big simplification below*)
   390 goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
   391 by (Blast_tac 1);
   392 val range_sessionkeys_not_priK = result();
   393 
   394 (*Lemma for the trivial direction of the if-and-only-if*)
   395 goal thy  
   396  "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
   397 \        (X : analz (G Un H))  =  (X : analz H)";
   398 by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
   399 val analz_image_keys_lemma = result();
   400 
   401 (** Strangely, the following version doesn't work:
   402 \    ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
   403 \           (Nonce N : analz (spies evs))";
   404 **)
   405 
   406 goal thy  
   407  "!!evs. evs : tls ==>                                    \
   408 \    ALL KK. KK <= range sessionK -->                     \
   409 \            (Nonce N : analz (Key``KK Un (spies evs))) = \
   410 \            (Nonce N : analz (spies evs))";
   411 by (etac tls.induct 1);
   412 by (ClientKeyExch_tac 7);
   413 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   414 by (REPEAT_FIRST (rtac analz_image_keys_lemma));
   415 by (ALLGOALS    (*15 seconds*)
   416     (asm_simp_tac (analz_image_keys_ss 
   417 		   addsimps (expand_ifs@pushes)
   418 		   addsimps [range_sessionkeys_not_priK, 
   419                              analz_image_priK, certificate_def])));
   420 by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
   421 (*Fake*) 
   422 by (spy_analz_tac 2);
   423 (*Base*)
   424 by (Blast_tac 1);
   425 qed_spec_mp "analz_image_keys";
   426 
   427 (*Knowing some session keys is no help in getting new nonces*)
   428 goal thy
   429  "!!evs. evs : tls ==>          \
   430 \        Nonce N : analz (insert (Key (sessionK z)) (spies evs)) =  \
   431 \        (Nonce N : analz (spies evs))";
   432 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1);
   433 qed "analz_insert_key";
   434 Addsimps [analz_insert_key];
   435 
   436 
   437 (*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
   438 
   439 (** Some lemmas about session keys, comprising clientK and serverK **)
   440 
   441 
   442 (*Lemma: session keys are never used if PMS is fresh.  
   443   Nonces don't have to agree, allowing session resumption.
   444   Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
   445   THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
   446 goal thy 
   447  "!!evs. [| Nonce PMS ~: parts (spies evs);  \
   448 \           K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b);  \
   449 \           evs : tls |]             \
   450 \  ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
   451 by (etac rev_mp 1);
   452 by (hyp_subst_tac 1);
   453 by (analz_induct_tac 1);
   454 (*SpyKeys*)
   455 by (blast_tac (claset() addSEs spies_partsEs) 3);
   456 (*Fake*)
   457 by (simp_tac (simpset() addsimps [parts_insert_spies]) 2);
   458 by (Fake_parts_insert_tac 2);
   459 (** LEVEL 6 **)
   460 (*Oops*)
   461 by (fast_tac (claset() addSEs [MPair_parts]
   462 		       addDs  [Says_imp_spies RS parts.Inj]
   463 		       addss (simpset())) 6);
   464 by (REPEAT 
   465     (blast_tac (claset() addSDs [Notes_Crypt_parts_spies, 
   466 				Notes_master_imp_Crypt_PMS]
   467                         addSEs spies_partsEs) 1));
   468 val lemma = result();
   469 
   470 goal thy 
   471  "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   472 \  ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)";
   473 by (blast_tac (claset() addDs [lemma]) 1);
   474 qed "PMS_sessionK_not_spied";
   475 bind_thm ("PMS_sessionK_spiedE", 
   476 	  PMS_sessionK_not_spied RSN (2,rev_notE));
   477 
   478 goal thy 
   479  "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   480 \  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
   481 by (blast_tac (claset() addDs [lemma]) 1);
   482 qed "PMS_Crypt_sessionK_not_spied";
   483 bind_thm ("PMS_Crypt_sessionK_spiedE", 
   484 	  PMS_Crypt_sessionK_not_spied RSN (2,rev_notE));
   485 
   486 (*Lemma: write keys are never sent if M (MASTER SECRET) is secure.  
   487   Converse doesn't hold; betraying M doesn't force the keys to be sent!
   488   The strong Oops condition can be weakened later by unicity reasoning, 
   489 	with some effort.*)
   490 goal thy 
   491  "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
   492 \           Nonce M ~: analz (spies evs);  evs : tls |]   \
   493 \        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
   494 by (etac rev_mp 1);
   495 by (etac rev_mp 1);
   496 by (analz_induct_tac 1);        (*17 seconds*)
   497 (*Oops*)
   498 by (Blast_tac 4);
   499 (*SpyKeys*)
   500 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]) 3);
   501 (*Fake*) 
   502 by (spy_analz_tac 2);
   503 (*Base*)
   504 by (Blast_tac 1);
   505 qed "sessionK_not_spied";
   506 Addsimps [sessionK_not_spied];
   507 
   508 
   509 (*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
   510 goal thy
   511  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
   512 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   513 \            Nonce PMS ~: analz (spies evs)";
   514 by (analz_induct_tac 1);   (*11 seconds*)
   515 (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
   516 by (REPEAT (fast_tac (claset() addss (simpset())) 6));
   517 (*ClientHello, ServerHello, ClientKeyExch, ServerResume: 
   518   mostly freshness reasoning*)
   519 by (REPEAT (blast_tac (claset() addSEs partsEs
   520 			       addDs  [Notes_Crypt_parts_spies,
   521 				       impOfSubs analz_subset_parts,
   522 				       Says_imp_spies RS analz.Inj]) 3));
   523 (*SpyKeys*)
   524 by (fast_tac (claset() addss (simpset())) 2);
   525 (*Fake*)
   526 by (spy_analz_tac 1);
   527 bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
   528 
   529 
   530 (*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
   531   will stay secret.*)
   532 goal thy
   533  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
   534 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   535 \            Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
   536 by (analz_induct_tac 1);   (*13 seconds*)
   537 (*ClientAccepts and ServerAccepts: because PMS was already visible*)
   538 by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS, 
   539 				      Says_imp_spies RS analz.Inj,
   540 				      Notes_imp_spies RS analz.Inj]) 6));
   541 (*ClientHello*)
   542 by (Blast_tac 3);
   543 (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
   544 by (blast_tac (claset() addSDs [Spy_not_see_PMS, 
   545 			       Says_imp_spies RS analz.Inj]) 2);
   546 (*Fake*)
   547 by (spy_analz_tac 1);
   548 (*ServerHello and ClientKeyExch: mostly freshness reasoning*)
   549 by (REPEAT (blast_tac (claset() addSEs partsEs
   550 			       addDs  [Notes_Crypt_parts_spies,
   551 				       impOfSubs analz_subset_parts,
   552 				       Says_imp_spies RS analz.Inj]) 1));
   553 bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
   554 
   555 
   556 (*** Weakening the Oops conditions for leakage of clientK ***)
   557 
   558 (*If A created PMS then nobody other than the Spy would send a message
   559   using a clientK generated from that PMS.*)
   560 goal thy
   561  "!!evs. [| evs : tls;  A' ~= Spy |]                \
   562 \  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   563 \      Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
   564 \      A = A'";
   565 by (analz_induct_tac 1);	(*8 seconds*)
   566 by (ALLGOALS Clarify_tac);
   567 (*ClientFinished, ClientResume: by unicity of PMS*)
   568 by (REPEAT 
   569     (blast_tac (claset() addSDs [Notes_master_imp_Notes_PMS]
   570      	 	        addIs  [Notes_unique_PMS RS conjunct1]) 2));
   571 (*ClientKeyExch*)
   572 by (blast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]
   573 	               addSDs [Says_imp_spies RS parts.Inj]) 1);
   574 bind_thm ("Says_clientK_unique",
   575 	  result() RSN(2,rev_mp) RSN(2,rev_mp));
   576 
   577 
   578 (*If A created PMS and has not leaked her clientK to the Spy, 
   579   then nobody has.*)
   580 goal thy
   581  "!!evs. evs : tls                         \
   582 \  ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
   583 \      Notes A {|Agent B, Nonce PMS|} : set evs -->                   \
   584 \      (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) ";
   585 by (etac tls.induct 1);
   586 (*This roundabout proof sequence avoids looping in simplification*)
   587 by (ALLGOALS Simp_tac);
   588 by (ALLGOALS Clarify_tac);
   589 by (Fake_parts_insert_tac 1);
   590 by (ALLGOALS Asm_simp_tac);
   591 (*Oops*)
   592 by (blast_tac (claset() addIs [Says_clientK_unique]) 2);
   593 (*ClientKeyExch*)
   594 by (blast_tac (claset() addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1);
   595 qed_spec_mp "clientK_Oops_ALL";
   596 
   597 
   598 
   599 (*** Weakening the Oops conditions for leakage of serverK ***)
   600 
   601 (*If A created PMS for B, then nobody other than B or the Spy would
   602   send a message using a serverK generated from that PMS.*)
   603 goal thy
   604  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad;  B' ~= Spy |]                \
   605 \  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   606 \      Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
   607 \      B = B'";
   608 by (analz_induct_tac 1);	(*9 seconds*)
   609 by (ALLGOALS Clarify_tac);
   610 (*ServerResume, ServerFinished: by unicity of PMS*)
   611 by (REPEAT
   612     (blast_tac (claset() addSEs [MPair_parts]
   613 		        addSDs [Notes_master_imp_Crypt_PMS, 
   614 				Says_imp_spies RS parts.Inj]
   615                         addDs  [Spy_not_see_PMS, 
   616 				Notes_Crypt_parts_spies,
   617 				Crypt_unique_PMS]) 2));
   618 (*ClientKeyExch*)
   619 by (blast_tac (claset() addSEs [PMS_Crypt_sessionK_spiedE]
   620 	               addSDs [Says_imp_spies RS parts.Inj]) 1);
   621 bind_thm ("Says_serverK_unique",
   622 	  result() RSN(2,rev_mp) RSN(2,rev_mp));
   623 
   624 (*If A created PMS for B, and B has not leaked his serverK to the Spy, 
   625   then nobody has.*)
   626 goal thy
   627  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                        \
   628 \  ==> Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
   629 \      Notes A {|Agent B, Nonce PMS|} : set evs -->                   \
   630 \      (ALL A. Says A Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) ";
   631 by (etac tls.induct 1);
   632 (*This roundabout proof sequence avoids looping in simplification*)
   633 by (ALLGOALS Simp_tac);
   634 by (ALLGOALS Clarify_tac);
   635 by (Fake_parts_insert_tac 1);
   636 by (ALLGOALS Asm_simp_tac);
   637 (*Oops*)
   638 by (blast_tac (claset() addIs [Says_serverK_unique]) 2);
   639 (*ClientKeyExch*)
   640 by (blast_tac (claset() addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1);
   641 qed_spec_mp "serverK_Oops_ALL";
   642 
   643 
   644 
   645 (*** Protocol goals: if A receives ServerFinished, then B is present 
   646      and has used the quoted values PA, PB, etc.  Note that it is up to A
   647      to compare PA with what she originally sent.
   648 ***)
   649 
   650 (*The mention of her name (A) in X assures A that B knows who she is.*)
   651 goal thy
   652  "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
   653 \                 (Hash{|Number SID, Nonce M,             \
   654 \                        Nonce Na, Number PA, Agent A,    \
   655 \                        Nonce Nb, Number PB, Agent B|}); \
   656 \           M = PRF(PMS,NA,NB);                           \
   657 \           evs : tls;  A ~: bad;  B ~: bad |]            \
   658 \        ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \
   659 \            Notes A {|Agent B, Nonce PMS|} : set evs --> \
   660 \            X : parts (spies evs) --> Says B A X : set evs";
   661 by (hyp_subst_tac 1);
   662 by (analz_induct_tac 1);        (*22 seconds*)
   663 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   664 (*proves ServerResume*)
   665 by (ALLGOALS Clarify_tac);
   666 (*ClientKeyExch*)
   667 by (fast_tac  (*blast_tac gives PROOF FAILED*)
   668     (claset() addSEs [PMS_Crypt_sessionK_spiedE]) 2);
   669 (*Fake: the Spy doesn't have the critical session key!*)
   670 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   671 by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
   672 				     not_parts_not_analz]) 2);
   673 by (Fake_parts_insert_tac 1);
   674 val lemma = normalize_thm [RSmp] (result());
   675 
   676 (*Final version*)
   677 goal thy
   678  "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
   679 \                 (Hash{|Number SID, Nonce M,             \
   680 \                        Nonce Na, Number PA, Agent A,    \
   681 \                        Nonce Nb, Number PB, Agent B|}); \
   682 \           M = PRF(PMS,NA,NB);                           \
   683 \           X : parts (spies evs);                        \
   684 \           Notes A {|Agent B, Nonce PMS|} : set evs;     \
   685 \           Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   686 \           evs : tls;  A ~: bad;  B ~: bad |]          \
   687 \        ==> Says B A X : set evs";
   688 by (blast_tac (claset() addIs [lemma]
   689                        addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
   690 qed_spec_mp "TrustServerFinished";
   691 
   692 
   693 
   694 (*This version refers not to ServerFinished but to any message from B.
   695   We don't assume B has received CertVerify, and an intruder could
   696   have changed A's identity in all other messages, so we can't be sure
   697   that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   698   to bind A's identity with PMS, then we could replace A' by A below.*)
   699 goal thy
   700  "!!evs. [| M = PRF(PMS,NA,NB);  evs : tls;  A ~: bad;  B ~: bad |]     \
   701 \        ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \
   702 \            Notes A {|Agent B, Nonce PMS|} : set evs -->              \
   703 \            Crypt (serverK(Na,Nb,M)) Y : parts (spies evs)  -->  \
   704 \            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
   705 by (hyp_subst_tac 1);
   706 by (analz_induct_tac 1);	(*20 seconds*)
   707 by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
   708 by (ALLGOALS Clarify_tac);
   709 (*ServerResume, ServerFinished: by unicity of PMS*)
   710 by (REPEAT
   711     (blast_tac (claset() addSEs [MPair_parts]
   712 		        addSDs [Notes_master_imp_Crypt_PMS, 
   713 				Says_imp_spies RS parts.Inj]
   714                         addDs  [Spy_not_see_PMS, 
   715 				Notes_Crypt_parts_spies,
   716 				Crypt_unique_PMS]) 3));
   717 (*ClientKeyExch*)
   718 by (blast_tac
   719     (claset() addSEs [PMS_Crypt_sessionK_spiedE]) 2);
   720 (*Fake: the Spy doesn't have the critical session key!*)
   721 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   722 by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
   723 				     not_parts_not_analz]) 2);
   724 by (Fake_parts_insert_tac 1);
   725 val lemma = normalize_thm [RSmp] (result());
   726 
   727 (*Final version*)
   728 goal thy
   729  "!!evs. [| M = PRF(PMS,NA,NB);                           \
   730 \           Crypt (serverK(Na,Nb,M)) Y : parts (spies evs); \
   731 \           Notes A {|Agent B, Nonce PMS|} : set evs;     \
   732 \           Says B Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   733 \           evs : tls;  A ~: bad;  B ~: bad |]          \
   734 \        ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs";
   735 by (blast_tac (claset() addIs [lemma]
   736                        addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
   737 qed_spec_mp "TrustServerMsg";
   738 
   739 
   740 
   741 (*** Protocol goal: if B receives any message encrypted with clientK
   742      then A has sent it, ASSUMING that A chose PMS.  Authentication is
   743      assumed here; B cannot verify it.  But if the message is
   744      ClientFinished, then B can then check the quoted values PA, PB, etc.
   745 ***)
   746 
   747 goal thy
   748  "!!evs. [| M = PRF(PMS,NA,NB);  evs : tls;  A ~: bad;  B ~: bad |] \
   749 \    ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \
   750 \        Notes A {|Agent B, Nonce PMS|} : set evs -->               \
   751 \        Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) -->         \
   752 \        Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
   753 by (hyp_subst_tac 1);
   754 by (analz_induct_tac 1);	(*15 seconds*)
   755 by (ALLGOALS Clarify_tac);
   756 (*ClientFinished, ClientResume: by unicity of PMS*)
   757 by (REPEAT (blast_tac (claset() delrules [conjI]
   758 		               addSDs [Notes_master_imp_Notes_PMS]
   759 	 	               addDs  [Notes_unique_PMS]) 3));
   760 (*ClientKeyExch*)
   761 by (fast_tac  (*blast_tac gives PROOF FAILED*)
   762     (claset() addSEs [PMS_Crypt_sessionK_spiedE]) 2);
   763 (*Fake: the Spy doesn't have the critical session key!*)
   764 by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   765 by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
   766 				     not_parts_not_analz]) 2);
   767 by (Fake_parts_insert_tac 1);
   768 val lemma = normalize_thm [RSmp] (result());
   769 
   770 (*Final version*)
   771 goal thy
   772  "!!evs. [| M = PRF(PMS,NA,NB);                           \
   773 \           Crypt (clientK(Na,Nb,M)) Y : parts (spies evs);  \
   774 \           Notes A {|Agent B, Nonce PMS|} : set evs;        \
   775 \           Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;  \
   776 \           evs : tls;  A ~: bad;  B ~: bad |]                         \
   777 \  ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
   778 by (blast_tac (claset() addIs [lemma]
   779                        addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1);
   780 qed "TrustClientMsg";
   781 
   782 
   783 
   784 (*** Protocol goal: if B receives ClientFinished, and if B is able to
   785      check a CertVerify from A, then A has used the quoted
   786      values PA, PB, etc.  Even this one requires A to be uncompromised.
   787  ***)
   788 goal thy
   789  "!!evs. [| M = PRF(PMS,NA,NB);                           \
   790 \           Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\
   791 \           Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \
   792 \           certificate A KA : parts (spies evs);       \
   793 \           Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\
   794 \             : set evs;                                                  \
   795 \        evs : tls;  A ~: bad;  B ~: bad |]                             \
   796 \     ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
   797 by (blast_tac (claset() addSIs [TrustClientMsg, UseCertVerify]
   798                        addDs  [Says_imp_spies RS parts.Inj]) 1);
   799 qed "AuthClientFinished";
   800 
   801 (*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)
   802 (*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*)
   803 (*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*)
   804 (*30/9/97: loads in 476s, after removing unused theorems*)
   805 (*30/9/97: loads in 448s, after fixing ServerResume*)