src/HOL/Auth/TLS.ML
author paulson
Tue Jul 01 17:37:42 1997 +0200 (1997-07-01)
changeset 3480 d59bbf053258
parent 3474 44249bba00ec
child 3500 0d8ad2f192d8
permissions -rw-r--r--
More realistic model: the Spy can compute clientK and serverK
     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 The public-key model has a weakness, especially concerning anonymous sessions.
     7 The Spy's state is recorded as the trace of message.  But if he himself is the
     8 Client and invents M, then he sends contains M encrypted with B's public key.
     9 This message gives no evidence that the spy knows M, and yet the spy actually
    10 chose M!  So, in any property concerning the secrecy of some item, one must
    11 establish that the spy didn't choose the item.  Guarantees normally assume
    12 that the other party is uncompromised (otherwise, one can prove little).
    13 
    14 Protocol goals: 
    15 * M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
    16      parties (though A is not necessarily authenticated).
    17 
    18 * B upon receiving CERTIFICATE VERIFY knows that A is present (But this
    19     message is optional!)
    20 
    21 * A upon receiving SERVER FINISHED knows that B is present
    22 
    23 * Each party who has received a FINISHED message can trust that the other
    24   party agrees on all message components, including XA and XB (thus foiling
    25   rollback attacks).
    26 
    27 A curious property found in these proofs is that CERTIFICATE VERIFY actually
    28 gives weaker authentication than CLIENT FINISHED.  The theorem for CERTIFICATE
    29 VERIFY is subject to A~:lost, since if A's private key is known to the spy
    30 then he can forge A's signature.  But the theorem for CLIENT FINISHED merely
    31 assumes that A is not the spy himself, since the model assumes that all other
    32 agents tell the truth.
    33 
    34 In the real world, there are agents who are not active attackers, and yet
    35 still cannot be trusted to identify themselves.  There may well be more such
    36 agents than there are compromised private keys.
    37 *)
    38 
    39 open TLS;
    40 
    41 proof_timing:=true;
    42 HOL_quantifiers := false;
    43 
    44 AddIffs [Spy_in_lost, Server_not_lost];
    45 
    46 goal thy "!!A. A ~: lost ==> A ~= Spy";
    47 by (Blast_tac 1);
    48 qed "not_lost_not_eq_Spy";
    49 Addsimps [not_lost_not_eq_Spy];
    50 
    51 (*Injectiveness of key-generating functions*)
    52 AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq];
    53 
    54 (* invKey(clientK x) = clientK x  and similarly for serverK*)
    55 Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
    56 	  isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
    57 
    58 
    59 (*Replacing the variable by a constant improves search speed by 50%!*)
    60 val Says_imp_sees_Spy' = 
    61     read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy;
    62 
    63 
    64 (*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
    65 
    66 goal thy "pubK A ~= clientK 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_clientK";
    71 
    72 goal thy "pubK A ~= serverK arg";
    73 br notI 1;
    74 by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    75 by (Full_simp_tac 1);
    76 qed "pubK_neq_serverK";
    77 
    78 goal thy "priK A ~= clientK 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_clientK";
    83 
    84 goal thy "priK A ~= serverK arg";
    85 br notI 1;
    86 by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    87 by (Full_simp_tac 1);
    88 qed "priK_neq_serverK";
    89 
    90 (*clientK and serverK have disjoint ranges*)
    91 goal thy "clientK arg ~= serverK arg'";
    92 by (cut_facts_tac [rangeI RS impOfSubs clientK_range] 1);
    93 by (Blast_tac 1);
    94 qed "clientK_neq_serverK";
    95 
    96 val ths = [pubK_neq_clientK, pubK_neq_serverK, 
    97 	   priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK];
    98 AddIffs (ths @ (ths RL [not_sym]));
    99 
   100 
   101 (**** Protocol Proofs ****)
   102 
   103 (*A "possibility property": there are traces that reach the end.
   104   This protocol has three end points and six messages to consider.*)
   105 
   106 (*Possibility property ending with ServerFinished.*)
   107 goal thy 
   108  "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
   109 \  Says B A (Crypt (serverK(NA,NB,M))                 \
   110 \            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
   111 \                   Nonce NA, Agent XA, Agent A,      \
   112 \                   Nonce NB, Agent XB,               \
   113 \                   Crypt (priK Server) {|Agent B, Key (pubK B)|}|})) \
   114 \    : set evs";
   115 by (REPEAT (resolve_tac [exI,bexI] 1));
   116 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
   117 	  RS tls.ServerFinished) 2);
   118 by possibility_tac;
   119 result();
   120 
   121 (*And one for ClientFinished.  Either FINISHED message may come first.*)
   122 goal thy 
   123  "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
   124 \  Says A B (Crypt (clientK(NA,NB,M))                 \
   125 \            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
   126 \                   Nonce NA, Agent XA,               \
   127 \                   Crypt (priK Server) {|Agent A, Key (pubK A)|},      \
   128 \                   Nonce NB, Agent XB, Agent B|})) : set evs";
   129 by (REPEAT (resolve_tac [exI,bexI] 1));
   130 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
   131 	  RS tls.ClientFinished) 2);
   132 by possibility_tac;
   133 result();
   134 
   135 (*Another one, for CertVerify (which is optional)*)
   136 goal thy 
   137  "!!A B. A ~= B ==> EX NB. EX evs: tls.     \
   138 \  Says A B (Crypt (priK A)                 \
   139 \            (Hash{|Nonce NB,               \
   140 \                   Crypt (priK Server)     \
   141 \                         {|Agent B, Key (pubK B)|}|})) : set evs";
   142 by (REPEAT (resolve_tac [exI,bexI] 1));
   143 by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.CertVerify) 2);
   144 by possibility_tac;
   145 result();
   146 
   147 
   148 (**** Inductive proofs about tls ****)
   149 
   150 (*Nobody sends themselves messages*)
   151 goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
   152 by (etac tls.induct 1);
   153 by (Auto_tac());
   154 qed_spec_mp "not_Says_to_self";
   155 Addsimps [not_Says_to_self];
   156 AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   157 
   158 
   159 (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
   160     sends messages containing X! **)
   161 
   162 (*Spy never sees another agent's private key! (unless it's lost at start)*)
   163 goal thy 
   164  "!!evs. evs : tls \
   165 \        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
   166 by (etac tls.induct 1);
   167 by (prove_simple_subgoals_tac 1);
   168 by (Fake_parts_insert_tac 1);
   169 qed "Spy_see_priK";
   170 Addsimps [Spy_see_priK];
   171 
   172 goal thy 
   173  "!!evs. evs : tls \
   174 \        ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)";
   175 by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
   176 qed "Spy_analz_priK";
   177 Addsimps [Spy_analz_priK];
   178 
   179 goal thy  "!!A. [| Key (priK A) : parts (sees lost Spy evs);       \
   180 \                  evs : tls |] ==> A:lost";
   181 by (blast_tac (!claset addDs [Spy_see_priK]) 1);
   182 qed "Spy_see_priK_D";
   183 
   184 bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D);
   185 AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
   186 
   187 
   188 (*Every Nonce that's hashed is already in past traffic. *)
   189 goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees lost Spy evs);  \
   190 \                   evs : tls |]  \
   191 \                ==> Nonce N : parts (sees lost Spy evs)";
   192 by (etac rev_mp 1);
   193 by (etac tls.induct 1);
   194 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   195 by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   196 		      addSEs partsEs) 1);
   197 by (Fake_parts_insert_tac 1);
   198 qed "Hash_imp_Nonce1";
   199 
   200 (*Lemma needed to prove Hash_Hash_imp_Nonce*)
   201 goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|}  \
   202 \                       : parts (sees lost Spy evs);     \
   203 \                   evs : tls |]  \
   204 \                ==> Nonce M : parts (sees lost Spy evs)";
   205 by (etac rev_mp 1);
   206 by (etac tls.induct 1);
   207 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   208 by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   209 		      addSEs partsEs) 1);
   210 by (Fake_parts_insert_tac 1);
   211 qed "Hash_imp_Nonce2";
   212 AddSDs [Hash_imp_Nonce2];
   213 
   214 goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |}  \
   215 \                      : parts (sees lost Spy evs);      \
   216 \                   evs : tls |]                         \
   217 \                ==> Nonce M : parts (sees lost Spy evs)";
   218 by (etac rev_mp 1);
   219 by (etac tls.induct 1);
   220 by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   221 by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   222 		      addSEs partsEs) 1);
   223 by (Fake_parts_insert_tac 1);
   224 qed "Hash_Hash_imp_Nonce";
   225 
   226 
   227 (*NEEDED??
   228   Every Nonce that's hashed is already in past traffic. 
   229   This general formulation is tricky to prove and hard to use, since the
   230   2nd premise is typically proved by simplification.*)
   231 goal thy "!!evs. [| Hash X : parts (sees lost Spy evs);  \
   232 \                   Nonce N : parts {X};  evs : tls |]  \
   233 \                ==> Nonce N : parts (sees lost Spy evs)";
   234 by (etac rev_mp 1);
   235 by (etac tls.induct 1);
   236 by (ALLGOALS Asm_simp_tac);
   237 by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   238 		      addSEs partsEs) 1);
   239 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
   240 (*ServerFinished*)
   241 by (Blast_tac 3);
   242 (*ClientFinished*)
   243 by (Blast_tac 2);
   244 by (Fake_parts_insert_tac 1);
   245 qed "Hash_imp_Nonce_seen";
   246 
   247 
   248 (*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
   249 
   250 (*Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
   251   message is Fake.  We don't need guarantees for the Spy anyway.  We must
   252   assume A~:lost; otherwise, the Spy can forge A's signature.*)
   253 goal thy 
   254  "!!evs. [| X = Crypt (priK A)                          \
   255 \                 (Hash{|Nonce NB,                                      \
   256 \                        Crypt (priK Server) {|Agent B, Key KB|}|});    \
   257 \           evs : tls;  A ~: lost;  B ~= Spy |]         \
   258 \    ==> Says B A {|Nonce NA, Nonce NB, Agent XB,       \
   259 \                   Crypt (priK Server) {|Agent B, Key KB|}|} : set evs --> \
   260 \        X : parts (sees lost Spy evs) --> Says A B X : set evs";
   261 by (hyp_subst_tac 1);
   262 by (etac tls.induct 1);
   263 by (ALLGOALS Asm_simp_tac);
   264 by (Fake_parts_insert_tac 1);
   265 (*ServerHello: nonce NB cannot be in X because it's fresh!*)
   266 by (blast_tac (!claset addSDs [Hash_imp_Nonce1]
   267 	               addSEs sees_Spy_partsEs) 1);
   268 qed_spec_mp "TrustCertVerify";
   269 
   270 
   271 (*This lemma says that no false certificates exist.  One might extend the
   272   model to include bogus certificates for the lost agents, but there seems
   273   little point in doing so: the loss of their private keys is a worse
   274   breach of security.*)
   275 goal thy 
   276  "!!evs. evs : tls     \
   277 \    ==> Crypt (priK Server) {|Agent B, Key KB|} : parts (sees lost Spy evs) \
   278 \        --> KB = pubK B";
   279 by (etac tls.induct 1);
   280 by (ALLGOALS Asm_simp_tac);
   281 by (Fake_parts_insert_tac 2);
   282 by (Blast_tac 1);
   283 bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
   284 
   285 
   286 (*Replace key KB in ClientCertKeyEx by (pubK B) *)
   287 val ClientCertKeyEx_tac = 
   288     forward_tac [Says_imp_sees_Spy' RS parts.Inj RS 
   289 		 parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
   290     THEN' assume_tac
   291     THEN' hyp_subst_tac;
   292 
   293 fun analz_induct_tac i = 
   294     etac tls.induct i   THEN
   295     ClientCertKeyEx_tac  (i+5)  THEN
   296     ALLGOALS (asm_simp_tac 
   297               (!simpset addsimps [not_parts_not_analz]
   298                         setloop split_tac [expand_if]))  THEN
   299     (*Remove instances of pubK B:  the Spy already knows all public keys.
   300       Combining the two simplifier calls makes them run extremely slowly.*)
   301     ALLGOALS (asm_simp_tac 
   302               (!simpset addsimps [insert_absorb]
   303                         setloop split_tac [expand_if]));
   304 
   305 (*** Specialized rewriting for the analz_image_... theorems ***)
   306 
   307 goal thy "insert (Key K) H = Key `` {K} Un H";
   308 by (Blast_tac 1);
   309 qed "insert_Key_singleton";
   310 
   311 goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
   312 by (Blast_tac 1);
   313 qed "insert_Key_image";
   314 
   315 (*Reverse the normal simplification of "image" to build up (not break down)
   316   the set of keys.  Based on analz_image_freshK_ss, but simpler.*)
   317 val analz_image_keys_ss = 
   318      !simpset delsimps [image_insert, image_Un]
   319               addsimps [image_insert RS sym, image_Un RS sym,
   320 			rangeI, 
   321 			insert_Key_singleton, 
   322 			insert_Key_image, Un_assoc RS sym]
   323               setloop split_tac [expand_if];
   324 
   325 (*No collection of keys can help the spy get new private keys*)
   326 goal thy  
   327  "!!evs. evs : tls ==>                                    \
   328 \  ALL KK. (Key(priK B) : analz (Key``KK Un (sees lost Spy evs))) =  \
   329 \            (priK B : KK | B : lost)";
   330 by (etac tls.induct 1);
   331 by (ALLGOALS (asm_simp_tac analz_image_keys_ss));
   332 (*Fake*) 
   333 by (spy_analz_tac 2);
   334 (*Base*)
   335 by (Blast_tac 1);
   336 qed_spec_mp "analz_image_priK";
   337 
   338 
   339 (*Lemma for the trivial direction of the if-and-only-if*)
   340 goal thy  
   341  "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
   342 \        (X : analz (G Un H))  =  (X : analz H)";
   343 by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
   344 val lemma = result();
   345 
   346 (*Knowing some clientKs and serverKs is no help in getting new nonces*)
   347 goal thy  
   348  "!!evs. evs : tls ==>                                 \
   349 \    ALL KK. KK <= (range clientK Un range serverK) -->           \
   350 \            (Nonce N : analz (Key``KK Un (sees lost Spy evs))) = \
   351 \            (Nonce N : analz (sees lost Spy evs))";
   352 by (etac tls.induct 1);
   353 by (ClientCertKeyEx_tac 6);
   354 by (REPEAT_FIRST (resolve_tac [allI, impI]));
   355 by (REPEAT_FIRST (rtac lemma ));
   356 	(*SLOW: 30s!*)
   357 by (ALLGOALS (asm_simp_tac analz_image_keys_ss));
   358 by (ALLGOALS (asm_simp_tac
   359 	      (!simpset addsimps [analz_image_priK, 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 (*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.
   370   The assumption is A~=Spy, not A~:lost, since A doesn't use her private key
   371   here.*)
   372 goal thy 
   373  "!!evs. [| evs : tls;  A~=Spy;  B ~: lost |]                       \
   374 \        ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
   375 \                       Crypt KB (Nonce M)|} : set evs -->             \
   376 \            Nonce M ~: analz (sees lost Spy evs)";
   377 by (analz_induct_tac 1);
   378 (*ClientHello*)
   379 by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   380 (*SpyKeys*)
   381 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   382 (*Fake*)
   383 by (spy_analz_tac 1);
   384 (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   385 by (REPEAT (blast_tac (!claset addSEs partsEs
   386 			       addDs  [impOfSubs analz_subset_parts,
   387 				       Says_imp_sees_Spy' RS analz.Inj]) 1));
   388 bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp));
   389 
   390 
   391 (*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
   392 
   393 (*The two proofs are identical*)
   394 goal thy 
   395  "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  \
   396 \           evs : tls |]                           \
   397 \        ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)";
   398 by (etac rev_mp 1);
   399 by (analz_induct_tac 1);
   400 (*SpyKeys*)
   401 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
   402 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3);
   403 (*Fake*) 
   404 by (spy_analz_tac 2);
   405 (*Base*)
   406 by (Blast_tac 1);
   407 qed "clientK_notin_parts";
   408 
   409 goal thy 
   410  "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  \
   411 \           evs : tls |]                           \
   412 \        ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)";
   413 by (etac rev_mp 1);
   414 by (analz_induct_tac 1);
   415 (*SpyKeys*)
   416 by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
   417 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3);
   418 (*Fake*) 
   419 by (spy_analz_tac 2);
   420 (*Base*)
   421 by (Blast_tac 1);
   422 qed "serverK_notin_parts";
   423 
   424 
   425 (*** Protocol goals: if A receives SERVER FINISHED, then B is present 
   426      and has used the quoted values XA, XB, etc.  Note that it is up to A
   427      to compare XA with what she originally sent.
   428 ***)
   429 
   430 goal thy 
   431  "!!evs. [| X = Crypt (serverK(NA,NB,M))                            \
   432 \                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},       \
   433 \                        Nonce NA, Agent XA, Agent A,               \
   434 \                        Nonce NB, Agent XB,                        \
   435 \                        Crypt (priK Server) {|Agent B, Key (pubK B)|}|}); \
   436 \           evs : tls;  A~=Spy;  B ~: lost |]                       \
   437 \    ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},  \
   438 \                   Crypt KB (Nonce M)|} : set evs -->              \
   439 \        X : parts (sees lost Spy evs) --> Says B A X : set evs";
   440 by (hyp_subst_tac 1);
   441 by (etac tls.induct 1);
   442 by (ALLGOALS Asm_simp_tac);
   443 (*ClientCertKeyEx: M isn't in the Hash because it's fresh!*)
   444 by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce]
   445                        addSEs sees_Spy_partsEs) 2);
   446 (*Fake: the Spy doesn't have the critical session key!*)
   447 by (REPEAT (rtac impI 1));
   448 by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
   449 by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
   450 				     serverK_notin_parts, 
   451 				     not_parts_not_analz]) 2);
   452 by (Fake_parts_insert_tac 1);
   453 qed_spec_mp "TrustServerFinished";
   454 
   455 
   456 (*** Protocol goal: if B receives CLIENT FINISHED, then A  is present
   457      and has used the quoted values XA, XB, etc.  Note that it is up to B
   458      to compare XB with what he originally sent. ***)
   459 
   460 (*This result seems too strong: A need not have sent CERTIFICATE VERIFY.  
   461   But we assume (as always) that the other party is honest...*)
   462 goal thy 
   463  "!!evs. [| X = Crypt (clientK(NA,NB,M))                        \
   464 \                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
   465 \                        Nonce NA, Agent XA,                    \
   466 \                        Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
   467 \                        Nonce NB, Agent XB, Agent B|});        \
   468 \           evs : tls;  A~=Spy;  B ~: lost |]                   \
   469 \     ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},  \
   470 \                    Crypt KB (Nonce M)|} : set evs -->              \
   471 \         X : parts (sees lost Spy evs) --> Says A B X : set evs";
   472 by (hyp_subst_tac 1);
   473 by (etac tls.induct 1);
   474 by (ALLGOALS Asm_simp_tac);
   475 (*ClientCertKeyEx: M isn't in the Hash because it's fresh!*)
   476 by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce]
   477                        addSEs sees_Spy_partsEs) 2);
   478 (*Fake: the Spy doesn't have the critical session key!*)
   479 by (REPEAT (rtac impI 1));
   480 by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
   481 by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
   482 				     clientK_notin_parts, 
   483 				     not_parts_not_analz]) 2);
   484 by (Fake_parts_insert_tac 1);
   485 qed_spec_mp "TrustClientFinished";