src/HOL/Auth/TLS.ML
changeset 3515 d8a71f6eaf40
parent 3506 a36e0a49d2cd
child 3519 ab0a9fbed4c0
     1.1 --- a/src/HOL/Auth/TLS.ML	Fri Jul 11 13:28:53 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Fri Jul 11 13:30:01 1997 +0200
     1.3 @@ -3,15 +3,6 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1997  University of Cambridge
     1.6  
     1.7 -The public-key model has a weakness, especially concerning anonymous sessions.
     1.8 -The Spy's state is recorded as the trace of message.  But if he himself is the
     1.9 -Client and invents M, then he encrypts M with B's public key before sending
    1.10 -it.  This message gives no evidence that the spy knows M, and yet the spy
    1.11 -actually chose M!  So, in any property concerning the secrecy of some item,
    1.12 -one must establish that the spy didn't choose the item.  Guarantees normally
    1.13 -assume that the other party is uncompromised (otherwise, one can prove
    1.14 -little).
    1.15 -
    1.16  Protocol goals: 
    1.17  * M, serverK(NA,NB,M) and clientK(NA,NB,M) will be known only to the two
    1.18       parties (though A is not necessarily authenticated).
    1.19 @@ -84,9 +75,9 @@
    1.20  by (Blast_tac 1);
    1.21  qed "clientK_neq_serverK";
    1.22  
    1.23 -val ths = [pubK_neq_clientK, pubK_neq_serverK, 
    1.24 -	   priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK];
    1.25 -AddIffs (ths @ (ths RL [not_sym]));
    1.26 +val keys_distinct = [pubK_neq_clientK, pubK_neq_serverK, 
    1.27 +		     priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK];
    1.28 +AddIffs (keys_distinct @ (keys_distinct RL [not_sym]));
    1.29  
    1.30  
    1.31  (**** Protocol Proofs ****)
    1.32 @@ -155,6 +146,7 @@
    1.33  \        ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)";
    1.34  by (etac tls.induct 1);
    1.35  by (prove_simple_subgoals_tac 1);
    1.36 +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 2);
    1.37  by (Fake_parts_insert_tac 1);
    1.38  qed "Spy_see_priK";
    1.39  Addsimps [Spy_see_priK];
    1.40 @@ -175,16 +167,56 @@
    1.41  AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
    1.42  
    1.43  
    1.44 +(*This lemma says that no false certificates exist.  One might extend the
    1.45 +  model to include bogus certificates for the lost agents, but there seems
    1.46 +  little point in doing so: the loss of their private keys is a worse
    1.47 +  breach of security.*)
    1.48 +goalw thy [certificate_def]
    1.49 + "!!evs. evs : tls     \
    1.50 +\        ==> certificate B KB : parts (sees lost Spy evs) --> KB = pubK B";
    1.51 +by (etac tls.induct 1);
    1.52 +by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if])));
    1.53 +by (Fake_parts_insert_tac 2);
    1.54 +by (Blast_tac 1);
    1.55 +bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
    1.56 +
    1.57 +
    1.58 +(*Replace key KB in ClientCertKeyEx by (pubK B) *)
    1.59 +val ClientCertKeyEx_tac = 
    1.60 +    forward_tac [Says_imp_sees_Spy' RS parts.Inj RS 
    1.61 +		 parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
    1.62 +    THEN' assume_tac
    1.63 +    THEN' hyp_subst_tac;
    1.64 +
    1.65 +fun analz_induct_tac i = 
    1.66 +    etac tls.induct i   THEN
    1.67 +    ClientCertKeyEx_tac  (i+7)  THEN	(*ClientFinished*)
    1.68 +    ClientCertKeyEx_tac  (i+6)  THEN	(*CertVerify*)
    1.69 +    ClientCertKeyEx_tac  (i+5)  THEN	(*ClientCertKeyEx*)
    1.70 +    rewrite_goals_tac  [certificate_def]  THEN
    1.71 +    ALLGOALS (asm_simp_tac 
    1.72 +              (!simpset addsimps [not_parts_not_analz]
    1.73 +                        setloop split_tac [expand_if]))  THEN
    1.74 +    (*Remove instances of pubK B:  the Spy already knows all public keys.
    1.75 +      Combining the two simplifier calls makes them run extremely slowly.*)
    1.76 +    ALLGOALS (asm_simp_tac 
    1.77 +              (!simpset addsimps [insert_absorb]
    1.78 +                        setloop split_tac [expand_if]));
    1.79 +
    1.80 +
    1.81 +(*** Hashing of nonces ***)
    1.82 +
    1.83  (*Every Nonce that's hashed is already in past traffic. *)
    1.84  goal thy "!!evs. [| Hash {|Nonce N, X|} : parts (sees lost Spy evs);  \
    1.85  \                   evs : tls |]  \
    1.86  \                ==> Nonce N : parts (sees lost Spy evs)";
    1.87  by (etac rev_mp 1);
    1.88  by (etac tls.induct 1);
    1.89 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
    1.90 -by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
    1.91 -		      addSEs partsEs) 1);
    1.92 -by (Fake_parts_insert_tac 1);
    1.93 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
    1.94 +			             setloop split_tac [expand_if])));
    1.95 +by (Fake_parts_insert_tac 2);
    1.96 +by (REPEAT (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
    1.97 +		               addSEs partsEs) 1));
    1.98  qed "Hash_imp_Nonce1";
    1.99  
   1.100  (*Lemma needed to prove Hash_Hash_imp_Nonce*)
   1.101 @@ -194,23 +226,36 @@
   1.102  \                ==> Nonce M : parts (sees lost Spy evs)";
   1.103  by (etac rev_mp 1);
   1.104  by (etac tls.induct 1);
   1.105 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   1.106 -by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.107 -		      addSEs partsEs) 1);
   1.108 -by (Fake_parts_insert_tac 1);
   1.109 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
   1.110 +			             setloop split_tac [expand_if])));
   1.111 +by (Fake_parts_insert_tac 2);
   1.112 +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.113 +		       addSEs partsEs) 1);
   1.114  qed "Hash_imp_Nonce2";
   1.115  AddSDs [Hash_imp_Nonce2];
   1.116  
   1.117 +
   1.118 +goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
   1.119 +\                ==> Crypt (pubK B) X : parts (sees lost Spy evs)";
   1.120 +by (etac rev_mp 1);
   1.121 +by (analz_induct_tac 1);
   1.122 +by (blast_tac (!claset addIs [parts_insertI]) 1);
   1.123 +qed "Notes_Crypt_parts_sees";
   1.124 +
   1.125 +
   1.126 +(*NEEDED??*)
   1.127  goal thy "!!evs. [| Hash {| Hash{|Nonce NA, Nonce NB, Nonce M|}, X |}  \
   1.128  \                      : parts (sees lost Spy evs);      \
   1.129  \                   evs : tls |]                         \
   1.130  \                ==> Nonce M : parts (sees lost Spy evs)";
   1.131  by (etac rev_mp 1);
   1.132  by (etac tls.induct 1);
   1.133 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   1.134 -by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.135 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]
   1.136 +			             setloop split_tac [expand_if])));
   1.137 +by (Fake_parts_insert_tac 2);
   1.138 +by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
   1.139 +			      Says_imp_sees_Spy' RS parts.Inj]
   1.140  		      addSEs partsEs) 1);
   1.141 -by (Fake_parts_insert_tac 1);
   1.142  qed "Hash_Hash_imp_Nonce";
   1.143  
   1.144  
   1.145 @@ -223,8 +268,9 @@
   1.146  \                ==> Nonce N : parts (sees lost Spy evs)";
   1.147  by (etac rev_mp 1);
   1.148  by (etac tls.induct 1);
   1.149 -by (ALLGOALS Asm_simp_tac);
   1.150 -by (step_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.151 +by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
   1.152 +by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
   1.153 +			      Says_imp_sees_Spy' RS parts.Inj]
   1.154  		      addSEs partsEs) 1);
   1.155  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
   1.156  by (Fake_parts_insert_tac 1);
   1.157 @@ -248,7 +294,7 @@
   1.158  \        X : parts (sees lost Spy evs) --> Says A B X : set evs";
   1.159  by (hyp_subst_tac 1);
   1.160  by (etac tls.induct 1);
   1.161 -by (ALLGOALS Asm_simp_tac);
   1.162 +by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
   1.163  by (Fake_parts_insert_tac 1);
   1.164  (*ServerHello: nonce NB cannot be in X because it's fresh!*)
   1.165  by (blast_tac (!claset addSDs [Hash_imp_Nonce1]
   1.166 @@ -256,68 +302,19 @@
   1.167  qed_spec_mp "TrustCertVerify";
   1.168  
   1.169  
   1.170 +(*If CERTIFICATE VERIFY is present then A has chosen M.*)
   1.171  goal thy
   1.172 - "!!evs. [| evs : tls;  A ~= Spy |]                                      \
   1.173 -\ ==> Says A B (Crypt (priK A)                                           \
   1.174 -\               (Hash{|Nonce NB, certificate B KB, Nonce M|})) : set evs \
   1.175 -\     --> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} : set evs";
   1.176 + "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, certificate B KB, Nonce M|})  \
   1.177 +\             : parts (sees lost Spy evs);                                \
   1.178 +\           evs : tls;  A ~: lost |]                                      \
   1.179 +\        ==> Notes A {|Agent B, Nonce M|} : set evs";
   1.180 +be rev_mp 1;
   1.181  by (etac tls.induct 1);
   1.182 -by (ALLGOALS Asm_full_simp_tac);
   1.183 -bind_thm ("UseCertVerify", result() RSN (2, rev_mp));
   1.184 -
   1.185 -
   1.186 -(*This lemma says that no false certificates exist.  One might extend the
   1.187 -  model to include bogus certificates for the lost agents, but there seems
   1.188 -  little point in doing so: the loss of their private keys is a worse
   1.189 -  breach of security.*)
   1.190 -goalw thy [certificate_def]
   1.191 - "!!evs. evs : tls     \
   1.192 -\        ==> certificate B KB : parts (sees lost Spy evs) --> KB = pubK B";
   1.193 -by (etac tls.induct 1);
   1.194 -by (ALLGOALS Asm_simp_tac);
   1.195 +by (ALLGOALS (asm_full_simp_tac (!simpset setloop split_tac [expand_if])));
   1.196  by (Fake_parts_insert_tac 2);
   1.197  by (Blast_tac 1);
   1.198 -bind_thm ("Server_cert_pubB", result() RSN (2, rev_mp));
   1.199 -
   1.200 -
   1.201 -(*Replace key KB in ClientCertKeyEx by (pubK B) *)
   1.202 -val ClientCertKeyEx_tac = 
   1.203 -    forward_tac [Says_imp_sees_Spy' RS parts.Inj RS 
   1.204 -		 parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
   1.205 -    THEN' assume_tac
   1.206 -    THEN' hyp_subst_tac;
   1.207 +qed "UseCertVerify";
   1.208  
   1.209 -fun analz_induct_tac i = 
   1.210 -    etac tls.induct i   THEN
   1.211 -    ClientCertKeyEx_tac  (i+5)  THEN
   1.212 -    ALLGOALS (asm_simp_tac 
   1.213 -              (!simpset addsimps [not_parts_not_analz]
   1.214 -                        setloop split_tac [expand_if]))  THEN
   1.215 -    (*Remove instances of pubK B:  the Spy already knows all public keys.
   1.216 -      Combining the two simplifier calls makes them run extremely slowly.*)
   1.217 -    ALLGOALS (asm_simp_tac 
   1.218 -              (!simpset addsimps [insert_absorb]
   1.219 -                        setloop split_tac [expand_if]));
   1.220 -
   1.221 -(*** Specialized rewriting for the analz_image_... theorems ***)
   1.222 -
   1.223 -goal thy "insert (Key K) H = Key `` {K} Un H";
   1.224 -by (Blast_tac 1);
   1.225 -qed "insert_Key_singleton";
   1.226 -
   1.227 -goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
   1.228 -by (Blast_tac 1);
   1.229 -qed "insert_Key_image";
   1.230 -
   1.231 -(*Reverse the normal simplification of "image" to build up (not break down)
   1.232 -  the set of keys.  Based on analz_image_freshK_ss, but simpler.*)
   1.233 -val analz_image_keys_ss = 
   1.234 -     !simpset delsimps [image_insert, image_Un]
   1.235 -              addsimps [image_insert RS sym, image_Un RS sym,
   1.236 -			rangeI, 
   1.237 -			insert_Key_singleton, 
   1.238 -			insert_Key_image, Un_assoc RS sym]
   1.239 -              setloop split_tac [expand_if];
   1.240  
   1.241  (*No collection of keys can help the spy get new private keys*)
   1.242  goal thy  
   1.243 @@ -325,7 +322,9 @@
   1.244  \  ALL KK. (Key(priK B) : analz (Key``KK Un (sees lost Spy evs))) =  \
   1.245  \            (priK B : KK | B : lost)";
   1.246  by (etac tls.induct 1);
   1.247 -by (ALLGOALS (asm_simp_tac analz_image_keys_ss));
   1.248 +by (ALLGOALS
   1.249 +    (asm_simp_tac (analz_image_keys_ss 
   1.250 +		   addsimps (certificate_def::keys_distinct))));
   1.251  (*Fake*) 
   1.252  by (spy_analz_tac 2);
   1.253  (*Base*)
   1.254 @@ -349,11 +348,14 @@
   1.255  by (etac tls.induct 1);
   1.256  by (ClientCertKeyEx_tac 6);
   1.257  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.258 -by (REPEAT_FIRST (rtac lemma ));
   1.259 -	(*SLOW: 30s!*)
   1.260 -by (ALLGOALS (asm_simp_tac analz_image_keys_ss));
   1.261 -by (ALLGOALS (asm_simp_tac
   1.262 -	      (!simpset addsimps [analz_image_priK, insert_absorb])));
   1.263 +by (REPEAT_FIRST (rtac lemma));
   1.264 +writeln"SLOW simplification: 50 secs!??";
   1.265 +by (ALLGOALS
   1.266 +    (asm_simp_tac (analz_image_keys_ss 
   1.267 +		   addsimps (analz_image_priK::certificate_def::
   1.268 +			     keys_distinct))));
   1.269 +by (ALLGOALS (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_priK])));
   1.270 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
   1.271  (*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*)
   1.272  by (Blast_tac 3);
   1.273  (*Fake*) 
   1.274 @@ -363,33 +365,37 @@
   1.275  qed_spec_mp "analz_image_keys";
   1.276  
   1.277  
   1.278 -(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.
   1.279 -  The assumption is A~=Spy, not A~:lost, since A doesn't use her private key
   1.280 -  here.*)
   1.281 -goalw thy [certificate_def]
   1.282 - "!!evs. [| evs : tls;  A~=Spy;  B ~: lost |]                        \
   1.283 -\        ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} \
   1.284 -\              : set evs  -->  Nonce M ~: analz (sees lost Spy evs)";
   1.285 +(*If A sends ClientCertKeyEx to an uncompromised B, then M will stay secret.*)
   1.286 +goal thy
   1.287 + "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
   1.288 +\        ==> Notes A {|Agent B, Nonce M|} : set evs  -->   \
   1.289 +\            Nonce M ~: analz (sees lost Spy evs)";
   1.290  by (analz_induct_tac 1);
   1.291  (*ClientHello*)
   1.292 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   1.293 +by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   1.294 +                               addSEs sees_Spy_partsEs) 3);
   1.295  (*SpyKeys*)
   1.296  by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   1.297  (*Fake*)
   1.298  by (spy_analz_tac 1);
   1.299  (*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   1.300  by (REPEAT (blast_tac (!claset addSEs partsEs
   1.301 -			       addDs  [impOfSubs analz_subset_parts,
   1.302 +			       addDs  [Notes_Crypt_parts_sees,
   1.303 +				       impOfSubs analz_subset_parts,
   1.304  				       Says_imp_sees_Spy' RS analz.Inj]) 1));
   1.305  bind_thm ("Spy_not_see_premaster_secret", result() RSN (2, rev_mp));
   1.306  
   1.307  
   1.308  (*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
   1.309  
   1.310 -(*The two proofs are identical*)
   1.311 +(** First, some lemmas about those write keys.  The proofs for serverK are 
   1.312 +    nearly identical to those for clientK. **)
   1.313 +
   1.314 +(*Lemma: those write keys are never sent if M is secure.  
   1.315 +  Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
   1.316 +
   1.317  goal thy 
   1.318 - "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  \
   1.319 -\           evs : tls |]                           \
   1.320 + "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]   \
   1.321  \        ==> Key (clientK(NA,NB,M)) ~: parts (sees lost Spy evs)";
   1.322  by (etac rev_mp 1);
   1.323  by (analz_induct_tac 1);
   1.324 @@ -402,9 +408,11 @@
   1.325  by (Blast_tac 1);
   1.326  qed "clientK_notin_parts";
   1.327  
   1.328 +Addsimps [clientK_notin_parts];
   1.329 +AddSEs [clientK_notin_parts RSN (2, rev_notE)];
   1.330 +
   1.331  goal thy 
   1.332 - "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  \
   1.333 -\           evs : tls |]                           \
   1.334 + "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]   \
   1.335  \        ==> Key (serverK(NA,NB,M)) ~: parts (sees lost Spy evs)";
   1.336  by (etac rev_mp 1);
   1.337  by (analz_induct_tac 1);
   1.338 @@ -417,65 +425,198 @@
   1.339  by (Blast_tac 1);
   1.340  qed "serverK_notin_parts";
   1.341  
   1.342 +Addsimps [serverK_notin_parts];
   1.343 +AddSEs [serverK_notin_parts RSN (2, rev_notE)];
   1.344 +
   1.345 +(*Lemma: those write keys are never used if M is fresh.  
   1.346 +  Converse doesn't hold; betraying M doesn't force the keys to be sent!
   1.347 +  NOT suitable as safe elim rules.*)
   1.348 +
   1.349 +goal thy 
   1.350 + "!!evs. [| Nonce M ~: used evs;  evs : tls |]                           \
   1.351 +\        ==> Crypt (clientK(NA,NB,M)) Y ~: parts (sees lost Spy evs)";
   1.352 +by (etac rev_mp 1);
   1.353 +by (analz_induct_tac 1);
   1.354 +(*ClientFinished: since M is fresh, a different instance of clientK was used.*)
   1.355 +by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   1.356 +                               addSEs sees_Spy_partsEs) 3);
   1.357 +by (Fake_parts_insert_tac 2);
   1.358 +(*Base*)
   1.359 +by (Blast_tac 1);
   1.360 +qed "Crypt_clientK_notin_parts";
   1.361 +
   1.362 +Addsimps [Crypt_clientK_notin_parts];
   1.363 +AddEs [Crypt_clientK_notin_parts RSN (2, rev_notE)];
   1.364 +
   1.365 +goal thy 
   1.366 + "!!evs. [| Nonce M ~: used evs;  evs : tls |]                           \
   1.367 +\        ==> Crypt (serverK(NA,NB,M)) Y ~: parts (sees lost Spy evs)";
   1.368 +by (etac rev_mp 1);
   1.369 +by (analz_induct_tac 1);
   1.370 +(*ServerFinished: since M is fresh, a different instance of serverK was used.*)
   1.371 +by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   1.372 +                               addSEs sees_Spy_partsEs) 3);
   1.373 +by (Fake_parts_insert_tac 2);
   1.374 +(*Base*)
   1.375 +by (Blast_tac 1);
   1.376 +qed "Crypt_serverK_notin_parts";
   1.377 +
   1.378 +Addsimps [Crypt_serverK_notin_parts];
   1.379 +AddEs [Crypt_serverK_notin_parts RSN (2, rev_notE)];
   1.380 +
   1.381 +
   1.382 +(*Weakening A~:lost to A~=Spy would complicate later uses of the rule*)
   1.383 +goal thy
   1.384 + "!!evs. [| Says A B {|certA, Crypt KB (Nonce M)|} : set evs;   \
   1.385 +\           A ~: lost;  evs : tls |] ==> KB = pubK B";
   1.386 +be rev_mp 1;
   1.387 +by (analz_induct_tac 1);
   1.388 +qed "A_Crypt_pubB";
   1.389 +
   1.390 +
   1.391 +(*** Unicity results for M, the pre-master-secret ***)
   1.392 +
   1.393 +(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ...
   1.394 +  It simplifies the proof by discarding needless information about
   1.395 +	analz (insert X (sees lost Spy evs)) 
   1.396 +*)
   1.397 +fun analz_mono_parts_induct_tac i = 
   1.398 +    etac tls.induct i           THEN 
   1.399 +    ClientCertKeyEx_tac  (i+5)  THEN	(*ClientCertKeyEx*)
   1.400 +    REPEAT_FIRST analz_mono_contra_tac;
   1.401 +
   1.402 +
   1.403 +(*M determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
   1.404 +goal thy 
   1.405 + "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]   \
   1.406 +\        ==> EX B'. ALL B.   \
   1.407 +\              Crypt (pubK B) (Nonce M) : parts (sees lost Spy evs) --> B=B'";
   1.408 +by (etac rev_mp 1);
   1.409 +by (analz_mono_parts_induct_tac 1);
   1.410 +by (prove_simple_subgoals_tac 1);
   1.411 +by (asm_simp_tac (!simpset addsimps [all_conj_distrib]
   1.412 +                           setloop split_tac [expand_if]) 2);
   1.413 +(*ClientCertKeyEx*)
   1.414 +by (expand_case_tac "M = ?y" 2 THEN
   1.415 +    REPEAT (blast_tac (!claset addSEs partsEs) 2));
   1.416 +by (Fake_parts_insert_tac 1);
   1.417 +val lemma = result();
   1.418 +
   1.419 +goal thy 
   1.420 + "!!evs. [| Crypt(pubK B)  (Nonce M) : parts (sees lost Spy evs); \
   1.421 +\           Crypt(pubK B') (Nonce M) : parts (sees lost Spy evs); \
   1.422 +\           Nonce M ~: analz (sees lost Spy evs);                 \
   1.423 +\           evs : tls |]                                          \
   1.424 +\        ==> B=B'";
   1.425 +by (prove_unique_tac lemma 1);
   1.426 +qed "unique_M";
   1.427 +
   1.428 +
   1.429 +(*In A's note to herself, M determines A and B.*)
   1.430 +goal thy 
   1.431 + "!!evs. [| Nonce M ~: analz (sees lost Spy evs);  evs : tls |]            \
   1.432 +\ ==> EX A' B'. ALL A B.                                                   \
   1.433 +\        Notes A {|Agent B, Nonce M|} : set evs --> A=A' & B=B'";
   1.434 +by (etac rev_mp 1);
   1.435 +by (analz_mono_parts_induct_tac 1);
   1.436 +by (prove_simple_subgoals_tac 1);
   1.437 +by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   1.438 +(*ClientCertKeyEx: if M is fresh, then it can't appear in Notes A X.*)
   1.439 +by (expand_case_tac "M = ?y" 1 THEN
   1.440 +    blast_tac (!claset addSDs [Notes_Crypt_parts_sees] addSEs partsEs) 1);
   1.441 +val lemma = result();
   1.442 +
   1.443 +goal thy 
   1.444 + "!!evs. [| Notes A  {|Agent B,  Nonce M|} : set evs;  \
   1.445 +\           Notes A' {|Agent B', Nonce M|} : set evs;  \
   1.446 +\           Nonce M ~: analz (sees lost Spy evs);      \
   1.447 +\           evs : tls |]                               \
   1.448 +\        ==> A=A' & B=B'";
   1.449 +by (prove_unique_tac lemma 1);
   1.450 +qed "Notes_unique_M";
   1.451 +
   1.452 +
   1.453  
   1.454  (*** Protocol goals: if A receives SERVER FINISHED, then B is present 
   1.455       and has used the quoted values XA, XB, etc.  Note that it is up to A
   1.456       to compare XA with what she originally sent.
   1.457  ***)
   1.458  
   1.459 -goalw thy [certificate_def]
   1.460 - "!!evs. [| X = Crypt (serverK(NA,NB,M))                            \
   1.461 -\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},       \
   1.462 -\                        Nonce NA, Agent XA, Agent A,               \
   1.463 +(*The mention of her name (A) in X assumes A that B knows who she is.*)
   1.464 +goal thy
   1.465 + "!!evs. [| X = Crypt (serverK(NA,NB,M))                                \
   1.466 +\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},           \
   1.467 +\                        Nonce NA, Agent XA, Agent A,                   \
   1.468  \                        Nonce NB, Agent XB, certificate B (pubK B)|}); \
   1.469 -\           evs : tls;  A~=Spy;  B ~: lost |]                       \
   1.470 -\    ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|} \
   1.471 -\          : set evs -->              \
   1.472 +\           evs : tls;  A ~: lost;  B ~: lost |]                        \
   1.473 +\        ==> Notes A {|Agent B, Nonce M|} : set evs -->                 \
   1.474  \        X : parts (sees lost Spy evs) --> Says B A X : set evs";
   1.475  by (hyp_subst_tac 1);
   1.476 -by (etac tls.induct 1);
   1.477 -by (ALLGOALS Asm_simp_tac);
   1.478 -(*ClientCertKeyEx: M isn't in the Hash because it's fresh!*)
   1.479 -by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce]
   1.480 -                       addSEs sees_Spy_partsEs) 2);
   1.481 +by (analz_induct_tac 1);
   1.482 +by (REPEAT_FIRST (rtac impI));
   1.483  (*Fake: the Spy doesn't have the critical session key!*)
   1.484  by (REPEAT (rtac impI 1));
   1.485  by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
   1.486  by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
   1.487 -				     serverK_notin_parts, 
   1.488  				     not_parts_not_analz]) 2);
   1.489  by (Fake_parts_insert_tac 1);
   1.490  qed_spec_mp "TrustServerFinished";
   1.491  
   1.492  
   1.493 -(*** Protocol goal: if B receives CLIENT FINISHED, then A has used the
   1.494 -     quoted values XA, XB, etc., which B can then check.  BUT NOTE:
   1.495 -     B has no way of knowing that A is the sender of CLIENT CERTIFICATE!
   1.496 +(*This version refers not to SERVER FINISHED but to any message from B.
   1.497 +  We don't assume B has received CERTIFICATE VERIFY, and an intruder could
   1.498 +  have changed A's identity in all other messages, so we can't be sure
   1.499 +  that B sends his message to A.*)
   1.500 +goal thy
   1.501 + "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                         \
   1.502 +\        ==> Notes A {|Agent B, Nonce M|} : set evs -->                  \
   1.503 +\            Crypt (serverK(NA,NB,M)) Y : parts (sees lost Spy evs)  --> \
   1.504 +\            (EX A'. Says B A' (Crypt (serverK(NA,NB,M)) Y) : set evs)";
   1.505 +by (analz_induct_tac 1);
   1.506 +by (REPEAT_FIRST (rtac impI));
   1.507 +(*Fake: the Spy doesn't have the critical session key!*)
   1.508 +by (subgoal_tac "Key (serverK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
   1.509 +by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
   1.510 +				     not_parts_not_analz]) 2);
   1.511 +by (Fake_parts_insert_tac 1);
   1.512 +(*ServerFinished.  If the message is old then apply induction hypothesis...*)
   1.513 +by (rtac conjI 1 THEN Blast_tac 2);
   1.514 +(*...otherwise delete induction hyp and use unicity of M.*)
   1.515 +by (thin_tac "?PP-->?QQ" 1);
   1.516 +by (Step_tac 1);
   1.517 +by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1);
   1.518 +by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
   1.519 +by (blast_tac (!claset addSEs [MPair_parts]
   1.520 +		       addDs  [Notes_Crypt_parts_sees,
   1.521 +			       Says_imp_sees_Spy' RS parts.Inj,
   1.522 +			       unique_M]) 1);
   1.523 +qed_spec_mp "TrustServerMsg";
   1.524 +
   1.525 +
   1.526 +(*** Protocol goal: if B receives any message encrypted with clientK
   1.527 +     then A has sent it, ASSUMING that A chose M.  Authentication is
   1.528 +     assumed here; B cannot verify it.  But if the message is
   1.529 +     CLIENT FINISHED, then B can then check the quoted values XA, XB, etc.
   1.530  ***)
   1.531 -goalw thy [certificate_def]
   1.532 - "!!evs. [| X = Crypt (clientK(NA,NB,M))                        \
   1.533 -\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
   1.534 -\                        Nonce NA, Agent XA,                    \
   1.535 -\                        certificate A (pubK A),                \
   1.536 -\                        Nonce NB, Agent XB, Agent B|});        \
   1.537 -\           evs : tls;  A~=Spy;  B ~: lost |]                   \
   1.538 -\     ==> Says A B {|certificate A (pubK A),                    \
   1.539 -\                    Crypt KB (Nonce M)|} : set evs -->         \
   1.540 -\         X : parts (sees lost Spy evs) --> Says A B X : set evs";
   1.541 -by (hyp_subst_tac 1);
   1.542 -by (etac tls.induct 1);
   1.543 -by (ALLGOALS Asm_simp_tac);
   1.544 -(*ClientCertKeyEx: M isn't in the Hash because it's fresh!*)
   1.545 -by (blast_tac (!claset addSDs [Hash_Hash_imp_Nonce]
   1.546 -                       addSEs sees_Spy_partsEs) 2);
   1.547 +goal thy
   1.548 + "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]                         \
   1.549 +\        ==> Notes A {|Agent B, Nonce M|} : set evs -->                  \
   1.550 +\            Crypt (clientK(NA,NB,M)) Y : parts (sees lost Spy evs) -->  \
   1.551 +\            Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs";
   1.552 +by (analz_induct_tac 1);
   1.553 +by (REPEAT_FIRST (rtac impI));
   1.554  (*Fake: the Spy doesn't have the critical session key!*)
   1.555 -by (REPEAT (rtac impI 1));
   1.556  by (subgoal_tac "Key (clientK(NA,NB,M)) ~: analz (sees lost Spy evsa)" 1);
   1.557  by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret, 
   1.558 -				     clientK_notin_parts, 
   1.559  				     not_parts_not_analz]) 2);
   1.560  by (Fake_parts_insert_tac 1);
   1.561 -qed_spec_mp "TrustClientFinished";
   1.562 +(*ClientFinished.  If the message is old then apply induction hypothesis...*)
   1.563 +by (step_tac (!claset delrules [conjI]) 1);
   1.564 +by (subgoal_tac "Nonce M ~: analz (sees lost Spy evsa)" 1);
   1.565 +by (asm_simp_tac (!simpset addsimps [Spy_not_see_premaster_secret]) 2);
   1.566 +by (blast_tac (!claset addSEs [MPair_parts]
   1.567 +		       addDs  [Notes_unique_M]) 1);
   1.568 +qed_spec_mp "TrustClientMsg";
   1.569  
   1.570  
   1.571  (*** Protocol goal: if B receives CLIENT FINISHED, and if B is able to
   1.572 @@ -483,22 +624,14 @@
   1.573       values XA, XB, etc.  Even this one requires A to be uncompromised.
   1.574   ***)
   1.575  goal thy
   1.576 - "!!evs. [| X = Crypt (clientK(NA,NB,M))                        \
   1.577 -\                 (Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},   \
   1.578 -\                        Nonce NA, Agent XA,                    \
   1.579 -\                        certificate A (pubK A),                \
   1.580 -\                        Nonce NB, Agent XB, Agent B|});        \
   1.581 -\           Says A' B X : set evs;                              \
   1.582 -\           Says B A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
   1.583 -\             : set evs;                                        \
   1.584 -\           Says A'' B (Crypt (priK A)                                   \
   1.585 -\                       (Hash{|Nonce NB, certificate B KB, Nonce M|}))   \
   1.586 -\             : set evs;                                        \
   1.587 -\        evs : tls;  A ~: lost;  B ~: lost |]                   \
   1.588 -\     ==> Says A B X : set evs";
   1.589 -br TrustClientFinished 1;
   1.590 -br (TrustCertVerify RS UseCertVerify) 5;
   1.591 -by (REPEAT_FIRST (ares_tac [refl]));
   1.592 -by (ALLGOALS 
   1.593 -    (asm_full_simp_tac (!simpset addsimps [Says_imp_sees_Spy RS parts.Inj])));
   1.594 -qed_spec_mp "AuthClientFinished";
   1.595 + "!!evs. [| Says A' B (Crypt (clientK(NA,NB,M)) Y) : set evs;             \
   1.596 +\           Says B  A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}  \
   1.597 +\             : set evs;                                                  \
   1.598 +\           Says A'' B (Crypt (priK A)                                    \
   1.599 +\                       (Hash{|Nonce NB, certificate B KB, Nonce M|}))    \
   1.600 +\             : set evs;                                                  \
   1.601 +\        evs : tls;  A ~: lost;  B ~: lost |]                             \
   1.602 +\     ==> Says A B (Crypt (clientK(NA,NB,M)) Y) : set evs";
   1.603 +by (blast_tac (!claset addSIs [TrustClientMsg, UseCertVerify]
   1.604 +                       addDs  [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.605 +qed "AuthClientFinished";