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