Now uses the Notes constructor to distinguish the Client (who has chosen M)
authorpaulson
Fri Jul 11 13:30:01 1997 +0200 (1997-07-11)
changeset 3515d8a71f6eaf40
parent 3514 eb16b8e8d872
child 3516 470626799511
Now uses the Notes constructor to distinguish the Client (who has chosen M)
from the Spy (who may have replayed her messages)
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     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";
     2.1 --- a/src/HOL/Auth/TLS.thy	Fri Jul 11 13:28:53 1997 +0200
     2.2 +++ b/src/HOL/Auth/TLS.thy	Fri Jul 11 13:30:01 1997 +0200
     2.3 @@ -18,6 +18,19 @@
     2.4  Abstracted from "The TLS Protocol, Version 1.0" by Tim Dierks and Christopher
     2.5  Allen, Transport Layer Security Working Group, 21 May 1997,
     2.6  INTERNET-DRAFT draft-ietf-tls-protocol-03.txt
     2.7 +
     2.8 +NOTE.  The event "Notes A {|Agent B, Nonce M|}" appears in ClientCertKeyEx,
     2.9 +CertVerify, ClientFinished to record that A knows M.  It is a note from A to
    2.10 +herself.  Nobody else can see it.  In ClientCertKeyEx, the Spy can substitute
    2.11 +his own certificate for A's, but he cannot replace A's note by one for himself.
    2.12 +
    2.13 +The note is needed because of a weakness in the public-key model.  Each
    2.14 +agent's state is recorded as the trace of messages.  When the true client (A)
    2.15 +invents M, he encrypts M with B's public key before sending it.  The model
    2.16 +does not distinguish the original occurrence of such a message from a replay.
    2.17 +
    2.18 +In the shared-key model, the ability to encrypt implies the ability to
    2.19 +decrypt, so the problem does not arise.
    2.20  *)
    2.21  
    2.22  TLS = Public + 
    2.23 @@ -77,7 +90,7 @@
    2.24  
    2.25      ServerHello
    2.26           (*XB represents CLIENT_VERSION, CIPHER_SUITE and COMPRESSION_METHOD.
    2.27 -	   Na is returned in its role as SESSION_ID.  A CERTIFICATE_REQUEST is
    2.28 +	   NA is returned in its role as SESSION_ID.  A CERTIFICATE_REQUEST is
    2.29  	   implied and a SERVER CERTIFICATE is always present.*)
    2.30           "[| evs: tls;  A ~= B;  Nonce NB ~: used evs;
    2.31               Says A' B {|Agent A, Nonce NA, Agent XA|} : set evs |]
    2.32 @@ -86,13 +99,16 @@
    2.33                  # evs  :  tls"
    2.34  
    2.35      ClientCertKeyEx
    2.36 -         (*CLIENT CERTIFICATE and KEY EXCHANGE.  M is the pre-master-secret.
    2.37 -           Note that A encrypts using the supplied KB, not pubK B.*)
    2.38 +         (*CLIENT CERTIFICATE and KEY EXCHANGE.  The client, A, chooses M,
    2.39 +           the pre-master-secret.  She encrypts M using the supplied KB,
    2.40 +           which ought to be pubK B, and also with her own public key,
    2.41 +           to record in the trace that she knows M (see NOTE at top).*)
    2.42           "[| evs: tls;  A ~= B;  Nonce M ~: used evs;
    2.43               Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
    2.44  	       : set evs |]
    2.45            ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|}
    2.46 -                # evs  :  tls"
    2.47 +	      # Notes A {|Agent B, Nonce M|}
    2.48 +	      # evs  :  tls"
    2.49  
    2.50      CertVerify
    2.51  	(*The optional CERTIFICATE VERIFY message contains the specific
    2.52 @@ -102,8 +118,7 @@
    2.53           "[| evs: tls;  A ~= B;  
    2.54               Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
    2.55  	       : set evs;
    2.56 -	     Says A B {|certificate A (pubK A), Crypt KB (Nonce M)|}
    2.57 -	       : set evs |]
    2.58 +	     Notes A {|Agent B, Nonce M|} : set evs |]
    2.59            ==> Says A B (Crypt (priK A)
    2.60  			(Hash{|Nonce NB, certificate B KB, Nonce M|}))
    2.61                  # evs  :  tls"
    2.62 @@ -112,13 +127,18 @@
    2.63            other things.  The master-secret is the hash of NA, NB and M.
    2.64            Either party may sent its message first.*)
    2.65  
    2.66 +        (*The occurrence of Crypt (pubK A) {|Agent B, Nonce M|} stops the 
    2.67 +          rule's applying when the Spy has satisfied the "Says A B" by
    2.68 +          repaying messages sent by the true client; in that case, the
    2.69 +          Spy does not know M and could not sent CLIENT FINISHED.  One
    2.70 +          could simply put A~=Spy into the rule, but one should not
    2.71 +          expect the spy to be well-behaved.*)
    2.72      ClientFinished
    2.73           "[| evs: tls;  A ~= B;
    2.74  	     Says A  B {|Agent A, Nonce NA, Agent XA|} : set evs;
    2.75               Says B' A {|Nonce NA, Nonce NB, Agent XB, certificate B KB|}
    2.76  	       : set evs;
    2.77 -             Says A  B {|certificate A (pubK A), Crypt KB (Nonce M)|}
    2.78 -	       : set evs |]
    2.79 +             Notes A {|Agent B, Nonce M|} : set evs |]
    2.80            ==> Says A B (Crypt (clientK(NA,NB,M))
    2.81  			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
    2.82  			       Nonce NA, Agent XA,
    2.83 @@ -127,15 +147,16 @@
    2.84                  # evs  :  tls"
    2.85  
    2.86  	(*Keeping A' and A'' distinct means B cannot even check that the
    2.87 -          two messages originate from the same source.*)
    2.88 -
    2.89 +          two messages originate from the same source.  B does not attempt
    2.90 +          to read A's encrypted "note to herself".*)
    2.91      ServerFinished
    2.92           "[| evs: tls;  A ~= B;
    2.93  	     Says A' B  {|Agent A, Nonce NA, Agent XA|} : set evs;
    2.94  	     Says B  A  {|Nonce NA, Nonce NB, Agent XB,
    2.95  		 	  certificate B (pubK B)|}
    2.96  	       : set evs;
    2.97 -	     Says A'' B {|CERTA, Crypt (pubK B) (Nonce M)|} : set evs |]
    2.98 +	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce M)|}
    2.99 +	       : set evs |]
   2.100            ==> Says B A (Crypt (serverK(NA,NB,M))
   2.101  			(Hash{|Hash{|Nonce NA, Nonce NB, Nonce M|},
   2.102  			       Nonce NA, Agent XA, Agent A,