Routine tidying up
authorpaulson
Fri Oct 03 10:32:50 1997 +0200 (1997-10-03)
changeset 37726ee707a73248
parent 3771 ede66fb99880
child 3773 989ef5e9d543
Routine tidying up
src/HOL/Auth/TLS.ML
     1.1 --- a/src/HOL/Auth/TLS.ML	Thu Oct 02 22:54:00 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Fri Oct 03 10:32:50 1997 +0200
     1.3 @@ -23,30 +23,8 @@
     1.4  proof_timing:=true;
     1.5  HOL_quantifiers := false;
     1.6  
     1.7 -(** We mostly DO NOT unfold the definition of "certificate".  The attached
     1.8 -    lemmas unfold it lazily, when "certificate B KB" occurs in appropriate
     1.9 -    contexts.
    1.10 -**)
    1.11 -
    1.12 -goalw thy [certificate_def] 
    1.13 -    "parts (insert (certificate B KB) H) =  \
    1.14 -\    parts (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
    1.15 -by (rtac refl 1);
    1.16 -qed "parts_insert_certificate";
    1.17 -
    1.18 -goalw thy [certificate_def] 
    1.19 -    "analz (insert (certificate B KB) H) =  \
    1.20 -\    analz (insert (Crypt (priK Server) {|Agent B, Key KB|}) H)";
    1.21 -by (rtac refl 1);
    1.22 -qed "analz_insert_certificate";
    1.23 -Addsimps [parts_insert_certificate, analz_insert_certificate];
    1.24 -
    1.25 -goalw thy [certificate_def] 
    1.26 -    "(X = certificate B KB) = (Crypt (priK Server) {|Agent B, Key KB|} = X)";
    1.27 -by (Blast_tac 1);
    1.28 -qed "eq_certificate_iff";
    1.29 -AddIffs [eq_certificate_iff];
    1.30 -
    1.31 +(*Automatically unfold the definition of "certificate"*)
    1.32 +Addsimps [certificate_def];
    1.33  
    1.34  (*Injectiveness of key-generating functions*)
    1.35  AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq];
    1.36 @@ -75,15 +53,14 @@
    1.37  
    1.38  (**** Protocol Proofs ****)
    1.39  
    1.40 -(*A "possibility property": there are traces that reach the end.
    1.41 -  This protocol has three end points and six messages to consider.*)
    1.42 +(*Possibility properties state that some traces run the protocol to the end.
    1.43 +  Four paths and 12 rules are considered.*)
    1.44  
    1.45  
    1.46 -(** These proofs make the further assumption that the Nonce_supply nonces 
    1.47 +(** These proofs assume that the Nonce_supply nonces 
    1.48  	(which have the form  @ N. Nonce N ~: used evs)
    1.49 -    lie outside the range of PRF.  This assumption seems reasonable, but
    1.50 -    as it is needed only for the possibility theorems, it is not taken
    1.51 -    as an axiom.
    1.52 +    lie outside the range of PRF.  It seems reasonable, but as it is needed
    1.53 +    only for the possibility theorems, it is not taken as an axiom.
    1.54  **)
    1.55  
    1.56  
    1.57 @@ -202,15 +179,17 @@
    1.58    little point in doing so: the loss of their private keys is a worse
    1.59    breach of security.*)
    1.60  goalw thy [certificate_def]
    1.61 - "!!evs. evs : tls ==> certificate B KB : parts (spies evs) --> KB = pubK B";
    1.62 + "!!evs. [| certificate B KB : parts (spies evs);  evs : tls |]  \
    1.63 +\        ==> pubK B = KB";
    1.64 +by (etac rev_mp 1);
    1.65  by (parts_induct_tac 1);
    1.66  by (Fake_parts_insert_tac 1);
    1.67 -bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
    1.68 +qed "certificate_valid";
    1.69  
    1.70  
    1.71  (*Replace key KB in ClientKeyExch by (pubK B) *)
    1.72  val ClientKeyExch_tac = 
    1.73 -    forward_tac [Says_imp_spies RS parts.Inj RS Server_cert_pubB]
    1.74 +    forward_tac [Says_imp_spies RS parts.Inj RS certificate_valid]
    1.75      THEN' assume_tac
    1.76      THEN' hyp_subst_tac;
    1.77  
    1.78 @@ -268,9 +247,9 @@
    1.79  
    1.80  (*B can check A's signature if he has received A's certificate.*)
    1.81  goal thy
    1.82 - "!!evs. [| X : parts (spies evs);          \
    1.83 -\           X = Crypt (priK A) (Hash{|nb, Agent B, pms|});      \
    1.84 -\           evs : tls;  A ~: bad |]                       \
    1.85 + "!!evs. [| X : parts (spies evs);                          \
    1.86 +\           X = Crypt (priK A) (Hash{|nb, Agent B, pms|});  \
    1.87 +\           evs : tls;  A ~: bad |]                         \
    1.88  \    ==> Says A B X : set evs";
    1.89  by (etac rev_mp 1);
    1.90  by (hyp_subst_tac 1);
    1.91 @@ -280,20 +259,20 @@
    1.92  
    1.93  (*Final version: B checks X using the distributed KA instead of priK A*)
    1.94  goal thy
    1.95 - "!!evs. [| X : parts (spies evs);          \
    1.96 -\           X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|});      \
    1.97 -\           certificate A KA : parts (spies evs);       \
    1.98 -\           evs : tls;  A ~: bad |]                       \
    1.99 + "!!evs. [| X : parts (spies evs);                            \
   1.100 +\           X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \
   1.101 +\           certificate A KA : parts (spies evs);             \
   1.102 +\           evs : tls;  A ~: bad |]                           \
   1.103  \    ==> Says A B X : set evs";
   1.104 -by (blast_tac (!claset addSDs [Server_cert_pubB] addSIs [lemma]) 1);
   1.105 +by (blast_tac (!claset addSDs [certificate_valid] addSIs [lemma]) 1);
   1.106  qed "TrustCertVerify";
   1.107  
   1.108  
   1.109  (*If CertVerify is present then A has chosen PMS.*)
   1.110  goal thy
   1.111 - "!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|})  \
   1.112 -\             : parts (spies evs);                                \
   1.113 -\           evs : tls;  A ~: bad |]                                      \
   1.114 + "!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \
   1.115 +\             : parts (spies evs);                          \
   1.116 +\           evs : tls;  A ~: bad |]                         \
   1.117  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
   1.118  be rev_mp 1;
   1.119  by (parts_induct_tac 1);
   1.120 @@ -302,83 +281,15 @@
   1.121  
   1.122  (*Final version using the distributed KA instead of priK A*)
   1.123  goal thy
   1.124 - "!!evs. [| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|})  \
   1.125 -\             : parts (spies evs);                                \
   1.126 -\           certificate A KA : parts (spies evs);       \
   1.127 -\           evs : tls;  A ~: bad |]                                      \
   1.128 + "!!evs. [| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}) \
   1.129 +\             : parts (spies evs);                             \
   1.130 +\           certificate A KA : parts (spies evs);              \
   1.131 +\           evs : tls;  A ~: bad |]                            \
   1.132  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
   1.133 -by (blast_tac (!claset addSDs [Server_cert_pubB] addSIs [lemma]) 1);
   1.134 +by (blast_tac (!claset addSDs [certificate_valid] addSIs [lemma]) 1);
   1.135  qed "UseCertVerify";
   1.136  
   1.137  
   1.138 -(*Key compromise lemma needed to prove analz_image_keys.
   1.139 -  No collection of keys can help the spy get new private keys.*)
   1.140 -goal thy  
   1.141 - "!!evs. evs : tls ==>                                    \
   1.142 -\  ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) =  \
   1.143 -\          (priK B : KK | B : bad)";
   1.144 -by (etac tls.induct 1);
   1.145 -by (ALLGOALS
   1.146 -    (asm_simp_tac (analz_image_keys_ss
   1.147 -		   addsimps (analz_insert_certificate::keys_distinct))));
   1.148 -(*Fake*) 
   1.149 -by (spy_analz_tac 2);
   1.150 -(*Base*)
   1.151 -by (Blast_tac 1);
   1.152 -qed_spec_mp "analz_image_priK";
   1.153 -
   1.154 -
   1.155 -(*slightly speeds up the big simplification below*)
   1.156 -goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
   1.157 -by (Blast_tac 1);
   1.158 -val range_sessionkeys_not_priK = result();
   1.159 -
   1.160 -(*Lemma for the trivial direction of the if-and-only-if*)
   1.161 -goal thy  
   1.162 - "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
   1.163 -\        (X : analz (G Un H))  =  (X : analz H)";
   1.164 -by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
   1.165 -val lemma = result();
   1.166 -
   1.167 -(** It is a mystery to me why the following formulation is actually slower
   1.168 -    in simplification:
   1.169 -
   1.170 -\    ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
   1.171 -\           (Nonce N : analz (spies evs))";
   1.172 -
   1.173 -More so as it can take advantage of unconditional rewrites such as 
   1.174 -     priK B ~: sessionK``Z
   1.175 -**)
   1.176 -
   1.177 -goal thy  
   1.178 - "!!evs. evs : tls ==>                                 \
   1.179 -\    ALL KK. KK <= range sessionK -->           \
   1.180 -\            (Nonce N : analz (Key``KK Un (spies evs))) = \
   1.181 -\            (Nonce N : analz (spies evs))";
   1.182 -by (etac tls.induct 1);
   1.183 -by (ClientKeyExch_tac 7);
   1.184 -by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.185 -by (REPEAT_FIRST (rtac lemma));
   1.186 -by (ALLGOALS    (*23 seconds*)
   1.187 -    (asm_simp_tac (analz_image_keys_ss 
   1.188 -		   addsimps [range_sessionkeys_not_priK, 
   1.189 -			     analz_image_priK, analz_insert_certificate])));
   1.190 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
   1.191 -(*Fake*) 
   1.192 -by (spy_analz_tac 2);
   1.193 -(*Base*)
   1.194 -by (Blast_tac 1);
   1.195 -qed_spec_mp "analz_image_keys";
   1.196 -
   1.197 -(*Knowing some session keys is no help in getting new nonces*)
   1.198 -goal thy
   1.199 - "!!evs. evs : tls ==>          \
   1.200 -\        Nonce N : analz (insert (Key (sessionK z)) (spies evs)) =  \
   1.201 -\        (Nonce N : analz (spies evs))";
   1.202 -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1);
   1.203 -qed "analz_insert_key";
   1.204 -Addsimps [analz_insert_key];
   1.205 -
   1.206  goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
   1.207  by (parts_induct_tac 1);
   1.208  (*ClientKeyExch: PMS is assumed to differ from any PRF.*)
   1.209 @@ -402,75 +313,6 @@
   1.210  
   1.211  
   1.212  
   1.213 -(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
   1.214 -
   1.215 -(** Some lemmas about session keys, comprising clientK and serverK **)
   1.216 -
   1.217 -
   1.218 -(*Lemma: session keys are never used if PMS is fresh.  
   1.219 -  Nonces don't have to agree, allowing session resumption.
   1.220 -  Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
   1.221 -  THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
   1.222 -goal thy 
   1.223 - "!!evs. [| Nonce PMS ~: parts (spies evs);  \
   1.224 -\           K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b);  \
   1.225 -\           evs : tls |]             \
   1.226 -\  ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
   1.227 -by (etac rev_mp 1);
   1.228 -by (hyp_subst_tac 1);
   1.229 -by (analz_induct_tac 1);
   1.230 -(*SpyKeys*)
   1.231 -by (blast_tac (!claset addSEs spies_partsEs) 3);
   1.232 -(*Fake*)
   1.233 -by (simp_tac (!simpset addsimps [parts_insert_spies]) 2);
   1.234 -by (Fake_parts_insert_tac 2);
   1.235 -(** LEVEL 6 **)
   1.236 -(*Oops*)
   1.237 -by (fast_tac (!claset addSEs [MPair_parts]
   1.238 -		       addDs  [Says_imp_spies RS parts.Inj]
   1.239 -		       addss (!simpset)) 6);
   1.240 -by (REPEAT 
   1.241 -    (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, 
   1.242 -				Notes_master_imp_Crypt_PMS]
   1.243 -                        addSEs spies_partsEs) 1));
   1.244 -val lemma = result();
   1.245 -
   1.246 -goal thy 
   1.247 - "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   1.248 -\  ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)";
   1.249 -by (blast_tac (!claset addDs [lemma]) 1);
   1.250 -qed "PMS_sessionK_not_spied";
   1.251 -
   1.252 -goal thy 
   1.253 - "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   1.254 -\  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
   1.255 -by (blast_tac (!claset addDs [lemma]) 1);
   1.256 -qed "PMS_Crypt_sessionK_not_spied";
   1.257 -
   1.258 -
   1.259 -(*Lemma: write keys are never sent if M (MASTER SECRET) is secure.  
   1.260 -  Converse doesn't hold; betraying M doesn't force the keys to be sent!
   1.261 -  The strong Oops condition can be weakened later by unicity reasoning, 
   1.262 -	with some effort.*)
   1.263 -goal thy 
   1.264 - "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
   1.265 -\           Nonce M ~: analz (spies evs);  evs : tls |]   \
   1.266 -\        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
   1.267 -by (etac rev_mp 1);
   1.268 -by (etac rev_mp 1);
   1.269 -by (analz_induct_tac 1);        (*17 seconds*)
   1.270 -(*Oops*)
   1.271 -by (Blast_tac 4);
   1.272 -(*SpyKeys*)
   1.273 -by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
   1.274 -(*Fake*) 
   1.275 -by (spy_analz_tac 2);
   1.276 -(*Base*)
   1.277 -by (Blast_tac 1);
   1.278 -qed "sessionK_not_spied";
   1.279 -Addsimps [sessionK_not_spied];
   1.280 -
   1.281 -
   1.282  (*** Unicity results for PMS, the pre-master-secret ***)
   1.283  
   1.284  (*PMS determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
   1.285 @@ -525,6 +367,144 @@
   1.286  
   1.287  
   1.288  
   1.289 +(**** Secrecy Theorems ****)
   1.290 +
   1.291 +(*Key compromise lemma needed to prove analz_image_keys.
   1.292 +  No collection of keys can help the spy get new private keys.*)
   1.293 +goal thy  
   1.294 + "!!evs. evs : tls ==>                                      \
   1.295 +\  ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
   1.296 +\          (priK B : KK | B : bad)";
   1.297 +by (etac tls.induct 1);
   1.298 +by (ALLGOALS
   1.299 +    (asm_simp_tac (analz_image_keys_ss
   1.300 +		   addsimps (certificate_def::keys_distinct))));
   1.301 +(*Fake*) 
   1.302 +by (spy_analz_tac 2);
   1.303 +(*Base*)
   1.304 +by (Blast_tac 1);
   1.305 +qed_spec_mp "analz_image_priK";
   1.306 +
   1.307 +
   1.308 +(*slightly speeds up the big simplification below*)
   1.309 +goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
   1.310 +by (Blast_tac 1);
   1.311 +val range_sessionkeys_not_priK = result();
   1.312 +
   1.313 +(*Lemma for the trivial direction of the if-and-only-if*)
   1.314 +goal thy  
   1.315 + "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
   1.316 +\        (X : analz (G Un H))  =  (X : analz H)";
   1.317 +by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
   1.318 +val lemma = result();
   1.319 +
   1.320 +(** Strangely, the following version doesn't work:
   1.321 +\    ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
   1.322 +\           (Nonce N : analz (spies evs))";
   1.323 +**)
   1.324 +
   1.325 +goal thy  
   1.326 + "!!evs. evs : tls ==>                                    \
   1.327 +\    ALL KK. KK <= range sessionK -->                     \
   1.328 +\            (Nonce N : analz (Key``KK Un (spies evs))) = \
   1.329 +\            (Nonce N : analz (spies evs))";
   1.330 +by (etac tls.induct 1);
   1.331 +by (ClientKeyExch_tac 7);
   1.332 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.333 +by (REPEAT_FIRST (rtac lemma));
   1.334 +by (ALLGOALS    (*24 seconds*)
   1.335 +    (asm_simp_tac (analz_image_keys_ss 
   1.336 +		   addsimps [range_sessionkeys_not_priK, 
   1.337 +                             analz_image_priK, certificate_def])));
   1.338 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
   1.339 +(*Fake*) 
   1.340 +by (spy_analz_tac 2);
   1.341 +(*Base*)
   1.342 +by (Blast_tac 1);
   1.343 +qed_spec_mp "analz_image_keys";
   1.344 +
   1.345 +(*Knowing some session keys is no help in getting new nonces*)
   1.346 +goal thy
   1.347 + "!!evs. evs : tls ==>          \
   1.348 +\        Nonce N : analz (insert (Key (sessionK z)) (spies evs)) =  \
   1.349 +\        (Nonce N : analz (spies evs))";
   1.350 +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 1);
   1.351 +qed "analz_insert_key";
   1.352 +Addsimps [analz_insert_key];
   1.353 +
   1.354 +
   1.355 +(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
   1.356 +
   1.357 +(** Some lemmas about session keys, comprising clientK and serverK **)
   1.358 +
   1.359 +
   1.360 +(*Lemma: session keys are never used if PMS is fresh.  
   1.361 +  Nonces don't have to agree, allowing session resumption.
   1.362 +  Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
   1.363 +  THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
   1.364 +goal thy 
   1.365 + "!!evs. [| Nonce PMS ~: parts (spies evs);  \
   1.366 +\           K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b);  \
   1.367 +\           evs : tls |]             \
   1.368 +\  ==> Key K ~: parts (spies evs) & (ALL Y. Crypt K Y ~: parts (spies evs))";
   1.369 +by (etac rev_mp 1);
   1.370 +by (hyp_subst_tac 1);
   1.371 +by (analz_induct_tac 1);
   1.372 +(*SpyKeys*)
   1.373 +by (blast_tac (!claset addSEs spies_partsEs) 3);
   1.374 +(*Fake*)
   1.375 +by (simp_tac (!simpset addsimps [parts_insert_spies]) 2);
   1.376 +by (Fake_parts_insert_tac 2);
   1.377 +(** LEVEL 6 **)
   1.378 +(*Oops*)
   1.379 +by (fast_tac (!claset addSEs [MPair_parts]
   1.380 +		       addDs  [Says_imp_spies RS parts.Inj]
   1.381 +		       addss (!simpset)) 6);
   1.382 +by (REPEAT 
   1.383 +    (blast_tac (!claset addSDs [Notes_Crypt_parts_spies, 
   1.384 +				Notes_master_imp_Crypt_PMS]
   1.385 +                        addSEs spies_partsEs) 1));
   1.386 +val lemma = result();
   1.387 +
   1.388 +goal thy 
   1.389 + "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   1.390 +\  ==> Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) ~: parts (spies evs)";
   1.391 +by (blast_tac (!claset addDs [lemma]) 1);
   1.392 +qed "PMS_sessionK_not_spied";
   1.393 +bind_thm ("PMS_sessionK_spiedE", 
   1.394 +	  PMS_sessionK_not_spied RSN (2,rev_notE));
   1.395 +
   1.396 +goal thy 
   1.397 + "!!evs. [| Nonce PMS ~: parts (spies evs);  evs : tls |]             \
   1.398 +\  ==> Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y ~: parts (spies evs)";
   1.399 +by (blast_tac (!claset addDs [lemma]) 1);
   1.400 +qed "PMS_Crypt_sessionK_not_spied";
   1.401 +bind_thm ("PMS_Crypt_sessionK_spiedE", 
   1.402 +	  PMS_Crypt_sessionK_not_spied RSN (2,rev_notE));
   1.403 +
   1.404 +(*Lemma: write keys are never sent if M (MASTER SECRET) is secure.  
   1.405 +  Converse doesn't hold; betraying M doesn't force the keys to be sent!
   1.406 +  The strong Oops condition can be weakened later by unicity reasoning, 
   1.407 +	with some effort.*)
   1.408 +goal thy 
   1.409 + "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
   1.410 +\           Nonce M ~: analz (spies evs);  evs : tls |]   \
   1.411 +\        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
   1.412 +by (etac rev_mp 1);
   1.413 +by (etac rev_mp 1);
   1.414 +by (analz_induct_tac 1);        (*17 seconds*)
   1.415 +(*Oops*)
   1.416 +by (Blast_tac 4);
   1.417 +(*SpyKeys*)
   1.418 +by (blast_tac (!claset addDs [Says_imp_spies RS analz.Inj]) 3);
   1.419 +(*Fake*) 
   1.420 +by (spy_analz_tac 2);
   1.421 +(*Base*)
   1.422 +by (Blast_tac 1);
   1.423 +qed "sessionK_not_spied";
   1.424 +Addsimps [sessionK_not_spied];
   1.425 +
   1.426 +
   1.427  (*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
   1.428  goal thy
   1.429   "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
   1.430 @@ -588,7 +568,7 @@
   1.431      (blast_tac (!claset addSDs [Notes_master_imp_Notes_PMS]
   1.432       	 	        addIs  [Notes_unique_PMS RS conjunct1]) 2));
   1.433  (*ClientKeyExch*)
   1.434 -by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
   1.435 +by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_spiedE]
   1.436  	               addSDs [Says_imp_spies RS parts.Inj]) 1);
   1.437  bind_thm ("Says_clientK_unique",
   1.438  	  result() RSN(2,rev_mp) RSN(2,rev_mp));
   1.439 @@ -610,8 +590,7 @@
   1.440  (*Oops*)
   1.441  by (blast_tac (!claset addIs [Says_clientK_unique]) 2);
   1.442  (*ClientKeyExch*)
   1.443 -by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
   1.444 -			       spies_partsEs)) 1);
   1.445 +by (blast_tac (!claset addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1);
   1.446  qed_spec_mp "clientK_Oops_ALL";
   1.447  
   1.448  
   1.449 @@ -636,7 +615,7 @@
   1.450  				Notes_Crypt_parts_spies,
   1.451  				Crypt_unique_PMS]) 2));
   1.452  (*ClientKeyExch*)
   1.453 -by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
   1.454 +by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_spiedE]
   1.455  	               addSDs [Says_imp_spies RS parts.Inj]) 1);
   1.456  bind_thm ("Says_serverK_unique",
   1.457  	  result() RSN(2,rev_mp) RSN(2,rev_mp));
   1.458 @@ -657,8 +636,7 @@
   1.459  (*Oops*)
   1.460  by (blast_tac (!claset addIs [Says_serverK_unique]) 2);
   1.461  (*ClientKeyExch*)
   1.462 -by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
   1.463 -			       spies_partsEs)) 1);
   1.464 +by (blast_tac (!claset addSEs (PMS_sessionK_spiedE::spies_partsEs)) 1);
   1.465  qed_spec_mp "serverK_Oops_ALL";
   1.466  
   1.467  
   1.468 @@ -670,16 +648,15 @@
   1.469  
   1.470  (*The mention of her name (A) in X assures A that B knows who she is.*)
   1.471  goal thy
   1.472 - "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   1.473 -\           X = Crypt (serverK(Na,Nb,M))                  \
   1.474 + "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
   1.475  \                 (Hash{|Number SID, Nonce M,             \
   1.476  \                        Nonce Na, Number PA, Agent A,    \
   1.477  \                        Nonce Nb, Number PB, Agent B|}); \
   1.478  \           M = PRF(PMS,NA,NB);                           \
   1.479 -\           evs : tls;  A ~: bad;  B ~: bad |]          \
   1.480 -\        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
   1.481 -\        X : parts (spies evs) --> Says B A X : set evs";
   1.482 -by (etac rev_mp 1);
   1.483 +\           evs : tls;  A ~: bad;  B ~: bad |]            \
   1.484 +\        ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \
   1.485 +\            Notes A {|Agent B, Nonce PMS|} : set evs --> \
   1.486 +\            X : parts (spies evs) --> Says B A X : set evs";
   1.487  by (hyp_subst_tac 1);
   1.488  by (analz_induct_tac 1);        (*22 seconds*)
   1.489  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   1.490 @@ -687,13 +664,13 @@
   1.491  by (ALLGOALS Clarify_tac);
   1.492  (*ClientKeyExch*)
   1.493  by (fast_tac  (*blast_tac gives PROOF FAILED*)
   1.494 -    (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
   1.495 +    (!claset addSEs [PMS_Crypt_sessionK_spiedE]) 2);
   1.496  (*Fake: the Spy doesn't have the critical session key!*)
   1.497  by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   1.498  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.499  				     not_parts_not_analz]) 2);
   1.500  by (Fake_parts_insert_tac 1);
   1.501 -val lemma = normalize_thm [RSspec, RSmp] (result());
   1.502 +val lemma = normalize_thm [RSmp] (result());
   1.503  
   1.504  (*Final version*)
   1.505  goal thy
   1.506 @@ -719,13 +696,11 @@
   1.507    that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
   1.508    to bind A's identity with PMS, then we could replace A' by A below.*)
   1.509  goal thy
   1.510 - "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   1.511 -\           evs : tls;  A ~: bad;  B ~: bad;                 \
   1.512 -\           M = PRF(PMS,NA,NB) |]            \
   1.513 -\        ==> Notes A {|Agent B, Nonce PMS|} : set evs -->              \
   1.514 + "!!evs. [| M = PRF(PMS,NA,NB);  evs : tls;  A ~: bad;  B ~: bad |]     \
   1.515 +\        ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \
   1.516 +\            Notes A {|Agent B, Nonce PMS|} : set evs -->              \
   1.517  \            Crypt (serverK(Na,Nb,M)) Y : parts (spies evs)  -->  \
   1.518  \            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
   1.519 -by (etac rev_mp 1);
   1.520  by (hyp_subst_tac 1);
   1.521  by (analz_induct_tac 1);	(*20 seconds*)
   1.522  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   1.523 @@ -740,13 +715,13 @@
   1.524  				Crypt_unique_PMS]) 3));
   1.525  (*ClientKeyExch*)
   1.526  by (blast_tac
   1.527 -    (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
   1.528 +    (!claset addSEs [PMS_Crypt_sessionK_spiedE]) 2);
   1.529  (*Fake: the Spy doesn't have the critical session key!*)
   1.530  by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   1.531  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.532  				     not_parts_not_analz]) 2);
   1.533  by (Fake_parts_insert_tac 1);
   1.534 -val lemma = normalize_thm [RSspec, RSmp] (result());
   1.535 +val lemma = normalize_thm [RSmp] (result());
   1.536  
   1.537  (*Final version*)
   1.538  goal thy
   1.539 @@ -758,7 +733,6 @@
   1.540  \        ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs";
   1.541  by (blast_tac (!claset addIs [lemma]
   1.542                         addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
   1.543 -
   1.544  qed_spec_mp "TrustServerMsg";
   1.545  
   1.546  
   1.547 @@ -770,11 +744,12 @@
   1.548  ***)
   1.549  
   1.550  goal thy
   1.551 - "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                         \
   1.552 -\  ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs) -->\
   1.553 -\      Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   1.554 -\      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) -->  \
   1.555 -\      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   1.556 + "!!evs. [| M = PRF(PMS,NA,NB);  evs : tls;  A ~: bad;  B ~: bad |] \
   1.557 +\    ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \
   1.558 +\        Notes A {|Agent B, Nonce PMS|} : set evs -->               \
   1.559 +\        Crypt (clientK(Na,Nb,M)) Y : parts (spies evs) -->         \
   1.560 +\        Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
   1.561 +by (hyp_subst_tac 1);
   1.562  by (analz_induct_tac 1);	(*15 seconds*)
   1.563  by (ALLGOALS Clarify_tac);
   1.564  (*ClientFinished, ClientResume: by unicity of PMS*)
   1.565 @@ -783,24 +758,25 @@
   1.566  	 	               addDs  [Notes_unique_PMS]) 3));
   1.567  (*ClientKeyExch*)
   1.568  by (fast_tac  (*blast_tac gives PROOF FAILED*)
   1.569 -    (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
   1.570 +    (!claset addSEs [PMS_Crypt_sessionK_spiedE]) 2);
   1.571  (*Fake: the Spy doesn't have the critical session key!*)
   1.572  by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   1.573  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.574  				     not_parts_not_analz]) 2);
   1.575  by (Fake_parts_insert_tac 1);
   1.576 -val lemma = normalize_thm [RSspec, RSmp] (result());
   1.577 +val lemma = normalize_thm [RSmp] (result());
   1.578  
   1.579  (*Final version*)
   1.580  goal thy
   1.581 - "!!evs. [| Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs);  \
   1.582 + "!!evs. [| M = PRF(PMS,NA,NB);                           \
   1.583 +\           Crypt (clientK(Na,Nb,M)) Y : parts (spies evs);  \
   1.584  \           Notes A {|Agent B, Nonce PMS|} : set evs;        \
   1.585 -\           Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;  \
   1.586 +\           Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;  \
   1.587  \           evs : tls;  A ~: bad;  B ~: bad |]                         \
   1.588 -\  ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   1.589 +\  ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
   1.590  by (blast_tac (!claset addIs [lemma]
   1.591                         addEs [clientK_Oops_ALL RSN(2, rev_notE)]) 1);
   1.592 -qed_spec_mp "TrustClientMsg";
   1.593 +qed "TrustClientMsg";
   1.594  
   1.595  
   1.596  
   1.597 @@ -809,13 +785,14 @@
   1.598       values PA, PB, etc.  Even this one requires A to be uncompromised.
   1.599   ***)
   1.600  goal thy
   1.601 - "!!evs. [| Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
   1.602 -\           Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
   1.603 + "!!evs. [| M = PRF(PMS,NA,NB);                           \
   1.604 +\           Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\
   1.605 +\           Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \
   1.606  \           certificate A KA : parts (spies evs);       \
   1.607  \           Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\
   1.608  \             : set evs;                                                  \
   1.609  \        evs : tls;  A ~: bad;  B ~: bad |]                             \
   1.610 -\     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   1.611 +\     ==> Says A B (Crypt (clientK(Na,Nb,M)) Y) : set evs";
   1.612  by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
   1.613                         addDs  [Says_imp_spies RS parts.Inj]) 1);
   1.614  qed "AuthClientFinished";