src/HOL/Auth/TLS.ML
author paulson
Mon Sep 22 13:17:29 1997 +0200 (1997-09-22)
changeset 3687 fb7d096d7884
parent 3686 4b484805b4c4
child 3704 2f99d7a0dccc
permissions -rw-r--r--
Simplified SpyKeys to use sessionK instead of clientK and serverK
Proved and used analz_insert_key, shortening scripts
     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 open TLS;
    21 
    22 proof_timing:=true;
    23 HOL_quantifiers := false;
    24 
    25 (** We mostly DO NOT unfold the definition of "certificate".  The attached
    26     lemmas unfold it lazily, when "certificate B KB" occurs in appropriate
    27     contexts.
    28 **)
    29 
    30 goalw thy [certificate_def] 
    31     "parts (insert (certificate B KB) H) =  \
    32 \    parts (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
    33 by (rtac refl 1);
    34 qed "parts_insert_certificate";
    35 
    36 goalw thy [certificate_def] 
    37     "analz (insert (certificate B KB) H) =  \
    38 \    analz (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
    39 by (rtac refl 1);
    40 qed "analz_insert_certificate";
    41 Addsimps [parts_insert_certificate, analz_insert_certificate];
    42 
    43 goalw thy [certificate_def] 
    44     "(X = certificate B KB) = (Crypt (priK Server) {|Agent B, Key KB|} = X)";
    45 by (Blast_tac 1);
    46 qed "eq_certificate_iff";
    47 AddIffs [eq_certificate_iff];
    48 
    49 
    50 (*Injectiveness of key-generating functions*)
    51 AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq];
    52 
    53 (* invKey(sessionK x) = sessionK x*)
    54 Addsimps [isSym_sessionK, rewrite_rule [isSymKey_def] isSym_sessionK];
    55 
    56 
    57 (*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
    58 
    59 goal thy "pubK A ~= sessionK arg";
    60 br notI 1;
    61 by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    62 by (Full_simp_tac 1);
    63 qed "pubK_neq_sessionK";
    64 
    65 goal thy "priK A ~= sessionK arg";
    66 br notI 1;
    67 by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    68 by (Full_simp_tac 1);
    69 qed "priK_neq_sessionK";
    70 
    71 val keys_distinct = [pubK_neq_sessionK, priK_neq_sessionK];
    72 AddIffs (keys_distinct @ (keys_distinct RL [not_sym]));
    73 
    74 
    75 (**** Protocol Proofs ****)
    76 
    77 (*A "possibility property": there are traces that reach the end.
    78   This protocol has three end points and six messages to consider.*)
    79 
    80 
    81 (** These proofs make the further assumption that the Nonce_supply nonces 
    82 	(which have the form  @ N. Nonce N ~: used evs)
    83     lie outside the range of PRF.  This assumption seems reasonable, but
    84     as it is needed only for the possibility theorems, it is not taken
    85     as an axiom.
    86 **)
    87 
    88 
    89 (*Possibility property ending with ClientAccepts.*)
    90 goal thy 
    91  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    92 \           A ~= B |] ==> EX SID M. EX evs: tls.    \
    93 \  Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
    94 by (REPEAT (resolve_tac [exI,bexI] 1));
    95 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    96 	RS tls.ClientFinished RS tls.ServerFinished RS tls.ClientAccepts) 2);
    97 by possibility_tac;
    98 by (REPEAT (Blast_tac 1));
    99 result();
   100 
   101 (*And one for ServerAccepts.  Either FINISHED message may come first.*)
   102 goal thy 
   103  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
   104 \           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
   105 \  Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
   106 by (REPEAT (resolve_tac [exI,bexI] 1));
   107 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
   108 	  RS tls.ServerFinished RS tls.ClientFinished RS tls.ServerAccepts) 2);
   109 by possibility_tac;
   110 by (REPEAT (Blast_tac 1));
   111 result();
   112 
   113 (*Another one, for CertVerify (which is optional)*)
   114 goal thy 
   115  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
   116 \           A ~= B |] ==> EX NB PMS. EX evs: tls.   \
   117 \  Says A B (Crypt (priK A)                 \
   118 \            (Hash{|Nonce NB, certificate B (pubK 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 XA NB XB. EX evs: tls.    \
   133 \  Says A B (Crypt (clientK(NA,NB,M))                           \
   134 \            (Hash{|Nonce M, Number SID,             \
   135 \                   Nonce NA, Number XA, Agent A,      \
   136 \                   Nonce NB, Number XB, 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_full_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 (*Fake*)
   256 by (blast_tac (!claset addIs [parts_insertI]) 1);
   257 (*Client, Server Accept*)
   258 by (Step_tac 1);
   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)                                        \
   304 \                 (Hash{|Nonce NB, certificate B KB, Nonce PMS|});      \
   305 \           evs : tls;  A ~: bad;  B ~= Spy |]                       \
   306 \    ==> Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
   307 \          : set evs --> \
   308 \        X : parts (spies evs) --> Says A B X : set evs";
   309 by (hyp_subst_tac 1);
   310 by (parts_induct_tac 1);
   311 by (Fake_parts_insert_tac 1);
   312 (*ServerHello: nonce NB cannot be in X because it's fresh!*)
   313 by (blast_tac (!claset addSDs [Hash_Nonce_CV]
   314 	               addSEs spies_partsEs) 1);
   315 qed_spec_mp "TrustCertVerify";
   316 
   317 
   318 (*If CertVerify is present then A has chosen PMS.*)
   319 goal thy
   320  "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|})  \
   321 \             : parts (spies evs);                                \
   322 \           evs : tls;  A ~: bad |]                                      \
   323 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
   324 be rev_mp 1;
   325 by (parts_induct_tac 1);
   326 by (Fake_parts_insert_tac 1);
   327 qed "UseCertVerify";
   328 
   329 
   330 (*Key compromise lemma needed to prove analz_image_keys.
   331   No collection of keys can help the spy get new private keys.*)
   332 goal thy  
   333  "!!evs. evs : tls ==>                                    \
   334 \  ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) =  \
   335 \          (priK B : KK | B : bad)";
   336 by (etac tls.induct 1);
   337 by (ALLGOALS
   338     (asm_simp_tac (analz_image_keys_ss
   339 		   addsimps (analz_insert_certificate::keys_distinct))));
   340 (*Fake*) 
   341 by (spy_analz_tac 2);
   342 (*Base*)
   343 by (Blast_tac 1);
   344 qed_spec_mp "analz_image_priK";
   345 
   346 
   347 (*Lemma for the trivial direction of the if-and-only-if*)
   348 goal thy  
   349  "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
   350 \        (X : analz (G Un H))  =  (X : analz H)";
   351 by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
   352 val lemma = result();
   353 
   354 (*slightly speeds up the big simplification below*)
   355 goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
   356 by (Blast_tac 1);
   357 val range_sessionkeys_not_priK = result();
   358 
   359 (** It is a mystery to me why the following formulation is actually slower
   360     in simplification:
   361 
   362 \    ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
   363 \           (Nonce N : analz (spies evs))";
   364 
   365 More so as it can take advantage of unconditional rewrites such as 
   366      priK B ~: sessionK``Z
   367 **)
   368 
   369 goal thy  
   370  "!!evs. evs : tls ==>                                 \
   371 \    ALL KK. KK <= range sessionK -->           \
   372 \            (Nonce N : analz (Key``KK Un (spies evs))) = \
   373 \            (Nonce N : analz (spies evs))";
   374 by (etac tls.induct 1);
   375 by (ClientCertKeyEx_tac 6);
   376 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   377 by (REPEAT_FIRST (rtac lemma));
   378 writeln"SLOW simplification: 55 secs??";
   379 (*ClientCertKeyEx is to blame, causing case splits for A, B: bad*)
   380 by (ALLGOALS
   381     (asm_simp_tac (analz_image_keys_ss 
   382 		   addsimps [range_sessionkeys_not_priK, 
   383 			     analz_image_priK, analz_insert_certificate])));
   384 by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
   385 (*Fake*) 
   386 by (spy_analz_tac 2);
   387 (*Base*)
   388 by (Blast_tac 1);
   389 qed_spec_mp "analz_image_keys";
   390 
   391 (*Knowing some session keys is no help in getting new nonces*)
   392 goal thy
   393  "!!evs. evs : tls ==>          \
   394 \        Nonce N : analz (insert (Key (sessionK z)) (spies evs)) =  \
   395 \        (Nonce N : analz (spies evs))";
   396 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1);
   397 qed "analz_insert_key";
   398 Addsimps [analz_insert_key];
   399 
   400 goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
   401 by (parts_induct_tac 1);
   402 (*ClientCertKeyEx: PMS is assumed to differ from any PRF.*)
   403 by (Blast_tac 1);
   404 qed "no_Notes_A_PRF";
   405 Addsimps [no_Notes_A_PRF];
   406 
   407 
   408 goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (spies evs);  \
   409 \                   evs : tls |]  \
   410 \                ==> Nonce PMS : parts (spies evs)";
   411 by (etac rev_mp 1);
   412 by (parts_induct_tac 1);
   413 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies])));
   414 by (Fake_parts_insert_tac 1);
   415 (*Six others, all trivial or by freshness*)
   416 by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
   417                                addSEs spies_partsEs) 1));
   418 qed "MS_imp_PMS";
   419 AddSDs [MS_imp_PMS];
   420 
   421 
   422 
   423 (*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
   424 
   425 (** Some lemmas about session keys, comprising clientK and serverK **)
   426 
   427 (*Lemma: those write keys are never sent if M (MASTER SECRET) is secure.  
   428   Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
   429 
   430 goal thy 
   431  "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
   432 \           Nonce M ~: analz (spies evs);  evs : tls |]   \
   433 \        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
   434 by (etac rev_mp 1);
   435 by (etac rev_mp 1);
   436 by (analz_induct_tac 1);	(*30 seconds??*)
   437 (*Oops*)
   438 by (Blast_tac 4);
   439 (*SpyKeys*)
   440 by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
   441 (*Fake*) 
   442 by (spy_analz_tac 2);
   443 (*Base*)
   444 by (Blast_tac 1);
   445 qed "sessionK_notin_parts";
   446 bind_thm ("sessionK_in_partsE", sessionK_notin_parts RSN (2, rev_notE));
   447 
   448 Addsimps [sessionK_notin_parts];
   449 AddSEs [sessionK_in_partsE, 
   450 	impOfSubs analz_subset_parts RS sessionK_in_partsE];
   451 
   452 
   453 (*Lemma: session keys are never used if PMS is fresh.  
   454   Nonces don't have to agree, allowing session resumption.
   455   Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
   456   They are NOT suitable as safe elim rules.*)
   457 
   458 goal thy 
   459  "!!evs. [| ALL A. Says A Spy (Key (sessionK((Na, Nb, PRF(PMS,NA,NB)),b))) \
   460 \                    ~: set evs; \
   461 \           Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   462 \  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
   463 by (etac rev_mp 1);
   464 by (etac rev_mp 1);
   465 by (analz_induct_tac 1);
   466 (*Fake*)
   467 by (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies]) 2);
   468 by (Fake_parts_insert_tac 2);
   469 (*Base, ClientFinished, ServerFinished, ClientResume: 
   470   trivial, e.g. by freshness*)
   471 by (REPEAT 
   472     (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, 
   473 				Notes_master_imp_Crypt_PMS]
   474                         addSEs spies_partsEs) 1));
   475 qed "Crypt_sessionK_notin_parts";
   476 
   477 Addsimps [Crypt_sessionK_notin_parts];
   478 AddEs [Crypt_sessionK_notin_parts RSN (2, rev_notE)];
   479 
   480 
   481 (*NEEDED??*)
   482 goal thy
   483  "!!evs. [| Says A B {|certA, Crypt KB (Nonce M)|} : set evs;   \
   484 \           A ~= Spy;  evs : tls |] ==> KB = pubK B";
   485 be rev_mp 1;
   486 by (analz_induct_tac 1);
   487 qed "A_Crypt_pubB";
   488 
   489 
   490 (*** Unicity results for PMS, the pre-master-secret ***)
   491 
   492 (*PMS determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
   493 goal thy 
   494  "!!evs. [| Nonce PMS ~: analz (spies evs);  evs : tls |]   \
   495 \        ==> EX B'. ALL B.   \
   496 \              Crypt (pubK B) (Nonce PMS) : parts (spies evs) --> B=B'";
   497 by (etac rev_mp 1);
   498 by (parts_induct_tac 1);
   499 by (Fake_parts_insert_tac 1);
   500 (*ClientCertKeyEx*)
   501 by (ClientCertKeyEx_tac 1);
   502 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   503 by (expand_case_tac "PMS = ?y" 1 THEN
   504     blast_tac (!claset addSEs partsEs) 1);
   505 val lemma = result();
   506 
   507 goal thy 
   508  "!!evs. [| Crypt(pubK B)  (Nonce PMS) : parts (spies evs); \
   509 \           Crypt(pubK B') (Nonce PMS) : parts (spies evs); \
   510 \           Nonce PMS ~: analz (spies evs);                 \
   511 \           evs : tls |]                                          \
   512 \        ==> B=B'";
   513 by (prove_unique_tac lemma 1);
   514 qed "unique_PMS";
   515 
   516 (** It is frustrating that we need two versions of the unicity results.
   517     But Notes A {|Agent B, Nonce PMS|} determines both A and B, while
   518     Crypt(pubK B) (Nonce PMS) determines only B, and sometimes only
   519     this weaker item is available.
   520 **)
   521 
   522 (*In A's internal Note, PMS determines A and B.*)
   523 goal thy 
   524  "!!evs. [| Nonce PMS ~: analz (spies evs);  evs : tls |]            \
   525 \ ==> EX A' B'. ALL A B.                                                   \
   526 \        Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
   527 by (etac rev_mp 1);
   528 by (parts_induct_tac 1);
   529 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   530 (*ClientCertKeyEx: if PMS is fresh, then it can't appear in Notes A X.*)
   531 by (expand_case_tac "PMS = ?y" 1 THEN
   532     blast_tac (!claset addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1);
   533 val lemma = result();
   534 
   535 goal thy 
   536  "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
   537 \           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
   538 \           Nonce PMS ~: analz (spies evs);      \
   539 \           evs : tls |]                               \
   540 \        ==> A=A' & B=B'";
   541 by (prove_unique_tac lemma 1);
   542 qed "Notes_unique_PMS";
   543 
   544 
   545 
   546 (*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
   547 goal thy
   548  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
   549 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   550 \            Nonce PMS ~: analz (spies evs)";
   551 by (analz_induct_tac 1);   (*30 seconds??*)
   552 (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
   553 by (EVERY (map (fast_tac (!claset addss (!simpset))) [7,6]));
   554 (*ClientHello, ServerHello, ClientCertKeyEx, ServerResume: 
   555   mostly freshness reasoning*)
   556 by (REPEAT (blast_tac (!claset addSEs partsEs
   557 			       addDs  [Notes_Crypt_parts_spies,
   558 				       impOfSubs analz_subset_parts,
   559 				       Says_imp_spies RS analz.Inj]) 3));
   560 (*SpyKeys*)
   561 by (fast_tac (!claset addss (!simpset)) 2);
   562 (*Fake*)
   563 by (spy_analz_tac 1);
   564 bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
   565 
   566 
   567 (*Another way of showing unicity*)
   568 goal thy 
   569  "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
   570 \           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
   571 \           A ~: bad;  B ~: bad;                         \
   572 \           evs : tls |]                                 \
   573 \        ==> A=A' & B=B'";
   574 by (REPEAT (ares_tac [Notes_unique_PMS, Spy_not_see_PMS] 1));
   575 qed "good_Notes_unique_PMS";
   576 
   577 
   578 (*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
   579   will stay secret.*)
   580 goal thy
   581  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
   582 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   583 \            Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
   584 by (analz_induct_tac 1);   (*35 seconds*)
   585 (*ClientAccepts and ServerAccepts: because PMS was already visible*)
   586 by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS, 
   587 				      Says_imp_spies RS analz.Inj,
   588 				      Notes_imp_spies RS analz.Inj]) 6));
   589 (*ClientHello*)
   590 by (Blast_tac 3);
   591 (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
   592 by (blast_tac (!claset addSDs [Spy_not_see_PMS, 
   593 			       Says_imp_spies RS analz.Inj]) 2);
   594 (*Fake*)
   595 by (spy_analz_tac 1);
   596 (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   597 by (REPEAT (blast_tac (!claset addSEs partsEs
   598 			       addDs  [Notes_Crypt_parts_spies,
   599 				       impOfSubs analz_subset_parts,
   600 				       Says_imp_spies RS analz.Inj]) 1));
   601 bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
   602 
   603 
   604 (*** Protocol goals: if A receives ServerFinished, then B is present 
   605      and has used the quoted values XA, XB, etc.  Note that it is up to A
   606      to compare XA with what she originally sent.
   607 ***)
   608 
   609 (*The mention of her name (A) in X assures A that B knows who she is.*)
   610 goal thy
   611  "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   612 \           X = Crypt (serverK(Na,Nb,M))                  \
   613 \                 (Hash{|Nonce M, Number SID,             \
   614 \                        Nonce NA, Number XA, Agent A,    \
   615 \                        Nonce NB, Number XB, Agent B|}); \
   616 \           M = PRF(PMS,NA,NB);                           \
   617 \           evs : tls;  A ~: bad;  B ~: bad |]          \
   618 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
   619 \        X : parts (spies evs) --> Says B A X : set evs";
   620 by (etac rev_mp 1);
   621 by (hyp_subst_tac 1);
   622 by (analz_induct_tac 1);	(*16 seconds*)
   623 (*ServerResume is trivial, but Blast_tac is too slow*)
   624 by (Best_tac 3);
   625 (*ClientCertKeyEx*)
   626 by (Blast_tac 2);
   627 (*Fake: the Spy doesn't have the critical session key!*)
   628 by (REPEAT (rtac impI 1));
   629 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   630 by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   631 				     not_parts_not_analz]) 2);
   632 by (Fake_parts_insert_tac 1);
   633 qed_spec_mp "TrustServerFinished";
   634 
   635 
   636 (*This version refers not to ServerFinished but to any message from B.
   637   We don't assume B has received CertVerify, and an intruder could
   638   have changed A's identity in all other messages, so we can't be sure
   639   that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   640   to bind A's identity with M, then we could replace A' by A below.*)
   641 goal thy
   642  "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   643 \           evs : tls;  A ~: bad;  B ~: bad;                 \
   644 \           M = PRF(PMS,NA,NB) |]            \
   645 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->              \
   646 \            Crypt (serverK(Na,Nb,M)) Y : parts (spies evs)  -->  \
   647 \            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
   648 by (etac rev_mp 1);
   649 by (hyp_subst_tac 1);
   650 by (analz_induct_tac 1);	(*20 seconds*)
   651 by (REPEAT_FIRST (rtac impI));
   652 (*ServerResume, by unicity of PMS*)
   653 by (blast_tac (!claset addSEs [MPair_parts]
   654 		       addDs  [Spy_not_see_PMS, 
   655 			       Notes_Crypt_parts_spies,
   656 			       Notes_master_imp_Crypt_PMS, unique_PMS]) 4);
   657 (*ServerFinished, by unicity of PMS (10 seconds)*)
   658 by (blast_tac (!claset addSEs [MPair_parts]
   659 		       addDs  [Spy_not_see_PMS, 
   660 			       Notes_Crypt_parts_spies,
   661 			       Says_imp_spies RS parts.Inj,
   662 			       unique_PMS]) 3);
   663 (*ClientCertKeyEx*)
   664 by (Blast_tac 2);
   665 (*Fake: the Spy doesn't have the critical session key!*)
   666 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   667 by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   668 				     not_parts_not_analz]) 2);
   669 by (Fake_parts_insert_tac 1);
   670 qed_spec_mp "TrustServerMsg";
   671 
   672 
   673 (*** Protocol goal: if B receives any message encrypted with clientK
   674      then A has sent it, ASSUMING that A chose PMS.  Authentication is
   675      assumed here; B cannot verify it.  But if the message is
   676      ClientFinished, then B can then check the quoted values XA, XB, etc.
   677 ***)
   678 goal thy
   679  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                         \
   680 \  ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) -->\
   681 \      Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   682 \      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) -->  \
   683 \      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   684 by (analz_induct_tac 1);	(*23 seconds*)
   685 by (REPEAT_FIRST (rtac impI));
   686 (*ClientResume: by unicity of PMS*)
   687 by (blast_tac (!claset delrules [conjI]
   688 		       addSEs [MPair_parts]
   689                        addSDs [Notes_master_imp_Notes_PMS]
   690 	 	       addDs  [good_Notes_unique_PMS]) 4);
   691 (*ClientFinished: by unicity of PMS*)
   692 by (blast_tac (!claset delrules [conjI]
   693 		       addSEs [MPair_parts]
   694 		       addDs  [good_Notes_unique_PMS]) 3);
   695 (*ClientCertKeyEx*)
   696 by (Blast_tac 2);
   697 (*Fake: the Spy doesn't have the critical session key!*)
   698 by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   699 by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   700 				     not_parts_not_analz]) 2);
   701 by (Fake_parts_insert_tac 1);
   702 qed_spec_mp "TrustClientMsg";
   703 
   704 
   705 
   706 (*** Protocol goal: if B receives ClientFinished, and if B is able to
   707      check a CertVerify from A, then A has used the quoted
   708      values XA, XB, etc.  Even this one requires A to be uncompromised.
   709  ***)
   710 goal thy
   711  "!!evs. [| ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
   712 \           Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
   713 \           Says B  A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
   714 \             : set evs;                                                  \
   715 \           Says A'' B (Crypt (priK A)                                    \
   716 \                       (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))  \
   717 \             : set evs;                                                  \
   718 \        evs : tls;  A ~: bad;  B ~: bad |]                             \
   719 \     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   720 by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
   721                        addDs  [Says_imp_spies RS parts.Inj]) 1);
   722 qed "AuthClientFinished";
   723 
   724 (*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)