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