More realistic model: the Spy can compute clientK and serverK
authorpaulson
Tue Jul 01 17:37:42 1997 +0200 (1997-07-01)
changeset 3480d59bbf053258
parent 3479 2aacd6f10654
child 3481 256f38c01b98
More realistic model: the Spy can compute clientK and serverK
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/TLS.ML	Tue Jul 01 17:36:42 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Tue Jul 01 17:37:42 1997 +0200
     1.3 @@ -4,17 +4,36 @@
     1.4      Copyright   1997  University of Cambridge
     1.5  
     1.6  The public-key model has a weakness, especially concerning anonymous sessions.
     1.7 -The Spy's state is recorded as the trace of message.  But if he himself is 
     1.8 -the Client and invents M, then the event he sends contains M encrypted with B's
     1.9 -public key.  From the trace there is no reason to believe that the spy knows
    1.10 -M, and yet the spy actually chose M!  So, in any property concerning the 
    1.11 -secrecy of some item, one must somehow establish that the spy didn't choose
    1.12 -the item.  In practice, this weakness does little harm, since one can expect
    1.13 -few guarantees when communicating directly with an enemy.
    1.14 +The Spy's state is recorded as the trace of message.  But if he himself is the
    1.15 +Client and invents M, then he sends contains M encrypted with B's public key.
    1.16 +This message gives no evidence that the spy knows M, and yet the spy actually
    1.17 +chose M!  So, in any property concerning the secrecy of some item, one must
    1.18 +establish that the spy didn't choose the item.  Guarantees normally assume
    1.19 +that the other party is uncompromised (otherwise, one can prove little).
    1.20 +
    1.21 +Protocol goals: 
    1.22 +* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
    1.23 +     parties (though A is not necessarily authenticated).
    1.24 +
    1.25 +* B upon receiving CERTIFICATE VERIFY knows that A is present (But this
    1.26 +    message is optional!)
    1.27  
    1.28 -The model, at present, doesn't recognize that if the Spy has NA, NB and M then
    1.29 -he also has clientK(NA,NB,M) and serverK(NA,NB,M).  Maybe this doesn't really
    1.30 -matter, since one can prove that he doesn't get M.
    1.31 +* A upon receiving SERVER FINISHED knows that B is present
    1.32 +
    1.33 +* Each party who has received a FINISHED message can trust that the other
    1.34 +  party agrees on all message components, including XA and XB (thus foiling
    1.35 +  rollback attacks).
    1.36 +
    1.37 +A curious property found in these proofs is that CERTIFICATE VERIFY actually
    1.38 +gives weaker authentication than CLIENT FINISHED.  The theorem for CERTIFICATE
    1.39 +VERIFY is subject to A~:lost, since if A's private key is known to the spy
    1.40 +then he can forge A's signature.  But the theorem for CLIENT FINISHED merely
    1.41 +assumes that A is not the spy himself, since the model assumes that all other
    1.42 +agents tell the truth.
    1.43 +
    1.44 +In the real world, there are agents who are not active attackers, and yet
    1.45 +still cannot be trusted to identify themselves.  There may well be more such
    1.46 +agents than there are compromised private keys.
    1.47  *)
    1.48  
    1.49  open TLS;
    1.50 @@ -24,13 +43,18 @@
    1.51  
    1.52  AddIffs [Spy_in_lost, Server_not_lost];
    1.53  
    1.54 +goal thy "!!A. A ~: lost ==> A ~= Spy";
    1.55 +by (Blast_tac 1);
    1.56 +qed "not_lost_not_eq_Spy";
    1.57 +Addsimps [not_lost_not_eq_Spy];
    1.58 +
    1.59  (*Injectiveness of key-generating functions*)
    1.60  AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq];
    1.61  
    1.62  (* invKey(clientK x) = clientK x  and similarly for serverK*)
    1.63  Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
    1.64  	  isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
    1.65 -	  
    1.66 +
    1.67  
    1.68  (*Replacing the variable by a constant improves search speed by 50%!*)
    1.69  val Says_imp_sees_Spy' = 
    1.70 @@ -63,8 +87,14 @@
    1.71  by (Full_simp_tac 1);
    1.72  qed "priK_neq_serverK";
    1.73  
    1.74 +(*clientK and serverK have disjoint ranges*)
    1.75 +goal thy "clientK arg ~= serverK arg'";
    1.76 +by (cut_facts_tac [rangeI RS impOfSubs clientK_range] 1);
    1.77 +by (Blast_tac 1);
    1.78 +qed "clientK_neq_serverK";
    1.79 +
    1.80  val ths = [pubK_neq_clientK, pubK_neq_serverK, 
    1.81 -	   priK_neq_clientK, priK_neq_serverK];
    1.82 +	   priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK];
    1.83  AddIffs (ths @ (ths RL [not_sym]));
    1.84  
    1.85  
    1.86 @@ -218,7 +248,8 @@
    1.87  (*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
    1.88  
    1.89  (*Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
    1.90 -  message is Fake.  We don't need guarantees for the Spy anyway.*)
    1.91 +  message is Fake.  We don't need guarantees for the Spy anyway.  We must
    1.92 +  assume A~:lost; otherwise, the Spy can forge A's signature.*)
    1.93  goal thy 
    1.94   "!!evs. [| X = Crypt (priK A)                          \
    1.95  \                 (Hash{|Nonce NB,                                      \
    1.96 @@ -227,11 +258,11 @@
    1.97  \    ==> Says B A {|Nonce NA, Nonce NB, Agent XB,       \
    1.98  \                   Crypt (priK Server) {|Agent B, Key KB|}|} : set evs --> \
    1.99  \        X : parts (sees lost Spy evs) --> Says A B X : set evs";
   1.100 -by (Asm_simp_tac 1);
   1.101 +by (hyp_subst_tac 1);
   1.102  by (etac tls.induct 1);
   1.103  by (ALLGOALS Asm_simp_tac);
   1.104  by (Fake_parts_insert_tac 1);
   1.105 -(*ServerHello*)
   1.106 +(*ServerHello: nonce NB cannot be in X because it's fresh!*)
   1.107  by (blast_tac (!claset addSDs [Hash_imp_Nonce1]
   1.108  	               addSEs sees_Spy_partsEs) 1);
   1.109  qed_spec_mp "TrustCertVerify";
   1.110 @@ -261,7 +292,7 @@
   1.111  
   1.112  fun analz_induct_tac i = 
   1.113      etac tls.induct i   THEN
   1.114 -    ClientCertKeyEx_tac  (i+4)  THEN
   1.115 +    ClientCertKeyEx_tac  (i+5)  THEN
   1.116      ALLGOALS (asm_simp_tac 
   1.117                (!simpset addsimps [not_parts_not_analz]
   1.118                          setloop split_tac [expand_if]))  THEN
   1.119 @@ -271,15 +302,83 @@
   1.120                (!simpset addsimps [insert_absorb]
   1.121                          setloop split_tac [expand_if]));
   1.122  
   1.123 -(*If A sends ClientCertKeyEx to an honest agent B, then M will stay secret.*)
   1.124 +(*** Specialized rewriting for the analz_image_... theorems ***)
   1.125 +
   1.126 +goal thy "insert (Key K) H = Key `` {K} Un H";
   1.127 +by (Blast_tac 1);
   1.128 +qed "insert_Key_singleton";
   1.129 +
   1.130 +goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
   1.131 +by (Blast_tac 1);
   1.132 +qed "insert_Key_image";
   1.133 +
   1.134 +(*Reverse the normal simplification of "image" to build up (not break down)
   1.135 +  the set of keys.  Based on analz_image_freshK_ss, but simpler.*)
   1.136 +val analz_image_keys_ss = 
   1.137 +     !simpset delsimps [image_insert, image_Un]
   1.138 +              addsimps [image_insert RS sym, image_Un RS sym,
   1.139 +			rangeI, 
   1.140 +			insert_Key_singleton, 
   1.141 +			insert_Key_image, Un_assoc RS sym]
   1.142 +              setloop split_tac [expand_if];
   1.143 +
   1.144 +(*No collection of keys can help the spy get new private keys*)
   1.145 +goal thy  
   1.146 + "!!evs. evs : tls ==>                                    \
   1.147 +\  ALL KK. (Key(priK B) : analz (Key``KK Un (sees lost Spy evs))) =  \
   1.148 +\            (priK B : KK | B : lost)";
   1.149 +by (etac tls.induct 1);
   1.150 +by (ALLGOALS (asm_simp_tac analz_image_keys_ss));
   1.151 +(*Fake*) 
   1.152 +by (spy_analz_tac 2);
   1.153 +(*Base*)
   1.154 +by (Blast_tac 1);
   1.155 +qed_spec_mp "analz_image_priK";
   1.156 +
   1.157 +
   1.158 +(*Lemma for the trivial direction of the if-and-only-if*)
   1.159 +goal thy  
   1.160 + "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
   1.161 +\        (X : analz (G Un H))  =  (X : analz H)";
   1.162 +by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
   1.163 +val lemma = result();
   1.164 +
   1.165 +(*Knowing some clientKs and serverKs is no help in getting new nonces*)
   1.166 +goal thy  
   1.167 + "!!evs. evs : tls ==>                                 \
   1.168 +\    ALL KK. KK <= (range clientK Un range serverK) -->           \
   1.169 +\            (Nonce N : analz (Key``KK Un (sees lost Spy evs))) = \
   1.170 +\            (Nonce N : analz (sees lost Spy evs))";
   1.171 +by (etac tls.induct 1);
   1.172 +by (ClientCertKeyEx_tac 6);
   1.173 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.174 +by (REPEAT_FIRST (rtac lemma ));
   1.175 +	(*SLOW: 30s!*)
   1.176 +by (ALLGOALS (asm_simp_tac analz_image_keys_ss));
   1.177 +by (ALLGOALS (asm_simp_tac
   1.178 +	      (!simpset addsimps [analz_image_priK, insert_absorb])));
   1.179 +(*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*)
   1.180 +by (Blast_tac 3);
   1.181 +(*Fake*) 
   1.182 +by (spy_analz_tac 2);
   1.183 +(*Base*)
   1.184 +by (Blast_tac 1);
   1.185 +qed_spec_mp "analz_image_keys";
   1.186 +
   1.187 +
   1.188 +(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.
   1.189 +  The assumption is A~=Spy, not A~:lost, since A doesn't use her private key
   1.190 +  here.*)
   1.191  goal thy 
   1.192 - "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |] ==> \
   1.193 -\    Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
   1.194 -\               Crypt KB (Nonce M)|} : set evs -->  \
   1.195 -\    Nonce M ~: analz (sees lost Spy evs)";
   1.196 + "!!evs. [| evs : tls;  A~=Spy;  B ~: lost |]                       \
   1.197 +\        ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
   1.198 +\                       Crypt KB (Nonce M)|} : set evs -->             \
   1.199 +\            Nonce M ~: analz (sees lost Spy evs)";
   1.200  by (analz_induct_tac 1);
   1.201  (*ClientHello*)
   1.202 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 2);
   1.203 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   1.204 +(*SpyKeys*)
   1.205 +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   1.206  (*Fake*)
   1.207  by (spy_analz_tac 1);
   1.208  (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   1.209 @@ -291,79 +390,96 @@
   1.210  
   1.211  (*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
   1.212  
   1.213 -(*In fact, nothing of the form clientK(NA,NB,M) or serverK(NA,NB,M) is ever
   1.214 -  sent!  These two theorems are too strong: the Spy is quite capable of
   1.215 -  forming many items of the form serverK(NA,NB,M).
   1.216 -  Additional Fake rules could model this capability.*)
   1.217 -
   1.218 +(*The two proofs are identical*)
   1.219  goal thy 
   1.220 - "!!evs. evs : tls ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)";
   1.221 -by (etac tls.induct 1);
   1.222 -by (prove_simple_subgoals_tac 1);
   1.223 -by (Fake_parts_insert_tac 1);
   1.224 + "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  \
   1.225 +\           evs : tls |]                           \
   1.226 +\        ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)";
   1.227 +by (etac rev_mp 1);
   1.228 +by (analz_induct_tac 1);
   1.229 +(*SpyKeys*)
   1.230 +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
   1.231 +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3);
   1.232 +(*Fake*) 
   1.233 +by (spy_analz_tac 2);
   1.234 +(*Base*)
   1.235 +by (Blast_tac 1);
   1.236  qed "clientK_notin_parts";
   1.237  
   1.238  goal thy 
   1.239 - "!!evs. evs : tls ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)";
   1.240 -by (etac tls.induct 1);
   1.241 -by (prove_simple_subgoals_tac 1);
   1.242 -by (Fake_parts_insert_tac 1);
   1.243 + "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  \
   1.244 +\           evs : tls |]                           \
   1.245 +\        ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)";
   1.246 +by (etac rev_mp 1);
   1.247 +by (analz_induct_tac 1);
   1.248 +(*SpyKeys*)
   1.249 +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
   1.250 +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]) 3);
   1.251 +(*Fake*) 
   1.252 +by (spy_analz_tac 2);
   1.253 +(*Base*)
   1.254 +by (Blast_tac 1);
   1.255  qed "serverK_notin_parts";
   1.256  
   1.257 -(*We need a version of AddIffs that takes CONDITIONAL equivalences*)
   1.258 -val ths = [clientK_notin_parts, clientK_notin_parts RS not_parts_not_analz,
   1.259 -	   serverK_notin_parts, serverK_notin_parts RS not_parts_not_analz];
   1.260 -Addsimps ths;
   1.261 -AddSEs (ths RLN (2, [rev_notE]));
   1.262 -
   1.263  
   1.264  (*** Protocol goals: if A receives SERVER FINISHED, then B is present 
   1.265       and has used the quoted values XA, XB, etc.  Note that it is up to A
   1.266       to compare XA with what she originally sent.
   1.267  ***)
   1.268  
   1.269 -(*Perhaps A~=Spy is unnecessary, but there's no obvious proof if the first
   1.270 -  message is Fake.  We don't need guarantees for the Spy anyway.*)
   1.271  goal thy 
   1.272 - "!!evs. [| X = Crypt (serverK(NA,NB,M))                        \
   1.273 -\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
   1.274 -\                        Nonce NA, Agent XA, Agent A,           \
   1.275 -\                        Nonce NB, Agent XB,                    \
   1.276 + "!!evs. [| X = Crypt (serverK(NA,NB,M))                            \
   1.277 +\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},       \
   1.278 +\                        Nonce NA, Agent XA, Agent A,               \
   1.279 +\                        Nonce NB, Agent XB,                        \
   1.280  \                        Crypt (priK Server) {|Agent B, Key (pubK B)|}|}); \
   1.281 -\           evs : tls;  A~=Spy;  B ~: lost |] ==>               \
   1.282 -\    Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},  \
   1.283 -\               Crypt KB (Nonce M)|} : set evs -->              \
   1.284 -\    X : parts (sees lost Spy evs) --> Says B A X : set evs";
   1.285 -by (Asm_simp_tac 1);
   1.286 +\           evs : tls;  A~=Spy;  B ~: lost |]                       \
   1.287 +\    ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},  \
   1.288 +\                   Crypt KB (Nonce M)|} : set evs -->              \
   1.289 +\        X : parts (sees lost Spy evs) --> Says B A X : set evs";
   1.290 +by (hyp_subst_tac 1);
   1.291  by (etac tls.induct 1);
   1.292  by (ALLGOALS Asm_simp_tac);
   1.293 +(*ClientCertKeyEx: M isn't in the Hash because it's fresh!*)
   1.294 +by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce]
   1.295 +                       addSEs sees_Spy_partsEs) 2);
   1.296 +(*Fake: the Spy doesn't have the critical session key!*)
   1.297 +by (REPEAT (rtac impI 1));
   1.298 +by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
   1.299 +by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
   1.300 +				     serverK_notin_parts, 
   1.301 +				     not_parts_not_analz]) 2);
   1.302  by (Fake_parts_insert_tac 1);
   1.303 -(*ClientCertKeyEx*)
   1.304 -by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce]
   1.305 -                       addSEs sees_Spy_partsEs) 1);
   1.306  qed_spec_mp "TrustServerFinished";
   1.307  
   1.308  
   1.309 -(*** Protocol goal: if B receives CLIENT FINISHED, then A  is present ??
   1.310 +(*** Protocol goal: if B receives CLIENT FINISHED, then A  is present
   1.311       and has used the quoted values XA, XB, etc.  Note that it is up to B
   1.312       to compare XB with what he originally sent. ***)
   1.313  
   1.314 -(*This result seems far too strong--it may be provable because the current
   1.315 -  model gives the Spy access to NO keys of the form clientK(NA,NB,M).*)
   1.316 +(*This result seems too strong: A need not have sent CERTIFICATE VERIFY.  
   1.317 +  But we assume (as always) that the other party is honest...*)
   1.318  goal thy 
   1.319   "!!evs. [| X = Crypt (clientK(NA,NB,M))                        \
   1.320  \                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
   1.321  \                        Nonce NA, Agent XA,                    \
   1.322  \                        Crypt (priK Server) {|Agent A, Key (pubK A)|}, \
   1.323  \                        Nonce NB, Agent XB, Agent B|});        \
   1.324 -\           evs : tls |] ==>               \
   1.325 -\    X : parts (sees lost Spy evs) --> Says A B X : set evs";
   1.326 -by (Asm_simp_tac 1);
   1.327 +\           evs : tls;  A~=Spy;  B ~: lost |]                   \
   1.328 +\     ==> Says A B {|Crypt (priK Server) {|Agent A, Key (pubK A)|},  \
   1.329 +\                    Crypt KB (Nonce M)|} : set evs -->              \
   1.330 +\         X : parts (sees lost Spy evs) --> Says A B X : set evs";
   1.331 +by (hyp_subst_tac 1);
   1.332  by (etac tls.induct 1);
   1.333  by (ALLGOALS Asm_simp_tac);
   1.334 -by (Blast_tac 1);
   1.335 +(*ClientCertKeyEx: M isn't in the Hash because it's fresh!*)
   1.336 +by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce]
   1.337 +                       addSEs sees_Spy_partsEs) 2);
   1.338 +(*Fake: the Spy doesn't have the critical session key!*)
   1.339 +by (REPEAT (rtac impI 1));
   1.340 +by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
   1.341 +by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
   1.342 +				     clientK_notin_parts, 
   1.343 +				     not_parts_not_analz]) 2);
   1.344  by (Fake_parts_insert_tac 1);
   1.345  qed_spec_mp "TrustClientFinished";
   1.346 -
   1.347 -
   1.348 -
     2.1 --- a/src/HOL/Auth/TLS.thy	Tue Jul 01 17:36:42 1997 +0200
     2.2 +++ b/src/HOL/Auth/TLS.thy	Tue Jul 01 17:37:42 1997 +0200
     2.3 @@ -12,20 +12,12 @@
     2.4  A is the client and B is the server, not to be confused with the constant
     2.5  Server, who is in charge of all public keys.
     2.6  
     2.7 -The model assumes that no fraudulent certificates are present.
     2.8 -
     2.9 -Protocol goals: 
    2.10 -* M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
    2.11 -     parties (though A is not necessarily authenticated).
    2.12 +The model assumes that no fraudulent certificates are present, but it does
    2.13 +assume that some private keys are lost to the spy.
    2.14  
    2.15 -* B upon receiving CERTIFICATE VERIFY knows that A is present (But this
    2.16 -    message is optional!)
    2.17 -
    2.18 -* A upon receiving SERVER FINISHED knows that B is present
    2.19 -
    2.20 -* Each party who has received a FINISHED message can trust that the other
    2.21 -  party agrees on all message components, including XA and XB (thus foiling
    2.22 -  rollback attacks).
    2.23 +Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
    2.24 +Allen, Transport Layer Security Working Group, 21 May 1997,
    2.25 +INTERNET-DRAFT draft-ietf-tls-protocol-03.txt
    2.26  *)
    2.27  
    2.28  TLS = Public + 
    2.29 @@ -39,9 +31,13 @@
    2.30    inj_clientK   "inj clientK"	
    2.31    isSym_clientK "isSymKey (clientK x)"	(*client write keys are symmetric*)
    2.32  
    2.33 +  (*serverK is similar*)
    2.34    inj_serverK   "inj serverK"	
    2.35    isSym_serverK "isSymKey (serverK x)"	(*server write keys are symmetric*)
    2.36  
    2.37 +  (*Clashes with pubK and priK are impossible, but this axiom is needed.*)
    2.38 +  clientK_range "range clientK <= Compl (range serverK)"
    2.39 +
    2.40    (*Spy has access to his own key for spoof messages, but Server is secure*)
    2.41    Spy_in_lost     "Spy: lost"
    2.42    Server_not_lost "Server ~: lost"
    2.43 @@ -58,7 +54,13 @@
    2.44      Fake (*The spy, an active attacker, MAY say anything he CAN say.*)
    2.45           "[| evs: tls;  B ~= Spy;  
    2.46               X: synth (analz (sees lost Spy evs)) |]
    2.47 -          ==> Says Spy B X  # evs : tls"
    2.48 +          ==> Says Spy B X # evs : tls"
    2.49 +
    2.50 +    SpyKeys (*The spy may apply clientK & serverK to nonces he's found*)
    2.51 +         "[| evs: tls;
    2.52 +	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evs |]
    2.53 +          ==> Says Spy B {| Key (clientK(NA,NB,M)),
    2.54 +			    Key (serverK(NA,NB,M)) |} # evs : tls"
    2.55  
    2.56      ClientHello
    2.57  	 (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.