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