src/HOL/Auth/TLS.ML
changeset 3745 4c5d3b1ddc75
parent 3729 6be7cf5086ab
child 3758 188a4fbfaf55
     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*)