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