TLS now with a distinction between premaster secret and master secret
authorpaulson
Tue Sep 16 13:32:22 1997 +0200 (1997-09-16)
changeset 367256e4365a0c99
parent 3671 8326f03d667c
child 3673 3b06747c3f37
TLS now with a distinction between premaster secret and master secret
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/TLS.ML	Fri Sep 12 10:45:51 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Tue Sep 16 13:32:22 1997 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4  
     1.5  
     1.6  (*Injectiveness of key-generating functions*)
     1.7 -AddIffs [inj_clientK RS inj_eq, inj_serverK RS inj_eq];
     1.8 +AddIffs [inj_PRF RS inj_eq, inj_clientK RS inj_eq, inj_serverK RS inj_eq];
     1.9  
    1.10  (* invKey(clientK x) = clientK x  and similarly for serverK*)
    1.11  Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
    1.12 @@ -97,43 +97,56 @@
    1.13  (*A "possibility property": there are traces that reach the end.
    1.14    This protocol has three end points and six messages to consider.*)
    1.15  
    1.16 +
    1.17 +(** These proofs make the further assumption that the Nonce_supply nonces 
    1.18 +	(which have the form  @ N. Nonce N ~: used evs)
    1.19 +    lie outside the range of PRF.  This assumption seems reasonable, but
    1.20 +    as it is needed only for the possibility theorems, it is not taken
    1.21 +    as an axiom.
    1.22 +**)
    1.23 +
    1.24 +
    1.25 +
    1.26  (*Possibility property ending with ServerFinished.*)
    1.27  goal thy 
    1.28 - "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.    \
    1.29 -\  Says B A (Crypt (serverK(NA,NB,M))                 \
    1.30 -\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|}, \
    1.31 -\                   Nonce NA, Agent XA, Agent A,      \
    1.32 -\                   Nonce NB, Agent XB,               \
    1.33 -\                   certificate B (pubK B)|})) \
    1.34 + "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.35 +\           A ~= B |] ==> EX NA XA NB XB M. EX evs: tls.    \
    1.36 +\  Says B A (Crypt (serverK(NA,NB,M))                       \
    1.37 +\            (Hash{|Nonce M, Nonce NA, Number XA, Agent A,      \
    1.38 +\                   Nonce NB, Number XB, Agent B|})) \
    1.39  \    : set evs";
    1.40  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.41  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.42  	  RS tls.ServerFinished) 2);
    1.43  by possibility_tac;
    1.44 +by (REPEAT (Blast_tac 1));
    1.45  result();
    1.46  
    1.47  (*And one for ClientFinished.  Either FINISHED message may come first.*)
    1.48  goal thy 
    1.49 - "!!A B. A ~= B ==> EX NA XA NB XB M. EX evs: tls.              \
    1.50 + "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.51 +\           A ~= B |] ==> EX NA XA NB XB M. EX evs: tls.    \
    1.52  \  Says A B (Crypt (clientK(NA,NB,M))                           \
    1.53 -\            (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},        \
    1.54 -\                   Nonce NA, Agent XA, certificate A (pubK A), \
    1.55 -\                   Nonce NB, Agent XB, Agent B|})) : set evs";
    1.56 +\            (Hash{|Nonce M, Nonce NA, Number XA, Agent A, \
    1.57 +\                   Nonce NB, Number XB, Agent B|})) : set evs";
    1.58  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.59  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.60  	  RS tls.ClientFinished) 2);
    1.61  by possibility_tac;
    1.62 +by (REPEAT (Blast_tac 1));
    1.63  result();
    1.64  
    1.65  (*Another one, for CertVerify (which is optional)*)
    1.66  goal thy 
    1.67 - "!!A B. A ~= B ==> EX NB M. EX evs: tls.   \
    1.68 + "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
    1.69 +\           A ~= B |] ==> EX NB PMS. EX evs: tls.   \
    1.70  \  Says A B (Crypt (priK A)                 \
    1.71 -\            (Hash{|Nonce NB, certificate B (pubK B), Nonce M|})) : set evs";
    1.72 +\            (Hash{|Nonce NB, certificate B (pubK B), Nonce PMS|})) : set evs";
    1.73  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.74  by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.75  	  RS tls.CertVerify) 2);
    1.76  by possibility_tac;
    1.77 +by (REPEAT (Blast_tac 1));
    1.78  result();
    1.79  
    1.80  
    1.81 @@ -211,40 +224,33 @@
    1.82      ClientCertKeyEx_tac  (i+6)  THEN	(*CertVerify*)
    1.83      ClientCertKeyEx_tac  (i+5)  THEN	(*ClientCertKeyEx*)
    1.84      ALLGOALS (asm_simp_tac 
    1.85 -              (!simpset addsimps [not_parts_not_analz]
    1.86 +              (!simpset addcongs [if_weak_cong]
    1.87                          setloop split_tac [expand_if]))  THEN
    1.88      (*Remove instances of pubK B:  the Spy already knows all public keys.
    1.89        Combining the two simplifier calls makes them run extremely slowly.*)
    1.90      ALLGOALS (asm_simp_tac 
    1.91 -              (!simpset addsimps [insert_absorb]
    1.92 +              (!simpset addcongs [if_weak_cong]
    1.93 +			addsimps [insert_absorb]
    1.94                          setloop split_tac [expand_if]));
    1.95  
    1.96  
    1.97  (*** Hashing of nonces ***)
    1.98  
    1.99 -(*Every Nonce that's hashed is already in past traffic. *)
   1.100 -goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees Spy evs);  \
   1.101 -\                   evs : tls |]  \
   1.102 -\                ==> Nonce N : parts (sees Spy evs)";
   1.103 +(*Every Nonce that's hashed is already in past traffic.  
   1.104 +  This event occurs in CERTIFICATE VERIFY*)
   1.105 +goal thy "!!evs. [| Hash {|Nonce NB, X|} : parts (sees Spy evs);  \
   1.106 +\                   NB ~: range PRF;  evs : tls |]  \
   1.107 +\                ==> Nonce NB : parts (sees Spy evs)";
   1.108 +by (etac rev_mp 1);
   1.109  by (etac rev_mp 1);
   1.110  by (parts_induct_tac 1);
   1.111  by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   1.112  by (Fake_parts_insert_tac 1);
   1.113 -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
   1.114 -	               addSEs partsEs) 1);
   1.115 -qed "Hash_imp_Nonce1";
   1.116 -
   1.117 -(*Lemma needed to prove Hash_Hash_imp_Nonce*)
   1.118 -goal thy "!!evs. [| Hash{|Nonce NA, Nonce NB, Nonce M|}  \
   1.119 -\                       : parts (sees Spy evs);     \
   1.120 -\                   evs : tls |]  \
   1.121 -\                ==> Nonce M : parts (sees Spy evs)";
   1.122 -by (etac rev_mp 1);
   1.123 -by (parts_induct_tac 1);
   1.124 -by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 1);
   1.125 -by (Fake_parts_insert_tac 1);
   1.126 -qed "Hash_imp_Nonce2";
   1.127 -AddSDs [Hash_imp_Nonce2];
   1.128 +(*FINISHED messages are trivial because M : range PRF*)
   1.129 +by (REPEAT (Blast_tac 2));
   1.130 +(*CERTIFICATE VERIFY is the only interesting case*)
   1.131 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   1.132 +qed "Hash_Nonce_CV";
   1.133  
   1.134  
   1.135  goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
   1.136 @@ -255,38 +261,25 @@
   1.137  qed "Notes_Crypt_parts_sees";
   1.138  
   1.139  
   1.140 -(*NEEDED??*)
   1.141 -goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |}  \
   1.142 -\                      : parts (sees Spy evs);      \
   1.143 -\                   evs : tls |]                         \
   1.144 -\                ==> Nonce M : parts (sees Spy evs)";
   1.145 -by (etac rev_mp 1);
   1.146 -by (parts_induct_tac 1);
   1.147 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   1.148 -by (Fake_parts_insert_tac 1);
   1.149 -by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_sees,
   1.150 -				       Says_imp_sees_Spy RS parts.Inj]
   1.151 -		               addSEs partsEs) 1));
   1.152 -qed "Hash_Hash_imp_Nonce";
   1.153 -
   1.154 -
   1.155 -(*NEEDED??
   1.156 -  Every Nonce that's hashed is already in past traffic. 
   1.157 -  This general formulation is tricky to prove and hard to use, since the
   1.158 -  2nd premise is typically proved by simplification.*)
   1.159 -goal thy "!!evs. [| Hash X : parts (sees Spy evs);  \
   1.160 -\                   Nonce N : parts {X};  evs : tls |]  \
   1.161 -\                ==> Nonce N : parts (sees Spy evs)";
   1.162 -by (etac rev_mp 1);
   1.163 -by (parts_induct_tac 1);
   1.164 -by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
   1.165 -			      Says_imp_sees_Spy RS parts.Inj]
   1.166 -		      addSEs partsEs) 1);
   1.167 -by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
   1.168 -by (Fake_parts_insert_tac 1);
   1.169 -(*CertVerify, ClientFinished, ServerFinished (?)*)
   1.170 -by (REPEAT (Blast_tac 1));
   1.171 -qed "Hash_imp_Nonce_seen";
   1.172 +(*****************
   1.173 +    (*NEEDED?  TRUE???
   1.174 +      Every Nonce that's hashed is already in past traffic. 
   1.175 +      This general formulation is tricky to prove and hard to use, since the
   1.176 +      2nd premise is typically proved by simplification.*)
   1.177 +    goal thy "!!evs. [| Hash X : parts (sees Spy evs);  \
   1.178 +    \                   Nonce N : parts {X};  evs : tls |]  \
   1.179 +    \                ==> Nonce N : parts (sees Spy evs)";
   1.180 +    by (etac rev_mp 1);
   1.181 +    by (parts_induct_tac 1);
   1.182 +    by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
   1.183 +				  Says_imp_sees_Spy RS parts.Inj]
   1.184 +			  addSEs partsEs) 1);
   1.185 +    by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
   1.186 +    by (Fake_parts_insert_tac 1);
   1.187 +    (*CertVerify, ClientFinished, ServerFinished (?)*)
   1.188 +    by (REPEAT (Blast_tac 1));
   1.189 +    qed "Hash_imp_Nonce_seen";
   1.190 +****************************************************************)
   1.191  
   1.192  
   1.193  (*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
   1.194 @@ -297,26 +290,26 @@
   1.195    assume A~:lost; otherwise, the Spy can forge A's signature.*)
   1.196  goal thy
   1.197   "!!evs. [| X = Crypt (priK A)                                        \
   1.198 -\                 (Hash{|Nonce NB, certificate B KB, Nonce M|});      \
   1.199 +\                 (Hash{|Nonce NB, certificate B KB, Nonce PMS|});      \
   1.200  \           evs : tls;  A ~: lost;  B ~= Spy |]                       \
   1.201 -\    ==> Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
   1.202 +\    ==> Says B A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}  \
   1.203  \          : set evs --> \
   1.204  \        X : parts (sees Spy evs) --> Says A B X : set evs";
   1.205  by (hyp_subst_tac 1);
   1.206  by (parts_induct_tac 1);
   1.207  by (Fake_parts_insert_tac 1);
   1.208  (*ServerHello: nonce NB cannot be in X because it's fresh!*)
   1.209 -by (blast_tac (!claset addSDs [Hash_imp_Nonce1]
   1.210 +by (blast_tac (!claset addSDs [Hash_Nonce_CV]
   1.211  	               addSEs sees_Spy_partsEs) 1);
   1.212  qed_spec_mp "TrustCertVerify";
   1.213  
   1.214  
   1.215 -(*If CERTIFICATE VERIFY is present then A has chosen M.*)
   1.216 +(*If CERTIFICATE VERIFY is present then A has chosen PMS.*)
   1.217  goal thy
   1.218 - "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce M|})  \
   1.219 + "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce PMS|})  \
   1.220  \             : parts (sees Spy evs);                                \
   1.221  \           evs : tls;  A ~: lost |]                                      \
   1.222 -\        ==> Notes A {|Agent B, Nonce M|} : set evs";
   1.223 +\        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
   1.224  be rev_mp 1;
   1.225  by (parts_induct_tac 1);
   1.226  by (Fake_parts_insert_tac 1);
   1.227 @@ -356,12 +349,11 @@
   1.228  by (ClientCertKeyEx_tac 6);
   1.229  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.230  by (REPEAT_FIRST (rtac lemma));
   1.231 -writeln"SLOW simplification: 50 secs!??";
   1.232 +writeln"SLOW simplification: 60 secs!??";
   1.233  by (ALLGOALS
   1.234      (asm_simp_tac (analz_image_keys_ss 
   1.235 -                   addsimps (analz_image_priK::certificate_def::
   1.236 +		   addsimps (analz_image_priK::certificate_def::
   1.237                               keys_distinct))));
   1.238 -by (ALLGOALS (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_priK])));
   1.239  by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
   1.240  (*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*)
   1.241  by (Blast_tac 3);
   1.242 @@ -372,17 +364,26 @@
   1.243  qed_spec_mp "analz_image_keys";
   1.244  
   1.245  
   1.246 -(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.*)
   1.247 +goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
   1.248 +by (parts_induct_tac 1);
   1.249 +(*ClientCertKeyEx: PMS is assumed to differ from any PRF.*)
   1.250 +by (Blast_tac 1);
   1.251 +qed "no_Notes_A_PRF";
   1.252 +Addsimps [no_Notes_A_PRF];
   1.253 +
   1.254 +
   1.255 +(*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
   1.256  goal thy
   1.257   "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
   1.258 -\        ==> Notes A {|Agent B, Nonce M|} : set evs  -->   \
   1.259 -\            Nonce M ~: analz (sees Spy evs)";
   1.260 -by (analz_induct_tac 1);
   1.261 +\        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   1.262 +\            Nonce PMS ~: analz (sees Spy evs)";
   1.263 +by (analz_induct_tac 1);   (*47 seconds???*)
   1.264  (*ClientHello*)
   1.265  by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   1.266                                 addSEs sees_Spy_partsEs) 3);
   1.267  (*SpyKeys*)
   1.268  by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   1.269 +by (fast_tac (!claset addss (!simpset)) 2);
   1.270  (*Fake*)
   1.271  by (spy_analz_tac 1);
   1.272  (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   1.273 @@ -390,7 +391,52 @@
   1.274  			       addDs  [Notes_Crypt_parts_sees,
   1.275  				       impOfSubs analz_subset_parts,
   1.276  				       Says_imp_sees_Spy RS analz.Inj]) 1));
   1.277 -bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp));
   1.278 +bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
   1.279 +
   1.280 +
   1.281 +
   1.282 +goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (sees Spy evs);  \
   1.283 +\                   evs : tls |]  \
   1.284 +\                ==> Nonce PMS : parts (sees Spy evs)";
   1.285 +by (etac rev_mp 1);
   1.286 +by (parts_induct_tac 1);
   1.287 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   1.288 +by (Fake_parts_insert_tac 1);
   1.289 +(*Client key exchange*)
   1.290 +by (Blast_tac 4);
   1.291 +(*Server Hello: by freshness*)
   1.292 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   1.293 +(*Client Hello: trivial*)
   1.294 +by (Blast_tac 2);
   1.295 +(*SpyKeys*)
   1.296 +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   1.297 +qed "MS_imp_PMS";
   1.298 +AddSDs [MS_imp_PMS];
   1.299 +
   1.300 +
   1.301 +(*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
   1.302 +  will stay secret.*)
   1.303 +goal thy
   1.304 + "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
   1.305 +\        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   1.306 +\            Nonce (PRF(PMS,NA,NB)) ~: analz (sees Spy evs)";
   1.307 +by (analz_induct_tac 1);   (*47 seconds???*)
   1.308 +(*ClientHello*)
   1.309 +by (Blast_tac 3);
   1.310 +(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
   1.311 +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   1.312 +by (blast_tac (!claset addSDs [Spy_not_see_PMS, 
   1.313 +			       Says_imp_sees_Spy RS analz.Inj]) 2);
   1.314 +(*Fake*)
   1.315 +by (spy_analz_tac 1);
   1.316 +(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   1.317 +by (REPEAT (blast_tac (!claset addSEs partsEs
   1.318 +			       addDs  [MS_imp_PMS,
   1.319 +				       Notes_Crypt_parts_sees,
   1.320 +				       impOfSubs analz_subset_parts,
   1.321 +				       Says_imp_sees_Spy RS analz.Inj]) 1));
   1.322 +bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
   1.323 +
   1.324  
   1.325  
   1.326  (*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
   1.327 @@ -398,7 +444,7 @@
   1.328  (** First, some lemmas about those write keys.  The proofs for serverK are 
   1.329      nearly identical to those for clientK. **)
   1.330  
   1.331 -(*Lemma: those write keys are never sent if M is secure.  
   1.332 +(*Lemma: those write keys are never sent if M (MASTER SECRET) is secure.  
   1.333    Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
   1.334  
   1.335  goal thy 
   1.336 @@ -414,9 +460,10 @@
   1.337  (*Base*)
   1.338  by (Blast_tac 1);
   1.339  qed "clientK_notin_parts";
   1.340 -
   1.341 +bind_thm ("clientK_in_partsE", clientK_notin_parts RSN (2, rev_notE));
   1.342  Addsimps [clientK_notin_parts];
   1.343 -AddSEs [clientK_notin_parts RSN (2, rev_notE)];
   1.344 +AddSEs [clientK_in_partsE, 
   1.345 +	impOfSubs analz_subset_parts RS clientK_in_partsE];
   1.346  
   1.347  goal thy 
   1.348   "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]   \
   1.349 @@ -431,33 +478,35 @@
   1.350  (*Base*)
   1.351  by (Blast_tac 1);
   1.352  qed "serverK_notin_parts";
   1.353 -
   1.354 +bind_thm ("serverK_in_partsE", serverK_notin_parts RSN (2, rev_notE));
   1.355  Addsimps [serverK_notin_parts];
   1.356 -AddSEs [serverK_notin_parts RSN (2, rev_notE)];
   1.357 +AddSEs [serverK_in_partsE, 
   1.358 +	impOfSubs analz_subset_parts RS serverK_in_partsE];
   1.359  
   1.360 -(*Lemma: those write keys are never used if M is fresh.  
   1.361 -  Converse doesn't hold; betraying M doesn't force the keys to be sent!
   1.362 -  NOT suitable as safe elim rules.*)
   1.363 +
   1.364 +(*Lemma: those write keys are never used if PMS is fresh.  
   1.365 +  Nonces don't have to agree, allowing session resumption.
   1.366 +  Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
   1.367 +  They are NOT suitable as safe elim rules.*)
   1.368  
   1.369  goal thy 
   1.370 - "!!evs. [| Nonce M ~: used evs;  evs : tls |]                           \
   1.371 -\        ==> Crypt (clientK(NA,NB,M)) Y ~: parts (sees Spy evs)";
   1.372 + "!!evs. [| Nonce PMS ~: used evs;  evs : tls |]                           \
   1.373 +\  ==> Crypt (clientK(Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
   1.374  by (etac rev_mp 1);
   1.375  by (analz_induct_tac 1);
   1.376  (*ClientFinished: since M is fresh, a different instance of clientK was used.*)
   1.377  by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   1.378 -                               addSEs sees_Spy_partsEs) 3);
   1.379 +                       addSEs sees_Spy_partsEs) 3);
   1.380  by (Fake_parts_insert_tac 2);
   1.381  (*Base*)
   1.382  by (Blast_tac 1);
   1.383  qed "Crypt_clientK_notin_parts";
   1.384 -
   1.385  Addsimps [Crypt_clientK_notin_parts];
   1.386  AddEs [Crypt_clientK_notin_parts RSN (2, rev_notE)];
   1.387  
   1.388  goal thy 
   1.389 - "!!evs. [| Nonce M ~: used evs;  evs : tls |]                           \
   1.390 -\        ==> Crypt (serverK(NA,NB,M)) Y ~: parts (sees Spy evs)";
   1.391 + "!!evs. [| Nonce PMS ~: used evs;  evs : tls |]                           \
   1.392 +\  ==> Crypt (serverK(Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
   1.393  by (etac rev_mp 1);
   1.394  by (analz_induct_tac 1);
   1.395  (*ServerFinished: since M is fresh, a different instance of serverK was used.*)
   1.396 @@ -481,54 +530,54 @@
   1.397  qed "A_Crypt_pubB";
   1.398  
   1.399  
   1.400 -(*** Unicity results for M, the pre-master-secret ***)
   1.401 +(*** Unicity results for PMS, the pre-master-secret ***)
   1.402  
   1.403 -(*M determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
   1.404 +(*PMS determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
   1.405  goal thy 
   1.406 - "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]   \
   1.407 + "!!evs. [| Nonce PMS ~: analz (sees Spy evs);  evs : tls |]   \
   1.408  \        ==> EX B'. ALL B.   \
   1.409 -\              Crypt (pubK B) (Nonce M) : parts (sees Spy evs) --> B=B'";
   1.410 +\              Crypt (pubK B) (Nonce PMS) : parts (sees Spy evs) --> B=B'";
   1.411  by (etac rev_mp 1);
   1.412  by (parts_induct_tac 1);
   1.413  by (Fake_parts_insert_tac 1);
   1.414  (*ClientCertKeyEx*)
   1.415  by (ClientCertKeyEx_tac 1);
   1.416  by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   1.417 -by (expand_case_tac "M = ?y" 1 THEN
   1.418 +by (expand_case_tac "PMS = ?y" 1 THEN
   1.419      blast_tac (!claset addSEs partsEs) 1);
   1.420  val lemma = result();
   1.421  
   1.422  goal thy 
   1.423 - "!!evs. [| Crypt(pubK B)  (Nonce M) : parts (sees Spy evs); \
   1.424 -\           Crypt(pubK B') (Nonce M) : parts (sees Spy evs); \
   1.425 -\           Nonce M ~: analz (sees Spy evs);                 \
   1.426 + "!!evs. [| Crypt(pubK B)  (Nonce PMS) : parts (sees Spy evs); \
   1.427 +\           Crypt(pubK B') (Nonce PMS) : parts (sees Spy evs); \
   1.428 +\           Nonce PMS ~: analz (sees Spy evs);                 \
   1.429  \           evs : tls |]                                          \
   1.430  \        ==> B=B'";
   1.431  by (prove_unique_tac lemma 1);
   1.432 -qed "unique_M";
   1.433 +qed "unique_PMS";
   1.434  
   1.435  
   1.436 -(*In A's note to herself, M determines A and B.*)
   1.437 +(*In A's note to herself, PMS determines A and B.*)
   1.438  goal thy 
   1.439 - "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]            \
   1.440 + "!!evs. [| Nonce PMS ~: analz (sees Spy evs);  evs : tls |]            \
   1.441  \ ==> EX A' B'. ALL A B.                                                   \
   1.442 -\        Notes A {|Agent B, Nonce M|} : set evs --> A=A' & B=B'";
   1.443 +\        Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
   1.444  by (etac rev_mp 1);
   1.445  by (parts_induct_tac 1);
   1.446  by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   1.447 -(*ClientCertKeyEx: if M is fresh, then it can't appear in Notes A X.*)
   1.448 -by (expand_case_tac "M = ?y" 1 THEN
   1.449 +(*ClientCertKeyEx: if PMS is fresh, then it can't appear in Notes A X.*)
   1.450 +by (expand_case_tac "PMS = ?y" 1 THEN
   1.451      blast_tac (!claset addSDs [Notes_Crypt_parts_sees] addSEs partsEs) 1);
   1.452  val lemma = result();
   1.453  
   1.454  goal thy 
   1.455 - "!!evs. [| Notes A  {|Agent B,  Nonce M|} : set evs;  \
   1.456 -\           Notes A' {|Agent B', Nonce M|} : set evs;  \
   1.457 -\           Nonce M ~: analz (sees Spy evs);      \
   1.458 + "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
   1.459 +\           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
   1.460 +\           Nonce PMS ~: analz (sees Spy evs);      \
   1.461  \           evs : tls |]                               \
   1.462  \        ==> A=A' & B=B'";
   1.463  by (prove_unique_tac lemma 1);
   1.464 -qed "Notes_unique_M";
   1.465 +qed "Notes_unique_PMS";
   1.466  
   1.467  
   1.468  
   1.469 @@ -539,20 +588,20 @@
   1.470  
   1.471  (*The mention of her name (A) in X assumes A that B knows who she is.*)
   1.472  goal thy
   1.473 - "!!evs. [| X = Crypt (serverK(NA,NB,M))                                \
   1.474 -\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},           \
   1.475 -\                        Nonce NA, Agent XA, Agent A,                   \
   1.476 -\                        Nonce NB, Agent XB, certificate B (pubK B)|}); \
   1.477 + "!!evs. [| X = Crypt (serverK(Na,Nb,M))                                \
   1.478 +\                 (Hash{|Nonce M, Nonce NA, Number XA, Agent A,         \
   1.479 +\                        Nonce NB, Number XB, Agent B|}); \
   1.480 +\           M = PRF(PMS,NA,NB); \
   1.481  \           evs : tls;  A ~: lost;  B ~: lost |]                        \
   1.482 -\        ==> Notes A {|Agent B, Nonce M|} : set evs -->                 \
   1.483 +\        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                 \
   1.484  \        X : parts (sees Spy evs) --> Says B A X : set evs";
   1.485  by (hyp_subst_tac 1);
   1.486  by (analz_induct_tac 1);
   1.487 -by (REPEAT_FIRST (rtac impI));
   1.488  (*Fake: the Spy doesn't have the critical session key!*)
   1.489  by (REPEAT (rtac impI 1));
   1.490 -by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
   1.491 -by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
   1.492 +by (subgoal_tac 
   1.493 +    "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
   1.494 +by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.495  				     not_parts_not_analz]) 2);
   1.496  by (Fake_parts_insert_tac 1);
   1.497  qed_spec_mp "TrustServerFinished";
   1.498 @@ -562,56 +611,60 @@
   1.499    We don't assume B has received CERTIFICATE VERIFY, and an intruder could
   1.500    have changed A's identity in all other messages, so we can't be sure
   1.501    that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   1.502 -  to bind A's identify with M, then we could replace A' by A below.*)
   1.503 +  to bind A's identity with M, then we could replace A' by A below.*)
   1.504  goal thy
   1.505 - "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                     \
   1.506 -\        ==> Notes A {|Agent B, Nonce M|} : set evs -->              \
   1.507 -\            Crypt (serverK(NA,NB,M)) Y : parts (sees Spy evs)  -->  \
   1.508 -\            (EX A'. Says B A' (Crypt (serverK(NA,NB,M)) Y) : set evs)";
   1.509 + "!!evs. [| evs : tls;  A ~: lost;  B ~: lost;                 \
   1.510 +\           M = PRF(PMS,NA,NB) |]            \
   1.511 +\        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->              \
   1.512 +\            Crypt (serverK(Na,Nb,M)) Y : parts (sees Spy evs)  -->  \
   1.513 +\            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
   1.514 +by (hyp_subst_tac 1);
   1.515  by (analz_induct_tac 1);
   1.516  by (REPEAT_FIRST (rtac impI));
   1.517  (*Fake: the Spy doesn't have the critical session key!*)
   1.518 -by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
   1.519 -by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
   1.520 +by (subgoal_tac 
   1.521 +    "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
   1.522 +by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.523  				     not_parts_not_analz]) 2);
   1.524  by (Fake_parts_insert_tac 1);
   1.525  (*ServerFinished.  If the message is old then apply induction hypothesis...*)
   1.526  by (rtac conjI 1 THEN Blast_tac 2);
   1.527 -(*...otherwise delete induction hyp and use unicity of M.*)
   1.528 +(*...otherwise delete induction hyp and use unicity of PMS.*)
   1.529  by (thin_tac "?PP-->?QQ" 1);
   1.530  by (Step_tac 1);
   1.531 -by (subgoal_tac "Nonce M ~: analz (sees Spy evsa)" 1);
   1.532 -by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
   1.533 +by (subgoal_tac "Nonce PMS ~: analz (sees Spy evsSF)" 1);
   1.534 +by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
   1.535  by (blast_tac (!claset addSEs [MPair_parts]
   1.536  		       addDs  [Notes_Crypt_parts_sees,
   1.537  			       Says_imp_sees_Spy RS parts.Inj,
   1.538 -			       unique_M]) 1);
   1.539 +			       unique_PMS]) 1);
   1.540  qed_spec_mp "TrustServerMsg";
   1.541  
   1.542  
   1.543  (*** Protocol goal: if B receives any message encrypted with clientK
   1.544 -     then A has sent it, ASSUMING that A chose M.  Authentication is
   1.545 +     then A has sent it, ASSUMING that A chose PMS.  Authentication is
   1.546       assumed here; B cannot verify it.  But if the message is
   1.547       CLIENT FINISHED, then B can then check the quoted values XA, XB, etc.
   1.548  ***)
   1.549  goal thy
   1.550   "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                         \
   1.551 -\        ==> Notes A {|Agent B, Nonce M|} : set evs -->                  \
   1.552 -\            Crypt (clientK(NA,NB,M)) Y : parts (sees Spy evs) -->  \
   1.553 -\            Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs";
   1.554 +\  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   1.555 +\      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (sees Spy evs) -->  \
   1.556 +\      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   1.557  by (analz_induct_tac 1);
   1.558  by (REPEAT_FIRST (rtac impI));
   1.559  (*Fake: the Spy doesn't have the critical session key!*)
   1.560 -by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees Spy evsa)" 1);
   1.561 -by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
   1.562 +by (subgoal_tac 
   1.563 +    "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
   1.564 +by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.565  				     not_parts_not_analz]) 2);
   1.566  by (Fake_parts_insert_tac 1);
   1.567  (*ClientFinished.  If the message is old then apply induction hypothesis...*)
   1.568  by (step_tac (!claset delrules [conjI]) 1);
   1.569 -by (subgoal_tac "Nonce M ~: analz (sees Spy evsa)" 1);
   1.570 -by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
   1.571 +by (subgoal_tac "Nonce PMS ~: analz (sees Spy evsCF)" 1);
   1.572 +by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
   1.573  by (blast_tac (!claset addSEs [MPair_parts]
   1.574 -		       addDs  [Notes_unique_M]) 1);
   1.575 +		       addDs  [Notes_unique_PMS]) 1);
   1.576  qed_spec_mp "TrustClientMsg";
   1.577  
   1.578  
   1.579 @@ -620,14 +673,14 @@
   1.580       values XA, XB, etc.  Even this one requires A to be uncompromised.
   1.581   ***)
   1.582  goal thy
   1.583 - "!!evs. [| Says A' B (Crypt (clientK(NA,NB,M)) Y) : set evs;             \
   1.584 -\           Says B  A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
   1.585 + "!!evs. [| Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
   1.586 +\           Says B  A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}  \
   1.587  \             : set evs;                                                  \
   1.588  \           Says A'' B (Crypt (priK A)                                    \
   1.589 -\                       (Hash{|Nonce NB, certificate B KB, Nonce M|}))    \
   1.590 +\                       (Hash{|Nonce NB, certificate B KB, Nonce PMS|}))  \
   1.591  \             : set evs;                                                  \
   1.592  \        evs : tls;  A ~: lost;  B ~: lost |]                             \
   1.593 -\     ==> Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs";
   1.594 +\     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   1.595  by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
   1.596                         addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.597  qed "AuthClientFinished";
     2.1 --- a/src/HOL/Auth/TLS.thy	Fri Sep 12 10:45:51 1997 +0200
     2.2 +++ b/src/HOL/Auth/TLS.thy	Tue Sep 16 13:32:22 1997 +0200
     2.3 @@ -4,6 +4,12 @@
     2.4      Copyright   1997  University of Cambridge
     2.5  
     2.6  Inductive relation "tls" for the baby TLS (Transport Layer Security) protocol.
     2.7 +This protocol is essentially the same as SSL 3.0.
     2.8 +
     2.9 +Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
    2.10 +Allen, Transport Layer Security Working Group, 21 May 1997,
    2.11 +INTERNET-DRAFT draft-ietf-tls-protocol-03.txt.  Section numbers below refer
    2.12 +to that memo.
    2.13  
    2.14  An RSA cryptosystem is assumed, and X.509v3 certificates are abstracted down
    2.15  to the trivial form {A, publicKey(A)}privateKey(Server), where Server is a
    2.16 @@ -15,18 +21,14 @@
    2.17  The model assumes that no fraudulent certificates are present, but it does
    2.18  assume that some private keys are to the spy.
    2.19  
    2.20 -Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
    2.21 -Allen, Transport Layer Security Working Group, 21 May 1997,
    2.22 -INTERNET-DRAFT draft-ietf-tls-protocol-03.txt
    2.23 -
    2.24 -NOTE.  The event "Notes A {|Agent B, Nonce M|}" appears in ClientCertKeyEx,
    2.25 +REMARK.  The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientCertKeyEx,
    2.26  CertVerify, ClientFinished to record that A knows M.  It is a note from A to
    2.27  herself.  Nobody else can see it.  In ClientCertKeyEx, the Spy can substitute
    2.28  his own certificate for A's, but he cannot replace A's note by one for himself.
    2.29  
    2.30 -The note is needed because of a weakness in the public-key model.  Each
    2.31 +The Note event avoids a weakness in the public-key model.  Each
    2.32  agent's state is recorded as the trace of messages.  When the true client (A)
    2.33 -invents M, he encrypts M with B's public key before sending it.  The model
    2.34 +invents PMS, he encrypts PMS with B's public key before sending it.  The model
    2.35  does not distinguish the original occurrence of such a message from a replay.
    2.36  
    2.37  In the shared-key model, the ability to encrypt implies the ability to
    2.38 @@ -36,8 +38,12 @@
    2.39  TLS = Public + 
    2.40  
    2.41  consts
    2.42 -  (*Client, server write keys.  They implicitly include the MAC secrets.*)
    2.43 +  (*Pseudo-random function of Section 5*)
    2.44 +  PRF  :: "nat*nat*nat => nat"
    2.45 +
    2.46 +  (*Client, server write keys implicitly include the MAC secrets.*)
    2.47    clientK, serverK :: "nat*nat*nat => key"
    2.48 +
    2.49    certificate      :: "[agent,key] => msg"
    2.50  
    2.51  defs
    2.52 @@ -45,6 +51,8 @@
    2.53      "certificate A KA == Crypt (priK Server) {|Agent A, Key KA|}"
    2.54  
    2.55  rules
    2.56 +  inj_PRF       "inj PRF"	
    2.57 +
    2.58    (*clientK is collision-free and makes symmetric keys*)
    2.59    inj_clientK   "inj clientK"	
    2.60    isSym_clientK "isSymKey (clientK x)"	(*client write keys are symmetric*)
    2.61 @@ -68,95 +76,105 @@
    2.62               X: synth (analz (sees Spy evs)) |]
    2.63            ==> Says Spy B X # evs : tls"
    2.64  
    2.65 -    SpyKeys (*The spy may apply clientK & serverK to nonces he's found*)
    2.66 -         "[| evs: tls;
    2.67 -	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evs |]
    2.68 -          ==> Says Spy B {| Key (clientK(NA,NB,M)),
    2.69 -			    Key (serverK(NA,NB,M)) |} # evs : tls"
    2.70 +    SpyKeys (*The spy may apply PRF, clientK & serverK to available nonces*)
    2.71 +         "[| evsSK: tls;
    2.72 +	     Says Spy B {|Nonce NA, Nonce NB, Nonce M|} : set evsSK |]
    2.73 +          ==> Says Spy B {| Nonce (PRF(M,NA,NB)),
    2.74 +			    Key (clientK(NA,NB,M)),
    2.75 +			    Key (serverK(NA,NB,M)) |} # evsSK : tls"
    2.76  
    2.77      ClientHello
    2.78 -	 (*XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
    2.79 +	 (*(7.4.1.2)
    2.80 +	   XA represents CLIENT_VERSION, CIPHER_SUITES and COMPRESSION_METHODS.
    2.81  	   It is uninterpreted but will be confirmed in the FINISHED messages.
    2.82  	   As an initial simplification, SESSION_ID is identified with NA
    2.83 -           and reuse of sessions is not supported.*)
    2.84 -         "[| evs: tls;  A ~= B;  Nonce NA ~: used evs |]
    2.85 -          ==> Says A B {|Agent A, Nonce NA, Agent XA|} # evs  :  tls"
    2.86 +           and reuse of sessions is not supported.
    2.87 +           May assume NA ~: range PRF because CLIENT RANDOM is 32 bytes
    2.88 +	   while MASTER SECRET is 48 byptes (6.1)*)
    2.89 +         "[| evsCH: tls;  A ~= B;  Nonce NA ~: used evsCH;  NA ~: range PRF |]
    2.90 +          ==> Says A B {|Agent A, Nonce NA, Number XA|} # evsCH  :  tls"
    2.91  
    2.92      ServerHello
    2.93 -         (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    2.94 -	   NA is returned in its role as SESSION_ID.  A CERTIFICATE_REQUEST is
    2.95 -	   implied and a SERVER CERTIFICATE is always present.*)
    2.96 -         "[| evs: tls;  A ~= B;  Nonce NB ~: used evs;
    2.97 -             Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |]
    2.98 -          ==> Says B A {|Nonce NA, Nonce NB, Agent XB,
    2.99 +         (*7.4.1.3 of the TLS Internet-Draft
   2.100 +	   XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
   2.101 +	   NA is returned in its role as SESSION_ID.
   2.102 +           SERVER CERTIFICATE (7.4.2) is always present.
   2.103 +           CERTIFICATE_REQUEST (7.4.4) is implied.*)
   2.104 +         "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
   2.105 +             Says A' B {|Agent A, Nonce NA, Number XA|} : set evsSH |]
   2.106 +          ==> Says B A {|Nonce NA, Nonce NB, Number XB,
   2.107  			 certificate B (pubK B)|}
   2.108 -                # evs  :  tls"
   2.109 +                # evsSH  :  tls"
   2.110  
   2.111      ClientCertKeyEx
   2.112 -         (*CLIENT CERTIFICATE and KEY EXCHANGE.  The client, A, chooses M,
   2.113 -           the pre-master-secret.  She encrypts M using the supplied KB,
   2.114 -           which ought to be pubK B, and also with her own public key,
   2.115 -           to record in the trace that she knows M (see NOTE at top).*)
   2.116 -         "[| evs: tls;  A ~= B;  Nonce M ~: used evs;
   2.117 -             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
   2.118 -	       : set evs |]
   2.119 -          ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|}
   2.120 -	      # Notes A {|Agent B, Nonce M|}
   2.121 -	      # evs  :  tls"
   2.122 +         (*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7).
   2.123 +           The client, A, chooses PMS, the PREMASTER SECRET.
   2.124 +           She encrypts PMS using the supplied KB, which ought to be pubK B.
   2.125 +           We assume PMS ~: range PRF because a clash betweem the PMS
   2.126 +           and another MASTER SECRET is highly unlikely (even though
   2.127 +	   both items have the same length, 48 bytes).
   2.128 +           The Note event records in the trace that she knows PMS
   2.129 +               (see REMARK at top).*)
   2.130 +         "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
   2.131 +             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
   2.132 +	       : set evsCX |]
   2.133 +          ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
   2.134 +	      # Notes A {|Agent B, Nonce PMS|}
   2.135 +	      # evsCX  :  tls"
   2.136  
   2.137      CertVerify
   2.138 -	(*The optional CERTIFICATE VERIFY message contains the specific
   2.139 -          components listed in the security analysis, Appendix F.1.1.2;
   2.140 -          it also contains the pre-master-secret.  Checking the signature,
   2.141 -          which is the only use of A's certificate, assures B of A's presence*)
   2.142 -         "[| evs: tls;  A ~= B;  
   2.143 -             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
   2.144 -	       : set evs;
   2.145 -	     Notes A {|Agent B, Nonce M|} : set evs |]
   2.146 +	(*The optional CERTIFICATE VERIFY (7.4.8) message contains the
   2.147 +          specific components listed in the security analysis, F.1.1.2.
   2.148 +          It adds the pre-master-secret, which is also essential!
   2.149 +          Checking the signature, which is the only use of A's certificate,
   2.150 +          assures B of A's presence*)
   2.151 +         "[| evsCV: tls;  A ~= B;  
   2.152 +             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
   2.153 +	       : set evsCV;
   2.154 +	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
   2.155            ==> Says A B (Crypt (priK A)
   2.156 -			(Hash{|Nonce NB, certificate B KB, Nonce M|}))
   2.157 -                # evs  :  tls"
   2.158 +			(Hash{|Nonce NB, certificate B KB, Nonce PMS|}))
   2.159 +                # evsCV  :  tls"
   2.160  
   2.161 -	(*Finally come the FINISHED messages, confirming XA and XB among
   2.162 -          other things.  The master-secret is the hash of NA, NB and M.
   2.163 +	(*Finally come the FINISHED messages (7.4.8), confirming XA and XB
   2.164 +          among other things.  The master-secret is PRF(PMS,NA,NB).
   2.165            Either party may sent its message first.*)
   2.166  
   2.167 -        (*The occurrence of Crypt (pubK A) {|Agent B, Nonce M|} stops the 
   2.168 +        (*The occurrence of Notes A {|Agent B, Nonce PMS|} stops the 
   2.169            rule's applying when the Spy has satisfied the "Says A B" by
   2.170            repaying messages sent by the true client; in that case, the
   2.171 -          Spy does not know M and could not sent CLIENT FINISHED.  One
   2.172 +          Spy does not know PMS and could not sent CLIENT FINISHED.  One
   2.173            could simply put A~=Spy into the rule, but one should not
   2.174            expect the spy to be well-behaved.*)
   2.175      ClientFinished
   2.176 -         "[| evs: tls;  A ~= B;
   2.177 -	     Says A  B {|Agent A, Nonce NA, Agent XA|} : set evs;
   2.178 -             Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
   2.179 -	       : set evs;
   2.180 -             Notes A {|Agent B, Nonce M|} : set evs |]
   2.181 +         "[| evsCF: tls;  
   2.182 +	     Says A  B {|Agent A, Nonce NA, Number XA|} : set evsCF;
   2.183 +             Says B' A {|Nonce NA, Nonce NB, Number XB, certificate B KB|}
   2.184 +	       : set evsCF;
   2.185 +             Notes A {|Agent B, Nonce PMS|} : set evsCF;
   2.186 +	     M = PRF(PMS,NA,NB) |]
   2.187            ==> Says A B (Crypt (clientK(NA,NB,M))
   2.188 -			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
   2.189 -			       Nonce NA, Agent XA,
   2.190 -			       certificate A (pubK A), 
   2.191 -			       Nonce NB, Agent XB, Agent B|}))
   2.192 -                # evs  :  tls"
   2.193 +			(Hash{|Nonce M,
   2.194 +			       Nonce NA, Number XA, Agent A, 
   2.195 +			       Nonce NB, Number XB, Agent B|}))
   2.196 +                # evsCF  :  tls"
   2.197  
   2.198  	(*Keeping A' and A'' distinct means B cannot even check that the
   2.199 -          two messages originate from the same source.  B does not attempt
   2.200 -          to read A's encrypted "note to herself".*)
   2.201 +          two messages originate from the same source. *)
   2.202      ServerFinished
   2.203 -         "[| evs: tls;  A ~= B;
   2.204 -	     Says A' B  {|Agent A, Nonce NA, Agent XA|} : set evs;
   2.205 -	     Says B  A  {|Nonce NA, Nonce NB, Agent XB,
   2.206 +         "[| evsSF: tls;
   2.207 +	     Says A' B  {|Agent A, Nonce NA, Number XA|} : set evsSF;
   2.208 +	     Says B  A  {|Nonce NA, Nonce NB, Number XB,
   2.209  		 	  certificate B (pubK B)|}
   2.210 -	       : set evs;
   2.211 -	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce M)|}
   2.212 -	       : set evs |]
   2.213 +	       : set evsSF;
   2.214 +	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
   2.215 +	       : set evsSF;
   2.216 +	     M = PRF(PMS,NA,NB) |]
   2.217            ==> Says B A (Crypt (serverK(NA,NB,M))
   2.218 -			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
   2.219 -			       Nonce NA, Agent XA, Agent A, 
   2.220 -			       Nonce NB, Agent XB,
   2.221 -			       certificate B (pubK B)|}))
   2.222 -                # evs  :  tls"
   2.223 +			(Hash{|Nonce M,
   2.224 +			       Nonce NA, Number XA, Agent A, 
   2.225 +			       Nonce NB, Number XB, Agent B|}))
   2.226 +                # evsSF  :  tls"
   2.227  
   2.228    (**Oops message??**)
   2.229