Client, Server certificates now sent using the separate Certificate rule,
authorpaulson
Tue Sep 30 11:03:55 1997 +0200 (1997-09-30)
changeset 37454c5d3b1ddc75
parent 3744 9921561ade57
child 3746 e832a36121ab
Client, Server certificates now sent using the separate Certificate rule,
simplifying ServerHello and ClientKeyExch. Resumption no longer needs its
own version of ServerHello. Proofs run nearly three minutes faster.
src/HOL/Auth/TLS.ML
src/HOL/Auth/TLS.thy
     1.1 --- a/src/HOL/Auth/TLS.ML	Mon Sep 29 15:39:28 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Tue Sep 30 11:03:55 1997 +0200
     1.3 @@ -93,8 +93,9 @@
     1.4  \           A ~= B |] ==> EX SID M. EX evs: tls.    \
     1.5  \  Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
     1.6  by (REPEAT (resolve_tac [exI,bexI] 1));
     1.7 -by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
     1.8 -	RS tls.ClientFinished RS tls.ServerFinished RS tls.ClientAccepts) 2);
     1.9 +by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
    1.10 +	  tls.ClientKeyExch RS tls.ClientFinished RS tls.ServerFinished RS
    1.11 +	  tls.ClientAccepts) 2);
    1.12  by possibility_tac;
    1.13  by (REPEAT (Blast_tac 1));
    1.14  result();
    1.15 @@ -105,8 +106,9 @@
    1.16  \           A ~= B |] ==> EX SID NA PA NB PB M. EX evs: tls.    \
    1.17  \  Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs";
    1.18  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.19 -by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.20 -	  RS tls.ServerFinished RS tls.ClientFinished RS tls.ServerAccepts) 2);
    1.21 +by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
    1.22 +	  tls.ClientKeyExch RS tls.ServerFinished RS tls.ClientFinished RS
    1.23 +	  tls.ServerAccepts) 2);
    1.24  by possibility_tac;
    1.25  by (REPEAT (Blast_tac 1));
    1.26  result();
    1.27 @@ -117,8 +119,8 @@
    1.28  \           A ~= B |] ==> EX NB PMS. EX evs: tls.   \
    1.29  \  Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})) : set evs";
    1.30  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.31 -by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.ClientCertKeyEx
    1.32 -	  RS tls.CertVerify) 2);
    1.33 +by (rtac (tls.Nil RS tls.ClientHello RS tls.ServerHello RS tls.Certificate RS
    1.34 +	  tls.ClientKeyExch RS tls.CertVerify) 2);
    1.35  by possibility_tac;
    1.36  by (REPEAT (Blast_tac 1));
    1.37  result();
    1.38 @@ -135,7 +137,8 @@
    1.39  \                   Nonce NA, Number PA, Agent A,      \
    1.40  \                   Nonce NB, Number PB, Agent B|})) : set evs";
    1.41  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.42 -by (etac (tls.ClientHello RS tls.ServerResume RS tls.ClientResume) 2);
    1.43 +by (etac (tls.ClientHello RS tls.ServerHello RS tls.ServerResume RS 
    1.44 +	  tls.ClientResume) 2);
    1.45  by possibility_tac;
    1.46  by (REPEAT (Blast_tac 1));
    1.47  result();
    1.48 @@ -182,8 +185,7 @@
    1.49  qed "Spy_analz_priK";
    1.50  Addsimps [Spy_analz_priK];
    1.51  
    1.52 -goal thy  "!!A. [| Key (priK A) : parts (spies evs);       \
    1.53 -\                  evs : tls |] ==> A:bad";
    1.54 +goal thy  "!!A. [| Key (priK A) : parts (spies evs);  evs : tls |] ==> A:bad";
    1.55  by (blast_tac (!claset addDs [Spy_see_priK]) 1);
    1.56  qed "Spy_see_priK_D";
    1.57  
    1.58 @@ -196,25 +198,21 @@
    1.59    little point in doing so: the loss of their private keys is a worse
    1.60    breach of security.*)
    1.61  goalw thy [certificate_def]
    1.62 - "!!evs. evs : tls     \
    1.63 -\        ==> certificate B KB : parts (spies evs) --> KB = pubK B";
    1.64 + "!!evs. evs : tls ==> certificate B KB : parts (spies evs) --> KB = pubK B";
    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  
    1.69  
    1.70 -(*Replace key KB in ClientCertKeyEx by (pubK B) *)
    1.71 -val ClientCertKeyEx_tac = 
    1.72 -    forward_tac [Says_imp_spies RS parts.Inj RS 
    1.73 -		 parts.Snd RS parts.Snd RS parts.Snd RS Server_cert_pubB]
    1.74 +(*Replace key KB in ClientKeyExch by (pubK B) *)
    1.75 +val ClientKeyExch_tac = 
    1.76 +    forward_tac [Says_imp_spies RS parts.Inj RS Server_cert_pubB]
    1.77      THEN' assume_tac
    1.78      THEN' hyp_subst_tac;
    1.79  
    1.80  fun analz_induct_tac i = 
    1.81      etac tls.induct i   THEN
    1.82 -    ClientCertKeyEx_tac  (i+7)  THEN	(*ClientFinished*)
    1.83 -    ClientCertKeyEx_tac  (i+6)  THEN	(*CertVerify*)
    1.84 -    ClientCertKeyEx_tac  (i+5)  THEN	(*ClientCertKeyEx*)
    1.85 +    ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
    1.86      ALLGOALS (asm_simp_tac 
    1.87                (!simpset addcongs [if_weak_cong]
    1.88                          setloop split_tac [expand_if]))  THEN
    1.89 @@ -295,34 +293,48 @@
    1.90  
    1.91  (*** Protocol goal: if B receives CertVerify, then A sent it ***)
    1.92  
    1.93 -(*B can check A's signature if he has received A's certificate.
    1.94 -  Perhaps B~=Spy is unnecessary, but there's no obvious proof if the first
    1.95 -  message is Fake.  We don't need guarantees for the Spy anyway.  We must
    1.96 -  assume A~:bad; otherwise, the Spy can forge A's signature.*)
    1.97 +(*B can check A's signature if he has received A's certificate.*)
    1.98  goal thy
    1.99 - "!!evs. [| X = Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|});      \
   1.100 -\           evs : tls;  A ~: bad;  B ~= Spy |]                       \
   1.101 -\    ==> Says B A {|Nonce NB, Number SID, Number PB, certificate B KB|}  \
   1.102 -\          : set evs --> \
   1.103 -\        X : parts (spies evs) --> Says A B X : set evs";
   1.104 + "!!evs. [| X : parts (spies evs);          \
   1.105 +\           X = Crypt (priK A) (Hash{|nb, Agent B, pms|});      \
   1.106 +\           evs : tls;  A ~: bad |]                       \
   1.107 +\    ==> Says A B X : set evs";
   1.108 +by (etac rev_mp 1);
   1.109  by (hyp_subst_tac 1);
   1.110  by (parts_induct_tac 1);
   1.111  by (Fake_parts_insert_tac 1);
   1.112 -(*ServerHello: nonce NB cannot be in X because it's fresh!*)
   1.113 -by (blast_tac (!claset addSDs [Hash_Nonce_CV]
   1.114 -	               addSEs spies_partsEs) 1);
   1.115 -qed_spec_mp "TrustCertVerify";
   1.116 +val lemma = result();
   1.117 +
   1.118 +(*Final version: B checks X using the distributed KA instead of priK A*)
   1.119 +goal thy
   1.120 + "!!evs. [| X : parts (spies evs);          \
   1.121 +\           X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|});      \
   1.122 +\           certificate A KA : parts (spies evs);       \
   1.123 +\           evs : tls;  A ~: bad |]                       \
   1.124 +\    ==> Says A B X : set evs";
   1.125 +by (blast_tac (!claset addSDs [Server_cert_pubB] addSIs [lemma]) 1);
   1.126 +qed "TrustCertVerify";
   1.127  
   1.128  
   1.129  (*If CertVerify is present then A has chosen PMS.*)
   1.130  goal thy
   1.131 - "!!evs. [| Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|})  \
   1.132 + "!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|})  \
   1.133  \             : parts (spies evs);                                \
   1.134  \           evs : tls;  A ~: bad |]                                      \
   1.135  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
   1.136  be rev_mp 1;
   1.137  by (parts_induct_tac 1);
   1.138  by (Fake_parts_insert_tac 1);
   1.139 +val lemma = result();
   1.140 +
   1.141 +(*Final version using the distributed KA instead of priK A*)
   1.142 +goal thy
   1.143 + "!!evs. [| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|})  \
   1.144 +\             : parts (spies evs);                                \
   1.145 +\           certificate A KA : parts (spies evs);       \
   1.146 +\           evs : tls;  A ~: bad |]                                      \
   1.147 +\        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
   1.148 +by (blast_tac (!claset addSDs [Server_cert_pubB] addSIs [lemma]) 1);
   1.149  qed "UseCertVerify";
   1.150  
   1.151  
   1.152 @@ -343,6 +355,11 @@
   1.153  qed_spec_mp "analz_image_priK";
   1.154  
   1.155  
   1.156 +(*slightly speeds up the big simplification below*)
   1.157 +goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
   1.158 +by (Blast_tac 1);
   1.159 +val range_sessionkeys_not_priK = result();
   1.160 +
   1.161  (*Lemma for the trivial direction of the if-and-only-if*)
   1.162  goal thy  
   1.163   "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
   1.164 @@ -350,11 +367,6 @@
   1.165  by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
   1.166  val lemma = result();
   1.167  
   1.168 -(*slightly speeds up the big simplification below*)
   1.169 -goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
   1.170 -by (Blast_tac 1);
   1.171 -val range_sessionkeys_not_priK = result();
   1.172 -
   1.173  (** It is a mystery to me why the following formulation is actually slower
   1.174      in simplification:
   1.175  
   1.176 @@ -371,12 +383,10 @@
   1.177  \            (Nonce N : analz (Key``KK Un (spies evs))) = \
   1.178  \            (Nonce N : analz (spies evs))";
   1.179  by (etac tls.induct 1);
   1.180 -by (ClientCertKeyEx_tac 6);
   1.181 +by (ClientKeyExch_tac 7);
   1.182  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.183  by (REPEAT_FIRST (rtac lemma));
   1.184 -writeln"SLOW simplification: 55 secs??";
   1.185 -(*ClientCertKeyEx is to blame, causing case splits for A, B: bad*)
   1.186 -by (ALLGOALS
   1.187 +by (ALLGOALS    (*23 seconds*)
   1.188      (asm_simp_tac (analz_image_keys_ss 
   1.189  		   addsimps [range_sessionkeys_not_priK, 
   1.190  			     analz_image_priK, analz_insert_certificate])));
   1.191 @@ -398,7 +408,7 @@
   1.192  
   1.193  goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
   1.194  by (parts_induct_tac 1);
   1.195 -(*ClientCertKeyEx: PMS is assumed to differ from any PRF.*)
   1.196 +(*ClientKeyExch: PMS is assumed to differ from any PRF.*)
   1.197  by (Blast_tac 1);
   1.198  qed "no_Notes_A_PRF";
   1.199  Addsimps [no_Notes_A_PRF];
   1.200 @@ -419,7 +429,7 @@
   1.201  
   1.202  
   1.203  
   1.204 -(*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
   1.205 +(*** Protocol goal: serverK(Na,Nb,M) and clientK(Na,Nb,M) remain secure ***)
   1.206  
   1.207  (** Some lemmas about session keys, comprising clientK and serverK **)
   1.208  
   1.209 @@ -475,7 +485,7 @@
   1.210  \        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
   1.211  by (etac rev_mp 1);
   1.212  by (etac rev_mp 1);
   1.213 -by (analz_induct_tac 1);        (*30 seconds??*)
   1.214 +by (analz_induct_tac 1);        (*17 seconds*)
   1.215  (*Oops*)
   1.216  by (Blast_tac 4);
   1.217  (*SpyKeys*)
   1.218 @@ -507,8 +517,8 @@
   1.219  by (etac rev_mp 1);
   1.220  by (parts_induct_tac 1);
   1.221  by (Fake_parts_insert_tac 1);
   1.222 -(*ClientCertKeyEx*)
   1.223 -by (ClientCertKeyEx_tac 1);
   1.224 +(*ClientKeyExch*)
   1.225 +by (ClientKeyExch_tac 1);
   1.226  by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   1.227  by (expand_case_tac "PMS = ?y" 1 THEN
   1.228      blast_tac (!claset addSEs partsEs) 1);
   1.229 @@ -536,7 +546,7 @@
   1.230  \                    Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
   1.231  by (parts_induct_tac 1);
   1.232  by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1);
   1.233 -(*ClientCertKeyEx: if PMS is fresh, then it can't appear in Notes A X.*)
   1.234 +(*ClientKeyExch: if PMS is fresh, then it can't appear in Notes A X.*)
   1.235  by (expand_case_tac "PMS = ?y" 1 THEN
   1.236      blast_tac (!claset addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1);
   1.237  val lemma = result();
   1.238 @@ -551,15 +561,15 @@
   1.239  
   1.240  
   1.241  
   1.242 -(*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
   1.243 +(*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
   1.244  goal thy
   1.245   "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
   1.246  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   1.247  \            Nonce PMS ~: analz (spies evs)";
   1.248 -by (analz_induct_tac 1);   (*30 seconds??*)
   1.249 +by (analz_induct_tac 1);   (*11 seconds*)
   1.250  (*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
   1.251 -by (EVERY (map (fast_tac (!claset addss (!simpset))) [7,6]));
   1.252 -(*ClientHello, ServerHello, ClientCertKeyEx, ServerResume: 
   1.253 +by (REPEAT (fast_tac (!claset addss (!simpset)) 6));
   1.254 +(*ClientHello, ServerHello, ClientKeyExch, ServerResume: 
   1.255    mostly freshness reasoning*)
   1.256  by (REPEAT (blast_tac (!claset addSEs partsEs
   1.257  			       addDs  [Notes_Crypt_parts_spies,
   1.258 @@ -572,13 +582,13 @@
   1.259  bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
   1.260  
   1.261  
   1.262 -(*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
   1.263 +(*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
   1.264    will stay secret.*)
   1.265  goal thy
   1.266   "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
   1.267  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   1.268  \            Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
   1.269 -by (analz_induct_tac 1);   (*35 seconds*)
   1.270 +by (analz_induct_tac 1);   (*13 seconds*)
   1.271  (*ClientAccepts and ServerAccepts: because PMS was already visible*)
   1.272  by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS, 
   1.273  				      Says_imp_spies RS analz.Inj,
   1.274 @@ -590,7 +600,7 @@
   1.275  			       Says_imp_spies RS analz.Inj]) 2);
   1.276  (*Fake*)
   1.277  by (spy_analz_tac 1);
   1.278 -(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   1.279 +(*ServerHello and ClientKeyExch: mostly freshness reasoning*)
   1.280  by (REPEAT (blast_tac (!claset addSEs partsEs
   1.281  			       addDs  [Notes_Crypt_parts_spies,
   1.282  				       impOfSubs analz_subset_parts,
   1.283 @@ -607,13 +617,13 @@
   1.284  \  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   1.285  \      Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
   1.286  \      A = A'";
   1.287 -by (analz_induct_tac 1);	(*17 seconds*)
   1.288 +by (analz_induct_tac 1);	(*8 seconds*)
   1.289  by (ALLGOALS Clarify_tac);
   1.290  (*ClientFinished, ClientResume: by unicity of PMS*)
   1.291  by (REPEAT 
   1.292      (blast_tac (!claset addSDs [Notes_master_imp_Notes_PMS]
   1.293       	 	        addIs  [Notes_unique_PMS RS conjunct1]) 2));
   1.294 -(*ClientCertKeyEx*)
   1.295 +(*ClientKeyExch*)
   1.296  by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
   1.297  	               addSDs [Says_imp_spies RS parts.Inj]) 1);
   1.298  bind_thm ("Says_clientK_unique",
   1.299 @@ -635,7 +645,7 @@
   1.300  by (ALLGOALS Asm_simp_tac);
   1.301  (*Oops*)
   1.302  by (blast_tac (!claset addIs [Says_clientK_unique]) 2);
   1.303 -(*ClientCertKeyEx*)
   1.304 +(*ClientKeyExch*)
   1.305  by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
   1.306  			       spies_partsEs)) 1);
   1.307  qed_spec_mp "clientK_Oops_ALL";
   1.308 @@ -651,7 +661,7 @@
   1.309  \  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   1.310  \      Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
   1.311  \      B = B'";
   1.312 -by (analz_induct_tac 1);	(*17 seconds*)
   1.313 +by (analz_induct_tac 1);	(*9 seconds*)
   1.314  by (ALLGOALS Clarify_tac);
   1.315  (*ServerResume, ServerFinished: by unicity of PMS*)
   1.316  by (REPEAT
   1.317 @@ -661,7 +671,7 @@
   1.318                          addDs  [Spy_not_see_PMS, 
   1.319  				Notes_Crypt_parts_spies,
   1.320  				Crypt_unique_PMS]) 2));
   1.321 -(*ClientCertKeyEx*)
   1.322 +(*ClientKeyExch*)
   1.323  by (blast_tac (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]
   1.324  	               addSDs [Says_imp_spies RS parts.Inj]) 1);
   1.325  bind_thm ("Says_serverK_unique",
   1.326 @@ -682,7 +692,7 @@
   1.327  by (ALLGOALS Asm_simp_tac);
   1.328  (*Oops*)
   1.329  by (blast_tac (!claset addIs [Says_serverK_unique]) 2);
   1.330 -(*ClientCertKeyEx*)
   1.331 +(*ClientKeyExch*)
   1.332  by (blast_tac (!claset addSEs ((PMS_sessionK_not_spied RSN (2,rev_notE)) ::
   1.333  			       spies_partsEs)) 1);
   1.334  qed_spec_mp "serverK_Oops_ALL";
   1.335 @@ -699,19 +709,19 @@
   1.336   "!!evs. [| ALL A. Says A Spy (Key (serverK(Na,Nb,M))) ~: set evs; \
   1.337  \           X = Crypt (serverK(Na,Nb,M))                  \
   1.338  \                 (Hash{|Nonce M, Number SID,             \
   1.339 -\                        Nonce NA, Number PA, Agent A,    \
   1.340 -\                        Nonce NB, Number PB, Agent B|}); \
   1.341 +\                        Nonce Na, Number PA, Agent A,    \
   1.342 +\                        Nonce Nb, Number PB, Agent B|}); \
   1.343  \           M = PRF(PMS,NA,NB);                           \
   1.344  \           evs : tls;  A ~: bad;  B ~: bad |]          \
   1.345  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
   1.346  \        X : parts (spies evs) --> Says B A X : set evs";
   1.347  by (etac rev_mp 1);
   1.348  by (hyp_subst_tac 1);
   1.349 -by (analz_induct_tac 1);        (*27 seconds*)
   1.350 +by (analz_induct_tac 1);        (*22 seconds*)
   1.351  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   1.352  (*proves ServerResume*)
   1.353  by (ALLGOALS Clarify_tac);
   1.354 -(*ClientCertKeyEx*)
   1.355 +(*ClientKeyExch*)
   1.356  by (fast_tac  (*blast_tac gives PROOF FAILED*)
   1.357      (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
   1.358  (*Fake: the Spy doesn't have the critical session key!*)
   1.359 @@ -725,8 +735,8 @@
   1.360  goal thy
   1.361   "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
   1.362  \                 (Hash{|Nonce M, Number SID,             \
   1.363 -\                        Nonce NA, Number PA, Agent A,    \
   1.364 -\                        Nonce NB, Number PB, Agent B|}); \
   1.365 +\                        Nonce Na, Number PA, Agent A,    \
   1.366 +\                        Nonce Nb, Number PB, Agent B|}); \
   1.367  \           M = PRF(PMS,NA,NB);                           \
   1.368  \           X : parts (spies evs);                        \
   1.369  \           Notes A {|Agent B, Nonce PMS|} : set evs;     \
   1.370 @@ -764,7 +774,7 @@
   1.371                          addDs  [Spy_not_see_PMS, 
   1.372  				Notes_Crypt_parts_spies,
   1.373  				Crypt_unique_PMS]) 3));
   1.374 -(*ClientCertKeyEx*)
   1.375 +(*ClientKeyExch*)
   1.376  by (blast_tac
   1.377      (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
   1.378  (*Fake: the Spy doesn't have the critical session key!*)
   1.379 @@ -801,13 +811,13 @@
   1.380  \      Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   1.381  \      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) -->  \
   1.382  \      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   1.383 -by (analz_induct_tac 1);	(*23 seconds*)
   1.384 +by (analz_induct_tac 1);	(*15 seconds*)
   1.385  by (ALLGOALS Clarify_tac);
   1.386  (*ClientFinished, ClientResume: by unicity of PMS*)
   1.387  by (REPEAT (blast_tac (!claset delrules [conjI]
   1.388  		               addSDs [Notes_master_imp_Notes_PMS]
   1.389  	 	               addDs  [Notes_unique_PMS]) 3));
   1.390 -(*ClientCertKeyEx*)
   1.391 +(*ClientKeyExch*)
   1.392  by (fast_tac  (*blast_tac gives PROOF FAILED*)
   1.393      (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
   1.394  (*Fake: the Spy doesn't have the critical session key!*)
   1.395 @@ -837,9 +847,8 @@
   1.396  goal thy
   1.397   "!!evs. [| Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs;\
   1.398  \           Says A' B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs; \
   1.399 -\           Says B  A {|Nonce NB, Number SID, Number PB, certificate B KB|}  \
   1.400 -\             : set evs;                                                  \
   1.401 -\           Says A'' B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))\
   1.402 +\           certificate A KA : parts (spies evs);       \
   1.403 +\           Says A'' B (Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}))\
   1.404  \             : set evs;                                                  \
   1.405  \        evs : tls;  A ~: bad;  B ~: bad |]                             \
   1.406  \     ==> Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   1.407 @@ -849,5 +858,4 @@
   1.408  
   1.409  (*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)
   1.410  (*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*)
   1.411 -
   1.412 -
   1.413 +(*29/9/97: loads in 481s, after removing Certificate from ClientKeyExch*)
     2.1 --- a/src/HOL/Auth/TLS.thy	Mon Sep 29 15:39:28 1997 +0200
     2.2 +++ b/src/HOL/Auth/TLS.thy	Tue Sep 30 11:03:55 1997 +0200
     2.3 @@ -21,9 +21,9 @@
     2.4  The model assumes that no fraudulent certificates are present, but it does
     2.5  assume that some private keys are to the spy.
     2.6  
     2.7 -REMARK.  The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientCertKeyEx,
     2.8 +REMARK.  The event "Notes A {|Agent B, Nonce PMS|}" appears in ClientKeyExch,
     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 +herself.  Nobody else can see it.  In ClientKeyExch, the Spy can substitute
    2.12  his own certificate for A's, but he cannot replace A's note by one for himself.
    2.13  
    2.14  The Note event avoids a weakness in the public-key model.  Each
    2.15 @@ -33,7 +33,7 @@
    2.16  In the shared-key model, the ability to encrypt implies the ability to
    2.17  decrypt, so the problem does not arise.
    2.18  
    2.19 -Proofs would be simpler if ClientCertKeyEx included A's name within
    2.20 +Proofs would be simpler if ClientKeyExch included A's name within
    2.21  Crypt KB (Nonce PMS).  As things stand, there is much overlap between proofs
    2.22  about that message (which B receives) and the stronger event
    2.23  	Notes A {|Agent B, Nonce PMS|}.
    2.24 @@ -61,17 +61,18 @@
    2.25      clientK, serverK :: "nat*nat*nat => key"
    2.26  
    2.27  translations
    2.28 -  "clientK (x)"	== "sessionK(x,0)"
    2.29 -  "serverK (x)"	== "sessionK(x,1)"
    2.30 +  "clientK (nonces)"	== "sessionK(nonces,0)"
    2.31 +  "serverK (nonces)"	== "sessionK(nonces,1)"
    2.32  
    2.33  rules
    2.34 +  (*the pseudo-random function is collision-free*)
    2.35    inj_PRF       "inj PRF"	
    2.36  
    2.37 -  (*sessionK is collision-free and makes symmetric keys.  Also, no clientK
    2.38 -    clashes with any serverK.*)
    2.39 +  (*sessionK is collision-free; also, no clientK clashes with any serverK.*)
    2.40    inj_sessionK  "inj sessionK"	
    2.41  
    2.42 -  isSym_sessionK "isSymKey (sessionK x)"
    2.43 +  (*sessionK makes symmetric keys*)
    2.44 +  isSym_sessionK "isSymKey (sessionK nonces)"
    2.45  
    2.46  
    2.47  consts    tls :: event list set
    2.48 @@ -111,12 +112,15 @@
    2.49           "[| evsSH: tls;  A ~= B;  Nonce NB ~: used evsSH;  NB ~: range PRF;
    2.50               Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
    2.51  	       : set evsSH |]
    2.52 -          ==> Says B A {|Nonce NB, Number SID, Number PB,
    2.53 -			 certificate B (pubK B)|}
    2.54 -                # evsSH  :  tls"
    2.55 +          ==> Says B A {|Nonce NB, Number SID, Number PB|} # evsSH  :  tls"
    2.56  
    2.57 -    ClientCertKeyEx
    2.58 -         (*CLIENT CERTIFICATE (7.4.6) and KEY EXCHANGE (7.4.7).
    2.59 +    Certificate
    2.60 +         (*SERVER (7.4.2) or CLIENT (7.4.6) CERTIFICATE.*)
    2.61 +         "[| evsC: tls;  A ~= B |]
    2.62 +          ==> Says B A (certificate B (pubK B)) # evsC  :  tls"
    2.63 +
    2.64 +    ClientKeyExch
    2.65 +         (*CLIENT KEY EXCHANGE (7.4.7).
    2.66             The client, A, chooses PMS, the PREMASTER SECRET.
    2.67             She encrypts PMS using the supplied KB, which ought to be pubK B.
    2.68             We assume PMS ~: range PRF because a clash betweem the PMS
    2.69 @@ -125,9 +129,9 @@
    2.70             The Note event records in the trace that she knows PMS
    2.71                 (see REMARK at top). *)
    2.72           "[| evsCX: tls;  A ~= B;  Nonce PMS ~: used evsCX;  PMS ~: range PRF;
    2.73 -             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
    2.74 -	       : set evsCX |]
    2.75 -          ==> Says A B {|certificate A (pubK A), Crypt KB (Nonce PMS)|}
    2.76 +             Says B'  A {|Nonce NB, Number SID, Number PB|} : set evsCX;
    2.77 +             Says B'' A (certificate B KB) : set evsCX |]
    2.78 +          ==> Says A B (Crypt KB (Nonce PMS))
    2.79  	      # Notes A {|Agent B, Nonce PMS|}
    2.80  	      # evsCX  :  tls"
    2.81  
    2.82 @@ -138,8 +142,7 @@
    2.83            Checking the signature, which is the only use of A's certificate,
    2.84            assures B of A's presence*)
    2.85           "[| evsCV: tls;  A ~= B;  
    2.86 -             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
    2.87 -	       : set evsCV;
    2.88 +             Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCV;
    2.89  	     Notes A {|Agent B, Nonce PMS|} : set evsCV |]
    2.90            ==> Says A B (Crypt (priK A) (Hash{|Nonce NB, Agent B, Nonce PMS|}))
    2.91                # evsCV  :  tls"
    2.92 @@ -158,8 +161,7 @@
    2.93           "[| evsCF: tls;  
    2.94  	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
    2.95  	       : set evsCF;
    2.96 -             Says B' A {|Nonce NB, Number SID, Number PB, certificate B KB|}
    2.97 -	       : set evsCF;
    2.98 +             Says B' A {|Nonce NB, Number SID, Number PB|} : set evsCF;
    2.99               Notes A {|Agent B, Nonce PMS|} : set evsCF;
   2.100  	     M = PRF(PMS,NA,NB) |]
   2.101            ==> Says A B (Crypt (clientK(NA,NB,M))
   2.102 @@ -174,11 +176,8 @@
   2.103           "[| evsSF: tls;
   2.104  	     Says A' B  {|Agent A, Nonce NA, Number SID, Number PA|}
   2.105  	       : set evsSF;
   2.106 -	     Says B  A  {|Nonce NB, Number SID, Number PB,
   2.107 -		 	  certificate B (pubK B)|}
   2.108 -	       : set evsSF;
   2.109 -	     Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
   2.110 -	       : set evsSF;
   2.111 +	     Says B  A  {|Nonce NB, Number SID, Number PB|} : set evsSF;
   2.112 +	     Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSF;
   2.113  	     M = PRF(PMS,NA,NB) |]
   2.114            ==> Says B A (Crypt (serverK(NA,NB,M))
   2.115  			(Hash{|Nonce M, Number SID,
   2.116 @@ -208,8 +207,7 @@
   2.117            needed to resume this session.  The "Says A'' B ..." premise is
   2.118            used to prove Notes_master_imp_Crypt_PMS.*)
   2.119           "[| evsSA: tls;
   2.120 -             Says A'' B {|certificate A KA, Crypt (pubK B) (Nonce PMS)|}
   2.121 -	       : set evsSA;
   2.122 +             Says A'' B (Crypt (pubK B) (Nonce PMS)) : set evsSA;
   2.123  	     M = PRF(PMS,NA,NB);  
   2.124  	     X = Hash{|Nonce M, Number SID,
   2.125  	               Nonce NA, Number PA, Agent A, 
   2.126 @@ -220,9 +218,8 @@
   2.127               Notes B {|Number SID, Agent A, Agent B, Nonce M|} # evsSA  :  tls"
   2.128  
   2.129      ServerResume
   2.130 -         (*Resumption is described in 7.3.  If B finds the SESSION_ID
   2.131 -           then he sends HELLO and FINISHED messages, using the
   2.132 -           previously stored MASTER SECRET*)
   2.133 +         (*Resumption (7.3):  If B finds the SESSION_ID then he can send
   2.134 +           a FINISHED message using the recovered MASTER SECRET*)
   2.135           "[| evsSR: tls;  A ~= B;  Nonce NB ~: used evsSR;  NB ~: range PRF;
   2.136               Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evsSR;
   2.137  	     Says A' B {|Agent A, Nonce NA, Number SID, Number PA|}
   2.138 @@ -230,12 +227,12 @@
   2.139            ==> Says B A (Crypt (serverK(NA,NB,M))
   2.140  			(Hash{|Nonce M, Number SID,
   2.141  			       Nonce NA, Number PA, Agent A, 
   2.142 -			       Nonce NB, Number PB, Agent B|}))
   2.143 -              # Says B A {|Nonce NB, Number SID, Number PB|} # evsSR  :  tls"
   2.144 +			       Nonce NB, Number PB, Agent B|})) # evsSR
   2.145 +	        :  tls"
   2.146  
   2.147      ClientResume
   2.148 -         (*If the response to ClientHello is ServerResume then send
   2.149 -           a FINISHED message using the new nonces and stored MASTER SECRET.*)
   2.150 +         (*If A recalls the SESSION_ID, then she sends a FINISHED message
   2.151 +           using the new nonces and stored MASTER SECRET.*)
   2.152           "[| evsCR: tls;  
   2.153  	     Says A  B {|Agent A, Nonce NA, Number SID, Number PA|}
   2.154  	       : set evsCR;