src/HOL/Auth/TLS.ML
author paulson
Fri Sep 19 18:27:31 1997 +0200 (1997-09-19)
changeset 3686 4b484805b4c4
parent 3685 5b8c0c8f576e
child 3687 fb7d096d7884
permissions -rw-r--r--
First working version with Oops event for session keys
     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 (*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 (*Knowing some session keys is no help in getting new nonces*)
   359 goal thy  
   360  "!!evs. evs : tls ==>                                 \
   361 \    ALL KK. KK <= range sessionK -->           \
   362 \            (Nonce N : analz (Key``KK Un (spies evs))) = \
   363 \            (Nonce N : analz (spies evs))";
   364 by (etac tls.induct 1);
   365 by (ClientCertKeyEx_tac 6);
   366 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   367 by (REPEAT_FIRST (rtac lemma));
   368 writeln"SLOW simplification: 55 secs??";
   369 (*ClientCertKeyEx is to blame, causing case splits for A, B: bad*)
   370 by (ALLGOALS
   371     (asm_simp_tac (analz_image_keys_ss 
   372 		   addsimps [range_sessionkeys_not_priK, 
   373 			     analz_image_priK, analz_insert_certificate])));
   374 by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
   375 (*Fake*) 
   376 by (spy_analz_tac 2);
   377 (*Base*)
   378 by (Blast_tac 1);
   379 qed_spec_mp "analz_image_keys";
   380 
   381 
   382 goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
   383 by (parts_induct_tac 1);
   384 (*ClientCertKeyEx: PMS is assumed to differ from any PRF.*)
   385 by (Blast_tac 1);
   386 qed "no_Notes_A_PRF";
   387 Addsimps [no_Notes_A_PRF];
   388 
   389 
   390 goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (spies evs);  \
   391 \                   evs : tls |]  \
   392 \                ==> Nonce PMS : parts (spies evs)";
   393 by (etac rev_mp 1);
   394 by (parts_induct_tac 1);
   395 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_spies])));
   396 by (Fake_parts_insert_tac 1);
   397 (*Six others, all trivial or by freshness*)
   398 by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
   399                                addSEs spies_partsEs) 1));
   400 qed "MS_imp_PMS";
   401 AddSDs [MS_imp_PMS];
   402 
   403 
   404 
   405 (*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
   406 
   407 (** Some lemmas about session keys, comprising clientK and serverK **)
   408 
   409 (*Lemma: those write keys are never sent if M (MASTER SECRET) is secure.  
   410   Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
   411 
   412 goal thy 
   413  "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
   414 \           Nonce M ~: analz (spies evs);  evs : tls |]   \
   415 \        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
   416 by (etac rev_mp 1);
   417 by (etac rev_mp 1);
   418 by (analz_induct_tac 1);	(*30 seconds??*)
   419 (*Oops*)
   420 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 4);
   421 by (Blast_tac 4);
   422 (*SpyKeys*)
   423 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
   424 by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
   425 (*Fake*) 
   426 by (spy_analz_tac 2);
   427 (*Base*)
   428 by (Blast_tac 1);
   429 qed "sessionK_notin_parts";
   430 bind_thm ("sessionK_in_partsE", sessionK_notin_parts RSN (2, rev_notE));
   431 
   432 Addsimps [sessionK_notin_parts];
   433 AddSEs [sessionK_in_partsE, 
   434 	impOfSubs analz_subset_parts RS sessionK_in_partsE];
   435 
   436 
   437 (*Lemma: session keys are never used if PMS is fresh.  
   438   Nonces don't have to agree, allowing session resumption.
   439   Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
   440   They are NOT suitable as safe elim rules.*)
   441 
   442 goal thy 
   443  "!!evs. [| ALL A. Says A Spy (Key (sessionK((Na, Nb, PRF(PMS,NA,NB)),b))) \
   444 \                    ~: set evs; \
   445 \           Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   446 \  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
   447 by (etac rev_mp 1);
   448 by (etac rev_mp 1);
   449 by (analz_induct_tac 1);
   450 (*Fake*)
   451 by (asm_simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_spies]) 2);
   452 by (Fake_parts_insert_tac 2);
   453 (*Base, ClientFinished, ServerFinished, ClientResume: 
   454   trivial, e.g. by freshness*)
   455 by (REPEAT 
   456     (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, 
   457 				Notes_master_imp_Crypt_PMS]
   458                         addSEs spies_partsEs) 1));
   459 qed "Crypt_sessionK_notin_parts";
   460 
   461 Addsimps [Crypt_sessionK_notin_parts];
   462 AddEs [Crypt_sessionK_notin_parts RSN (2, rev_notE)];
   463 
   464 
   465 (*NEEDED??*)
   466 goal thy
   467  "!!evs. [| Says A B {|certA, Crypt KB (Nonce M)|} : set evs;   \
   468 \           A ~= Spy;  evs : tls |] ==> KB = pubK B";
   469 be rev_mp 1;
   470 by (analz_induct_tac 1);
   471 qed "A_Crypt_pubB";
   472 
   473 
   474 (*** Unicity results for PMS, the pre-master-secret ***)
   475 
   476 (*PMS determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
   477 goal thy 
   478  "!!evs. [| Nonce PMS ~: analz (spies evs);  evs : tls |]   \
   479 \        ==> EX B'. ALL B.   \
   480 \              Crypt (pubK B) (Nonce PMS) : parts (spies evs) --> B=B'";
   481 by (etac rev_mp 1);
   482 by (parts_induct_tac 1);
   483 by (Fake_parts_insert_tac 1);
   484 (*ClientCertKeyEx*)
   485 by (ClientCertKeyEx_tac 1);
   486 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   487 by (expand_case_tac "PMS = ?y" 1 THEN
   488     blast_tac (!claset addSEs partsEs) 1);
   489 val lemma = result();
   490 
   491 goal thy 
   492  "!!evs. [| Crypt(pubK B)  (Nonce PMS) : parts (spies evs); \
   493 \           Crypt(pubK B') (Nonce PMS) : parts (spies evs); \
   494 \           Nonce PMS ~: analz (spies evs);                 \
   495 \           evs : tls |]                                          \
   496 \        ==> B=B'";
   497 by (prove_unique_tac lemma 1);
   498 qed "unique_PMS";
   499 
   500 (** It is frustrating that we need two versions of the unicity results.
   501     But Notes A {|Agent B, Nonce PMS|} determines both A and B, while
   502     Crypt(pubK B) (Nonce PMS) determines only B, and sometimes only
   503     this weaker item is available.
   504 **)
   505 
   506 (*In A's internal Note, PMS determines A and B.*)
   507 goal thy 
   508  "!!evs. [| Nonce PMS ~: analz (spies evs);  evs : tls |]            \
   509 \ ==> EX A' B'. ALL A B.                                                   \
   510 \        Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
   511 by (etac rev_mp 1);
   512 by (parts_induct_tac 1);
   513 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   514 (*ClientCertKeyEx: if PMS is fresh, then it can't appear in Notes A X.*)
   515 by (expand_case_tac "PMS = ?y" 1 THEN
   516     blast_tac (!claset addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1);
   517 val lemma = result();
   518 
   519 goal thy 
   520  "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
   521 \           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
   522 \           Nonce PMS ~: analz (spies evs);      \
   523 \           evs : tls |]                               \
   524 \        ==> A=A' & B=B'";
   525 by (prove_unique_tac lemma 1);
   526 qed "Notes_unique_PMS";
   527 
   528 
   529 
   530 (*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
   531 goal thy
   532  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
   533 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   534 \            Nonce PMS ~: analz (spies evs)";
   535 by (analz_induct_tac 1);   (*30 seconds??*)
   536 (*oops*)
   537 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 9);
   538 (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
   539 by (EVERY (map (fast_tac (!claset addss (!simpset))) [7,6]));
   540 (*ServerHello, ClientCertKeyEx, ServerResume: mostly freshness reasoning*)
   541 by (REPEAT (blast_tac (!claset addSEs partsEs
   542 			       addDs  [Notes_Crypt_parts_spies,
   543 				       impOfSubs analz_subset_parts,
   544 				       Says_imp_spies RS analz.Inj]) 4));
   545 (*ClientHello*)
   546 by (blast_tac (!claset addSDs [Notes_Crypt_parts_spies]
   547                        addSEs spies_partsEs) 3);
   548 (*SpyKeys*)
   549 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   550 by (fast_tac (!claset addss (!simpset)) 2);
   551 (*Fake*)
   552 by (spy_analz_tac 1);
   553 bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
   554 
   555 
   556 (*Another way of showing unicity*)
   557 goal thy 
   558  "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
   559 \           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
   560 \           A ~: bad;  B ~: bad;                         \
   561 \           evs : tls |]                                 \
   562 \        ==> A=A' & B=B'";
   563 by (REPEAT (ares_tac [Notes_unique_PMS, Spy_not_see_PMS] 1));
   564 qed "good_Notes_unique_PMS";
   565 
   566 
   567 (*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
   568   will stay secret.*)
   569 goal thy
   570  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
   571 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   572 \            Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
   573 by (analz_induct_tac 1);   (*35 seconds*)
   574 (*Oops*)
   575 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 9);
   576 (*ClientAccepts and ServerAccepts: because PMS was already visible*)
   577 by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS, 
   578 				      Says_imp_spies RS analz.Inj,
   579 				      Notes_imp_spies RS analz.Inj]) 6));
   580 (*ClientHello*)
   581 by (Blast_tac 3);
   582 (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
   583 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   584 by (blast_tac (!claset addSDs [Spy_not_see_PMS, 
   585 			       Says_imp_spies RS analz.Inj]) 2);
   586 (*Fake*)
   587 by (spy_analz_tac 1);
   588 (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   589 by (REPEAT (blast_tac (!claset addSEs partsEs
   590 			       addDs  [Notes_Crypt_parts_spies,
   591 				       impOfSubs analz_subset_parts,
   592 				       Says_imp_spies RS analz.Inj]) 1));
   593 bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
   594 
   595 
   596 (*** Protocol goals: if A receives ServerFinished, then B is present 
   597      and has used the quoted values XA, XB, etc.  Note that it is up to A
   598      to compare XA with what she originally sent.
   599 ***)
   600 
   601 (*The mention of her name (A) in X assures A that B knows who she is.*)
   602 goal thy
   603  "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   604 \           X = Crypt (serverK(Na,Nb,M))                  \
   605 \                 (Hash{|Nonce M, Number SID,             \
   606 \                        Nonce NA, Number XA, Agent A,    \
   607 \                        Nonce NB, Number XB, Agent B|}); \
   608 \           M = PRF(PMS,NA,NB);                           \
   609 \           evs : tls;  A ~: bad;  B ~: bad |]          \
   610 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
   611 \        X : parts (spies evs) --> Says B A X : set evs";
   612 by (etac rev_mp 1);
   613 by (hyp_subst_tac 1);
   614 by (analz_induct_tac 1);	(*16 seconds*)
   615 (*ServerResume is trivial, but Blast_tac is too slow*)
   616 by (Best_tac 3);
   617 (*ClientCertKeyEx*)
   618 by (Blast_tac 2);
   619 (*Fake: the Spy doesn't have the critical session key!*)
   620 by (REPEAT (rtac impI 1));
   621 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   622 by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   623 				     not_parts_not_analz]) 2);
   624 by (Fake_parts_insert_tac 1);
   625 qed_spec_mp "TrustServerFinished";
   626 
   627 
   628 (*This version refers not to ServerFinished but to any message from B.
   629   We don't assume B has received CertVerify, and an intruder could
   630   have changed A's identity in all other messages, so we can't be sure
   631   that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   632   to bind A's identity with M, then we could replace A' by A below.*)
   633 goal thy
   634  "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   635 \           evs : tls;  A ~: bad;  B ~: bad;                 \
   636 \           M = PRF(PMS,NA,NB) |]            \
   637 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->              \
   638 \            Crypt (serverK(Na,Nb,M)) Y : parts (spies evs)  -->  \
   639 \            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
   640 by (etac rev_mp 1);
   641 by (hyp_subst_tac 1);
   642 by (analz_induct_tac 1);	(*20 seconds*)
   643 by (REPEAT_FIRST (rtac impI));
   644 (*ServerResume, by unicity of PMS*)
   645 by (blast_tac (!claset addSEs [MPair_parts]
   646 		       addDs  [Spy_not_see_PMS, 
   647 			       Notes_Crypt_parts_spies,
   648 			       Notes_master_imp_Crypt_PMS, unique_PMS]) 4);
   649 (*ServerFinished, by unicity of PMS (10 seconds)*)
   650 by (blast_tac (!claset addSEs [MPair_parts]
   651 		       addDs  [Spy_not_see_PMS, 
   652 			       Notes_Crypt_parts_spies,
   653 			       Says_imp_spies RS parts.Inj,
   654 			       unique_PMS]) 3);
   655 (*ClientCertKeyEx*)
   656 by (Blast_tac 2);
   657 (*Fake: the Spy doesn't have the critical session key!*)
   658 by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   659 by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   660 				     not_parts_not_analz]) 2);
   661 by (Fake_parts_insert_tac 1);
   662 qed_spec_mp "TrustServerMsg";
   663 
   664 
   665 (*** Protocol goal: if B receives any message encrypted with clientK
   666      then A has sent it, ASSUMING that A chose PMS.  Authentication is
   667      assumed here; B cannot verify it.  But if the message is
   668      ClientFinished, then B can then check the quoted values XA, XB, etc.
   669 ***)
   670 goal thy
   671  "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                         \
   672 \  ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) -->\
   673 \      Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   674 \      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) -->  \
   675 \      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   676 by (analz_induct_tac 1);	(*23 seconds*)
   677 by (REPEAT_FIRST (rtac impI));
   678 (*ClientResume: by unicity of PMS*)
   679 by (blast_tac (!claset delrules [conjI]
   680 		       addSEs [MPair_parts]
   681                        addSDs [Notes_master_imp_Notes_PMS]
   682 	 	       addDs  [good_Notes_unique_PMS]) 4);
   683 (*ClientFinished: by unicity of PMS*)
   684 by (blast_tac (!claset delrules [conjI]
   685 		       addSEs [MPair_parts]
   686 		       addDs  [good_Notes_unique_PMS]) 3);
   687 (*ClientCertKeyEx*)
   688 by (Blast_tac 2);
   689 (*Fake: the Spy doesn't have the critical session key!*)
   690 by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   691 by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   692 				     not_parts_not_analz]) 2);
   693 by (Fake_parts_insert_tac 1);
   694 qed_spec_mp "TrustClientMsg";
   695 
   696 
   697 
   698 (*** Protocol goal: if B receives ClientFinished, and if B is able to
   699      check a CertVerify from A, then A has used the quoted
   700      values XA, XB, etc.  Even this one requires A to be uncompromised.
   701  ***)
   702 goal thy
   703  "!!evs. [| ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
   704 \           Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
   705 \           Says B  A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
   706 \             : set evs;                                                  \
   707 \           Says A'' B (Crypt (priK A)                                    \
   708 \                       (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))  \
   709 \             : set evs;                                                  \
   710 \        evs : tls;  A ~: bad;  B ~: bad |]                             \
   711 \     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   712 by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
   713                        addDs  [Says_imp_spies RS parts.Inj]) 1);
   714 qed "AuthClientFinished";