src/HOL/Auth/TLS.ML
author paulson
Tue Sep 16 14:40:01 1997 +0200 (1997-09-16)
changeset 3676 cbaec955056b
parent 3672 56e4365a0c99
child 3677 f2569416d18b
permissions -rw-r--r--
Addition of SessionIDs to the Hello and Finished messages
     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 CERTIFICATE VERIFY knows that A is present (But this
    11     message is optional!)
    12 
    13 * A upon receiving SERVER FINISHED 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_clientK RS inj_eq, inj_serverK RS inj_eq];
    52 
    53 (* invKey(clientK x) = clientK x  and similarly for serverK*)
    54 Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
    55 	  isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
    56 
    57 
    58 (*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
    59 
    60 goal thy "pubK A ~= clientK 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_clientK";
    65 
    66 goal thy "pubK A ~= serverK arg";
    67 br notI 1;
    68 by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    69 by (Full_simp_tac 1);
    70 qed "pubK_neq_serverK";
    71 
    72 goal thy "priK A ~= clientK arg";
    73 br notI 1;
    74 by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    75 by (Full_simp_tac 1);
    76 qed "priK_neq_clientK";
    77 
    78 goal thy "priK A ~= serverK arg";
    79 br notI 1;
    80 by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    81 by (Full_simp_tac 1);
    82 qed "priK_neq_serverK";
    83 
    84 (*clientK and serverK have disjoint ranges*)
    85 goal thy "clientK arg ~= serverK arg'";
    86 by (cut_facts_tac [rangeI RS impOfSubs clientK_range] 1);
    87 by (Blast_tac 1);
    88 qed "clientK_neq_serverK";
    89 
    90 val keys_distinct = [pubK_neq_clientK, pubK_neq_serverK, 
    91 		     priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK];
    92 AddIffs (keys_distinct @ (keys_distinct RL [not_sym]));
    93 
    94 
    95 (**** Protocol Proofs ****)
    96 
    97 (*A "possibility property": there are traces that reach the end.
    98   This protocol has three end points and six messages to consider.*)
    99 
   100 
   101 (** These proofs make the further assumption that the Nonce_supply nonces 
   102 	(which have the form  @ N. Nonce N ~: used evs)
   103     lie outside the range of PRF.  This assumption seems reasonable, but
   104     as it is needed only for the possibility theorems, it is not taken
   105     as an axiom.
   106 **)
   107 
   108 
   109 
   110 (*Possibility property ending with ServerFinished.*)
   111 goal thy 
   112  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
   113 \           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
   114 \  Says B A (Crypt (serverK(NA,NB,M))                       \
   115 \            (Hash{|Nonce M, Number SID,             \
   116 \                   Nonce NA, Number XA, Agent A,      \
   117 \                   Nonce NB, Number XB, Agent B|})) \
   118 \    : 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.ServerFinished) 2);
   122 by possibility_tac;
   123 by (REPEAT (Blast_tac 1));
   124 result();
   125 
   126 (*And one for ClientFinished.  Either FINISHED message may come first.*)
   127 goal thy 
   128  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
   129 \           A ~= B |] ==> EX SID NA XA NB XB M. EX evs: tls.    \
   130 \  Says A B (Crypt (clientK(NA,NB,M))                           \
   131 \            (Hash{|Nonce M, Number SID,             \
   132 \                   Nonce NA, Number XA, Agent A,      \
   133 \                   Nonce NB, Number XB, Agent B|})) : set evs";
   134 by (REPEAT (resolve_tac [exI,bexI] 1));
   135 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
   136 	  RS tls.ClientFinished) 2);
   137 by possibility_tac;
   138 by (REPEAT (Blast_tac 1));
   139 result();
   140 
   141 (*Another one, for CertVerify (which is optional)*)
   142 goal thy 
   143  "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
   144 \           A ~= B |] ==> EX NB PMS. EX evs: tls.   \
   145 \  Says A B (Crypt (priK A)                 \
   146 \            (Hash{|Nonce NB, certificate B (pubK B), Nonce PMS|})) : set evs";
   147 by (REPEAT (resolve_tac [exI,bexI] 1));
   148 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
   149 	  RS tls.CertVerify) 2);
   150 by possibility_tac;
   151 by (REPEAT (Blast_tac 1));
   152 result();
   153 
   154 
   155 (**** Inductive proofs about tls ****)
   156 
   157 (*Nobody sends themselves messages*)
   158 goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
   159 by (etac tls.induct 1);
   160 by (Auto_tac());
   161 qed_spec_mp "not_Says_to_self";
   162 Addsimps [not_Says_to_self];
   163 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   164 
   165 
   166 (*Induction for regularity theorems.  If induction formula has the form
   167    X ~: analz (sees Spy evs) --> ... then it shortens the proof by discarding
   168    needless information about analz (insert X (sees Spy evs))  *)
   169 fun parts_induct_tac i = 
   170     etac tls.induct i
   171     THEN 
   172     REPEAT (FIRSTGOAL analz_mono_contra_tac)
   173     THEN 
   174     fast_tac (!claset addss (!simpset)) i THEN
   175     ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if]));
   176 
   177 
   178 (** Theorems of the form X ~: parts (sees Spy evs) imply that NOBODY
   179     sends messages containing X! **)
   180 
   181 (*Spy never sees another agent's private key! (unless it's lost at start)*)
   182 goal thy 
   183  "!!evs. evs : tls ==> (Key (priK A) : parts (sees Spy evs)) = (A : lost)";
   184 by (parts_induct_tac 1);
   185 by (Fake_parts_insert_tac 1);
   186 qed "Spy_see_priK";
   187 Addsimps [Spy_see_priK];
   188 
   189 goal thy 
   190  "!!evs. evs : tls ==> (Key (priK A) : analz (sees Spy evs)) = (A : lost)";
   191 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   192 qed "Spy_analz_priK";
   193 Addsimps [Spy_analz_priK];
   194 
   195 goal thy  "!!A. [| Key (priK A) : parts (sees Spy evs);       \
   196 \                  evs : tls |] ==> A:lost";
   197 by (blast_tac (!claset addDs [Spy_see_priK]) 1);
   198 qed "Spy_see_priK_D";
   199 
   200 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
   201 AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
   202 
   203 
   204 (*This lemma says that no false certificates exist.  One might extend the
   205   model to include bogus certificates for the agents, but there seems
   206   little point in doing so: the loss of their private keys is a worse
   207   breach of security.*)
   208 goalw thy [certificate_def]
   209  "!!evs. evs : tls     \
   210 \        ==> certificate B KB : parts (sees Spy evs) --> KB = pubK B";
   211 by (parts_induct_tac 1);
   212 by (Fake_parts_insert_tac 1);
   213 bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
   214 
   215 
   216 (*Replace key KB in ClientCertKeyEx by (pubK B) *)
   217 val ClientCertKeyEx_tac = 
   218     forward_tac [Says_imp_sees_Spy RS parts.Inj RS 
   219 		 parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
   220     THEN' assume_tac
   221     THEN' hyp_subst_tac;
   222 
   223 fun analz_induct_tac i = 
   224     etac tls.induct i   THEN
   225     ClientCertKeyEx_tac  (i+7)  THEN	(*ClientFinished*)
   226     ClientCertKeyEx_tac  (i+6)  THEN	(*CertVerify*)
   227     ClientCertKeyEx_tac  (i+5)  THEN	(*ClientCertKeyEx*)
   228     ALLGOALS (asm_simp_tac 
   229               (!simpset addcongs [if_weak_cong]
   230                         setloop split_tac [expand_if]))  THEN
   231     (*Remove instances of pubK B:  the Spy already knows all public keys.
   232       Combining the two simplifier calls makes them run extremely slowly.*)
   233     ALLGOALS (asm_simp_tac 
   234               (!simpset addcongs [if_weak_cong]
   235 			addsimps [insert_absorb]
   236                         setloop split_tac [expand_if]));
   237 
   238 
   239 (*** Hashing of nonces ***)
   240 
   241 (*Every Nonce that's hashed is already in past traffic.  
   242   This event occurs in CERTIFICATE VERIFY*)
   243 goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (sees Spy evs);  \
   244 \                   NB ~: range PRF;  evs : tls |]  \
   245 \                ==> Nonce NB : parts (sees Spy evs)";
   246 by (etac rev_mp 1);
   247 by (etac rev_mp 1);
   248 by (parts_induct_tac 1);
   249 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   250 by (Fake_parts_insert_tac 1);
   251 (*FINISHED messages are trivial because M : range PRF*)
   252 by (REPEAT (Blast_tac 2));
   253 (*CERTIFICATE VERIFY is the only interesting case*)
   254 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   255 qed "Hash_Nonce_CV";
   256 
   257 
   258 goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
   259 \                ==> Crypt (pubK B) X : parts (sees Spy evs)";
   260 by (etac rev_mp 1);
   261 by (analz_induct_tac 1);
   262 by (blast_tac (!claset addIs [parts_insertI]) 1);
   263 qed "Notes_Crypt_parts_sees";
   264 
   265 
   266 (*****************
   267     (*NEEDED?  TRUE???
   268       Every Nonce that's hashed is already in past traffic. 
   269       This general formulation is tricky to prove and hard to use, since the
   270       2nd premise is typically proved by simplification.*)
   271     goal thy "!!evs. [| Hash X : parts (sees Spy evs);  \
   272     \                   Nonce N : parts {X};  evs : tls |]  \
   273     \                ==> Nonce N : parts (sees Spy evs)";
   274     by (etac rev_mp 1);
   275     by (parts_induct_tac 1);
   276     by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
   277 				  Says_imp_sees_Spy RS parts.Inj]
   278 			  addSEs partsEs) 1);
   279     by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
   280     by (Fake_parts_insert_tac 1);
   281     (*CertVerify, ClientFinished, ServerFinished (?)*)
   282     by (REPEAT (Blast_tac 1));
   283     qed "Hash_imp_Nonce_seen";
   284 ****************************************************************)
   285 
   286 
   287 (*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
   288 
   289 (*B can check A's signature if he has received A's certificate.
   290   Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
   291   message is Fake.  We don't need guarantees for the Spy anyway.  We must
   292   assume A~:lost; otherwise, the Spy can forge A's signature.*)
   293 goal thy
   294  "!!evs. [| X = Crypt (priK A)                                        \
   295 \                 (Hash{|Nonce NB, certificate B KB, Nonce PMS|});      \
   296 \           evs : tls;  A ~: lost;  B ~= Spy |]                       \
   297 \    ==> Says B A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
   298 \          : set evs --> \
   299 \        X : parts (sees Spy evs) --> Says A B X : set evs";
   300 by (hyp_subst_tac 1);
   301 by (parts_induct_tac 1);
   302 by (Fake_parts_insert_tac 1);
   303 (*ServerHello: nonce NB cannot be in X because it's fresh!*)
   304 by (blast_tac (!claset addSDs [Hash_Nonce_CV]
   305 	               addSEs sees_Spy_partsEs) 1);
   306 qed_spec_mp "TrustCertVerify";
   307 
   308 
   309 (*If CERTIFICATE VERIFY is present then A has chosen PMS.*)
   310 goal thy
   311  "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|})  \
   312 \             : parts (sees Spy evs);                                \
   313 \           evs : tls;  A ~: lost |]                                      \
   314 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
   315 be rev_mp 1;
   316 by (parts_induct_tac 1);
   317 by (Fake_parts_insert_tac 1);
   318 qed "UseCertVerify";
   319 
   320 
   321 (*No collection of keys can help the spy get new private keys*)
   322 goal thy  
   323  "!!evs. evs : tls ==>                                    \
   324 \  ALL KK. (Key(priK B) : analz (Key``KK Un (sees Spy evs))) =  \
   325 \            (priK B : KK | B : lost)";
   326 by (etac tls.induct 1);
   327 by (ALLGOALS
   328     (asm_simp_tac (analz_image_keys_ss
   329 		   addsimps (certificate_def::keys_distinct))));
   330 (*Fake*) 
   331 by (spy_analz_tac 2);
   332 (*Base*)
   333 by (Blast_tac 1);
   334 qed_spec_mp "analz_image_priK";
   335 
   336 
   337 (*Lemma for the trivial direction of the if-and-only-if*)
   338 goal thy  
   339  "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
   340 \        (X : analz (G Un H))  =  (X : analz H)";
   341 by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
   342 val lemma = result();
   343 
   344 (*Knowing some clientKs and serverKs is no help in getting new nonces*)
   345 goal thy  
   346  "!!evs. evs : tls ==>                                 \
   347 \    ALL KK. KK <= (range clientK Un range serverK) -->           \
   348 \            (Nonce N : analz (Key``KK Un (sees Spy evs))) = \
   349 \            (Nonce N : analz (sees Spy evs))";
   350 by (etac tls.induct 1);
   351 by (ClientCertKeyEx_tac 6);
   352 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   353 by (REPEAT_FIRST (rtac lemma));
   354 writeln"SLOW simplification: 60 secs!??";
   355 by (ALLGOALS
   356     (asm_simp_tac (analz_image_keys_ss 
   357 		   addsimps (analz_image_priK::certificate_def::
   358                              keys_distinct))));
   359 by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
   360 (*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*)
   361 by (Blast_tac 3);
   362 (*Fake*) 
   363 by (spy_analz_tac 2);
   364 (*Base*)
   365 by (Blast_tac 1);
   366 qed_spec_mp "analz_image_keys";
   367 
   368 
   369 goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
   370 by (parts_induct_tac 1);
   371 (*ClientCertKeyEx: PMS is assumed to differ from any PRF.*)
   372 by (Blast_tac 1);
   373 qed "no_Notes_A_PRF";
   374 Addsimps [no_Notes_A_PRF];
   375 
   376 
   377 (*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
   378 goal thy
   379  "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
   380 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   381 \            Nonce PMS ~: analz (sees Spy evs)";
   382 by (analz_induct_tac 1);   (*47 seconds???*)
   383 (*ClientHello*)
   384 by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   385                                addSEs sees_Spy_partsEs) 3);
   386 (*SpyKeys*)
   387 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   388 by (fast_tac (!claset addss (!simpset)) 2);
   389 (*Fake*)
   390 by (spy_analz_tac 1);
   391 (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   392 by (REPEAT (blast_tac (!claset addSEs partsEs
   393 			       addDs  [Notes_Crypt_parts_sees,
   394 				       impOfSubs analz_subset_parts,
   395 				       Says_imp_sees_Spy RS analz.Inj]) 1));
   396 bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
   397 
   398 
   399 
   400 goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (sees Spy evs);  \
   401 \                   evs : tls |]  \
   402 \                ==> Nonce PMS : parts (sees Spy evs)";
   403 by (etac rev_mp 1);
   404 by (parts_induct_tac 1);
   405 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   406 by (Fake_parts_insert_tac 1);
   407 (*Client key exchange*)
   408 by (Blast_tac 4);
   409 (*Server Hello: by freshness*)
   410 by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   411 (*Client Hello: trivial*)
   412 by (Blast_tac 2);
   413 (*SpyKeys*)
   414 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   415 qed "MS_imp_PMS";
   416 AddSDs [MS_imp_PMS];
   417 
   418 
   419 (*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
   420   will stay secret.*)
   421 goal thy
   422  "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
   423 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   424 \            Nonce (PRF(PMS,NA,NB)) ~: analz (sees Spy evs)";
   425 by (analz_induct_tac 1);   (*47 seconds???*)
   426 (*ClientHello*)
   427 by (Blast_tac 3);
   428 (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
   429 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   430 by (blast_tac (!claset addSDs [Spy_not_see_PMS, 
   431 			       Says_imp_sees_Spy RS analz.Inj]) 2);
   432 (*Fake*)
   433 by (spy_analz_tac 1);
   434 (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   435 by (REPEAT (blast_tac (!claset addSEs partsEs
   436 			       addDs  [MS_imp_PMS,
   437 				       Notes_Crypt_parts_sees,
   438 				       impOfSubs analz_subset_parts,
   439 				       Says_imp_sees_Spy RS analz.Inj]) 1));
   440 bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
   441 
   442 
   443 
   444 (*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
   445 
   446 (** First, some lemmas about those write keys.  The proofs for serverK are 
   447     nearly identical to those for clientK. **)
   448 
   449 (*Lemma: those write keys are never sent if M (MASTER SECRET) is secure.  
   450   Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
   451 
   452 goal thy 
   453  "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]   \
   454 \        ==> Key (clientK(NA,NB,M)) ~: parts (sees Spy evs)";
   455 by (etac rev_mp 1);
   456 by (analz_induct_tac 1);
   457 (*SpyKeys*)
   458 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
   459 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]) 3);
   460 (*Fake*) 
   461 by (spy_analz_tac 2);
   462 (*Base*)
   463 by (Blast_tac 1);
   464 qed "clientK_notin_parts";
   465 bind_thm ("clientK_in_partsE", clientK_notin_parts RSN (2, rev_notE));
   466 Addsimps [clientK_notin_parts];
   467 AddSEs [clientK_in_partsE, 
   468 	impOfSubs analz_subset_parts RS clientK_in_partsE];
   469 
   470 goal thy 
   471  "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]   \
   472 \        ==> Key (serverK(NA,NB,M)) ~: parts (sees Spy evs)";
   473 by (etac rev_mp 1);
   474 by (analz_induct_tac 1);
   475 (*SpyKeys*)
   476 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
   477 by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]) 3);
   478 (*Fake*) 
   479 by (spy_analz_tac 2);
   480 (*Base*)
   481 by (Blast_tac 1);
   482 qed "serverK_notin_parts";
   483 bind_thm ("serverK_in_partsE", serverK_notin_parts RSN (2, rev_notE));
   484 Addsimps [serverK_notin_parts];
   485 AddSEs [serverK_in_partsE, 
   486 	impOfSubs analz_subset_parts RS serverK_in_partsE];
   487 
   488 
   489 (*Lemma: those write keys are never used if PMS is fresh.  
   490   Nonces don't have to agree, allowing session resumption.
   491   Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
   492   They are NOT suitable as safe elim rules.*)
   493 
   494 goal thy 
   495  "!!evs. [| Nonce PMS ~: used evs;  evs : tls |]                           \
   496 \  ==> Crypt (clientK(Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
   497 by (etac rev_mp 1);
   498 by (analz_induct_tac 1);
   499 (*ClientFinished: since M is fresh, a different instance of clientK was used.*)
   500 by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   501                        addSEs sees_Spy_partsEs) 3);
   502 by (Fake_parts_insert_tac 2);
   503 (*Base*)
   504 by (Blast_tac 1);
   505 qed "Crypt_clientK_notin_parts";
   506 Addsimps [Crypt_clientK_notin_parts];
   507 AddEs [Crypt_clientK_notin_parts RSN (2, rev_notE)];
   508 
   509 goal thy 
   510  "!!evs. [| Nonce PMS ~: used evs;  evs : tls |]                           \
   511 \  ==> Crypt (serverK(Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
   512 by (etac rev_mp 1);
   513 by (analz_induct_tac 1);
   514 (*ServerFinished: since M is fresh, a different instance of serverK was used.*)
   515 by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   516                                addSEs sees_Spy_partsEs) 3);
   517 by (Fake_parts_insert_tac 2);
   518 (*Base*)
   519 by (Blast_tac 1);
   520 qed "Crypt_serverK_notin_parts";
   521 
   522 Addsimps [Crypt_serverK_notin_parts];
   523 AddEs [Crypt_serverK_notin_parts RSN (2, rev_notE)];
   524 
   525 
   526 (*NEEDED??*)
   527 goal thy
   528  "!!evs. [| Says A B {|certA, Crypt KB (Nonce M)|} : set evs;   \
   529 \           A ~= Spy;  evs : tls |] ==> KB = pubK B";
   530 be rev_mp 1;
   531 by (analz_induct_tac 1);
   532 qed "A_Crypt_pubB";
   533 
   534 
   535 (*** Unicity results for PMS, the pre-master-secret ***)
   536 
   537 (*PMS determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
   538 goal thy 
   539  "!!evs. [| Nonce PMS ~: analz (sees Spy evs);  evs : tls |]   \
   540 \        ==> EX B'. ALL B.   \
   541 \              Crypt (pubK B) (Nonce PMS) : parts (sees Spy evs) --> B=B'";
   542 by (etac rev_mp 1);
   543 by (parts_induct_tac 1);
   544 by (Fake_parts_insert_tac 1);
   545 (*ClientCertKeyEx*)
   546 by (ClientCertKeyEx_tac 1);
   547 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   548 by (expand_case_tac "PMS = ?y" 1 THEN
   549     blast_tac (!claset addSEs partsEs) 1);
   550 val lemma = result();
   551 
   552 goal thy 
   553  "!!evs. [| Crypt(pubK B)  (Nonce PMS) : parts (sees Spy evs); \
   554 \           Crypt(pubK B') (Nonce PMS) : parts (sees Spy evs); \
   555 \           Nonce PMS ~: analz (sees Spy evs);                 \
   556 \           evs : tls |]                                          \
   557 \        ==> B=B'";
   558 by (prove_unique_tac lemma 1);
   559 qed "unique_PMS";
   560 
   561 
   562 (*In A's note to herself, PMS determines A and B.*)
   563 goal thy 
   564  "!!evs. [| Nonce PMS ~: analz (sees Spy evs);  evs : tls |]            \
   565 \ ==> EX A' B'. ALL A B.                                                   \
   566 \        Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
   567 by (etac rev_mp 1);
   568 by (parts_induct_tac 1);
   569 by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   570 (*ClientCertKeyEx: if PMS is fresh, then it can't appear in Notes A X.*)
   571 by (expand_case_tac "PMS = ?y" 1 THEN
   572     blast_tac (!claset addSDs [Notes_Crypt_parts_sees] addSEs partsEs) 1);
   573 val lemma = result();
   574 
   575 goal thy 
   576  "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
   577 \           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
   578 \           Nonce PMS ~: analz (sees Spy evs);      \
   579 \           evs : tls |]                               \
   580 \        ==> A=A' & B=B'";
   581 by (prove_unique_tac lemma 1);
   582 qed "Notes_unique_PMS";
   583 
   584 
   585 
   586 (*** Protocol goals: if A receives SERVER FINISHED, then B is present 
   587      and has used the quoted values XA, XB, etc.  Note that it is up to A
   588      to compare XA with what she originally sent.
   589 ***)
   590 
   591 (*The mention of her name (A) in X assumes A that B knows who she is.*)
   592 goal thy
   593  "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
   594 \                 (Hash{|Nonce M, Number SID,             \
   595 \                        Nonce NA, Number XA, Agent A,    \
   596 \                        Nonce NB, Number XB, Agent B|}); \
   597 \           M = PRF(PMS,NA,NB);                           \
   598 \           evs : tls;  A ~: lost;  B ~: lost |]          \
   599 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
   600 \        X : parts (sees Spy evs) --> Says B A X : set evs";
   601 by (hyp_subst_tac 1);
   602 by (analz_induct_tac 1);
   603 (*Fake: the Spy doesn't have the critical session key!*)
   604 by (REPEAT (rtac impI 1));
   605 by (subgoal_tac 
   606     "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
   607 by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   608 				     not_parts_not_analz]) 2);
   609 by (Fake_parts_insert_tac 1);
   610 qed_spec_mp "TrustServerFinished";
   611 
   612 
   613 (*This version refers not to SERVER FINISHED but to any message from B.
   614   We don't assume B has received CERTIFICATE VERIFY, and an intruder could
   615   have changed A's identity in all other messages, so we can't be sure
   616   that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   617   to bind A's identity with M, then we could replace A' by A below.*)
   618 goal thy
   619  "!!evs. [| evs : tls;  A ~: lost;  B ~: lost;                 \
   620 \           M = PRF(PMS,NA,NB) |]            \
   621 \        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->              \
   622 \            Crypt (serverK(Na,Nb,M)) Y : parts (sees Spy evs)  -->  \
   623 \            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
   624 by (hyp_subst_tac 1);
   625 by (analz_induct_tac 1);
   626 by (REPEAT_FIRST (rtac impI));
   627 (*Fake: the Spy doesn't have the critical session key!*)
   628 by (subgoal_tac 
   629     "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy 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 (*ServerFinished.  If the message is old then apply induction hypothesis...*)
   634 by (rtac conjI 1 THEN Blast_tac 2);
   635 (*...otherwise delete induction hyp and use unicity of PMS.*)
   636 by (thin_tac "?PP-->?QQ" 1);
   637 by (Step_tac 1);
   638 by (subgoal_tac "Nonce PMS ~: analz (sees Spy evsSF)" 1);
   639 by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
   640 by (blast_tac (!claset addSEs [MPair_parts]
   641 		       addDs  [Notes_Crypt_parts_sees,
   642 			       Says_imp_sees_Spy RS parts.Inj,
   643 			       unique_PMS]) 1);
   644 qed_spec_mp "TrustServerMsg";
   645 
   646 
   647 (*** Protocol goal: if B receives any message encrypted with clientK
   648      then A has sent it, ASSUMING that A chose PMS.  Authentication is
   649      assumed here; B cannot verify it.  But if the message is
   650      CLIENT FINISHED, then B can then check the quoted values XA, XB, etc.
   651 ***)
   652 goal thy
   653  "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                         \
   654 \  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   655 \      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (sees Spy evs) -->  \
   656 \      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   657 by (analz_induct_tac 1);
   658 by (REPEAT_FIRST (rtac impI));
   659 (*Fake: the Spy doesn't have the critical session key!*)
   660 by (subgoal_tac 
   661     "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
   662 by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   663 				     not_parts_not_analz]) 2);
   664 by (Fake_parts_insert_tac 1);
   665 (*ClientFinished.  If the message is old then apply induction hypothesis...*)
   666 by (step_tac (!claset delrules [conjI]) 1);
   667 by (subgoal_tac "Nonce PMS ~: analz (sees Spy evsCF)" 1);
   668 by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
   669 by (blast_tac (!claset addSEs [MPair_parts]
   670 		       addDs  [Notes_unique_PMS]) 1);
   671 qed_spec_mp "TrustClientMsg";
   672 
   673 
   674 (*** Protocol goal: if B receives CLIENT FINISHED, and if B is able to
   675      check a CERTIFICATE VERIFY from A, then A has used the quoted
   676      values XA, XB, etc.  Even this one requires A to be uncompromised.
   677  ***)
   678 goal thy
   679  "!!evs. [| Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
   680 \           Says B  A {|Nonce NB, Number SID, Number XB, certificate B KB|}  \
   681 \             : set evs;                                                  \
   682 \           Says A'' B (Crypt (priK A)                                    \
   683 \                       (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))  \
   684 \             : set evs;                                                  \
   685 \        evs : tls;  A ~: lost;  B ~: lost |]                             \
   686 \     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   687 by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
   688                        addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   689 qed "AuthClientFinished";