src/HOL/Auth/TLS.ML
changeset 3677 f2569416d18b
parent 3676 cbaec955056b
child 3683 aafe719dff14
     1.1 --- a/src/HOL/Auth/TLS.ML	Tue Sep 16 14:40:01 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Wed Sep 17 16:37:21 1997 +0200
     1.3 @@ -48,47 +48,27 @@
     1.4  
     1.5  
     1.6  (*Injectiveness of key-generating functions*)
     1.7 -AddIffs [inj_PRF RS inj_eq, inj_clientK RS inj_eq, inj_serverK RS inj_eq];
     1.8 +AddIffs [inj_PRF RS inj_eq, inj_sessionK RS inj_eq];
     1.9  
    1.10 -(* invKey(clientK x) = clientK x  and similarly for serverK*)
    1.11 -Addsimps [isSym_clientK, rewrite_rule [isSymKey_def] isSym_clientK,
    1.12 -	  isSym_serverK, rewrite_rule [isSymKey_def] isSym_serverK];
    1.13 +(* invKey(sessionK x) = sessionK x*)
    1.14 +Addsimps [isSym_sessionK, rewrite_rule [isSymKey_def] isSym_sessionK];
    1.15  
    1.16  
    1.17  (*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
    1.18  
    1.19 -goal thy "pubK A ~= clientK arg";
    1.20 -br notI 1;
    1.21 -by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    1.22 -by (Full_simp_tac 1);
    1.23 -qed "pubK_neq_clientK";
    1.24 -
    1.25 -goal thy "pubK A ~= serverK arg";
    1.26 -br notI 1;
    1.27 -by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    1.28 -by (Full_simp_tac 1);
    1.29 -qed "pubK_neq_serverK";
    1.30 -
    1.31 -goal thy "priK A ~= clientK arg";
    1.32 +goal thy "pubK A ~= sessionK arg";
    1.33  br notI 1;
    1.34  by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    1.35  by (Full_simp_tac 1);
    1.36 -qed "priK_neq_clientK";
    1.37 +qed "pubK_neq_sessionK";
    1.38  
    1.39 -goal thy "priK A ~= serverK arg";
    1.40 +goal thy "priK A ~= sessionK arg";
    1.41  br notI 1;
    1.42  by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    1.43  by (Full_simp_tac 1);
    1.44 -qed "priK_neq_serverK";
    1.45 +qed "priK_neq_sessionK";
    1.46  
    1.47 -(*clientK and serverK have disjoint ranges*)
    1.48 -goal thy "clientK arg ~= serverK arg'";
    1.49 -by (cut_facts_tac [rangeI RS impOfSubs clientK_range] 1);
    1.50 -by (Blast_tac 1);
    1.51 -qed "clientK_neq_serverK";
    1.52 -
    1.53 -val keys_distinct = [pubK_neq_clientK, pubK_neq_serverK, 
    1.54 -		     priK_neq_clientK, priK_neq_serverK, clientK_neq_serverK];
    1.55 +val keys_distinct = [pubK_neq_sessionK, priK_neq_sessionK];
    1.56  AddIffs (keys_distinct @ (keys_distinct RL [not_sym]));
    1.57  
    1.58  
    1.59 @@ -263,27 +243,6 @@
    1.60  qed "Notes_Crypt_parts_sees";
    1.61  
    1.62  
    1.63 -(*****************
    1.64 -    (*NEEDED?  TRUE???
    1.65 -      Every Nonce that's hashed is already in past traffic. 
    1.66 -      This general formulation is tricky to prove and hard to use, since the
    1.67 -      2nd premise is typically proved by simplification.*)
    1.68 -    goal thy "!!evs. [| Hash X : parts (sees Spy evs);  \
    1.69 -    \                   Nonce N : parts {X};  evs : tls |]  \
    1.70 -    \                ==> Nonce N : parts (sees Spy evs)";
    1.71 -    by (etac rev_mp 1);
    1.72 -    by (parts_induct_tac 1);
    1.73 -    by (step_tac (!claset addSDs [Notes_Crypt_parts_sees,
    1.74 -				  Says_imp_sees_Spy RS parts.Inj]
    1.75 -			  addSEs partsEs) 1);
    1.76 -    by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [parts_insert_sees])));
    1.77 -    by (Fake_parts_insert_tac 1);
    1.78 -    (*CertVerify, ClientFinished, ServerFinished (?)*)
    1.79 -    by (REPEAT (Blast_tac 1));
    1.80 -    qed "Hash_imp_Nonce_seen";
    1.81 -****************************************************************)
    1.82 -
    1.83 -
    1.84  (*** Protocol goal: if B receives CERTIFICATE VERIFY, then A sent it ***)
    1.85  
    1.86  (*B can check A's signature if he has received A's certificate.
    1.87 @@ -326,7 +285,7 @@
    1.88  by (etac tls.induct 1);
    1.89  by (ALLGOALS
    1.90      (asm_simp_tac (analz_image_keys_ss
    1.91 -		   addsimps (certificate_def::keys_distinct))));
    1.92 +		   addsimps (analz_insert_certificate::keys_distinct))));
    1.93  (*Fake*) 
    1.94  by (spy_analz_tac 2);
    1.95  (*Base*)
    1.96 @@ -341,24 +300,28 @@
    1.97  by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
    1.98  val lemma = result();
    1.99  
   1.100 -(*Knowing some clientKs and serverKs is no help in getting new nonces*)
   1.101 +(*slightly speeds up the big simplification below*)
   1.102 +goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
   1.103 +by (Blast_tac 1);
   1.104 +val range_sessionkeys_not_priK = result();
   1.105 +
   1.106 +(*Knowing some session keys is no help in getting new nonces*)
   1.107  goal thy  
   1.108   "!!evs. evs : tls ==>                                 \
   1.109 -\    ALL KK. KK <= (range clientK Un range serverK) -->           \
   1.110 +\    ALL KK. KK <= range sessionK -->           \
   1.111  \            (Nonce N : analz (Key``KK Un (sees Spy evs))) = \
   1.112  \            (Nonce N : analz (sees Spy evs))";
   1.113  by (etac tls.induct 1);
   1.114  by (ClientCertKeyEx_tac 6);
   1.115  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   1.116  by (REPEAT_FIRST (rtac lemma));
   1.117 -writeln"SLOW simplification: 60 secs!??";
   1.118 +writeln"SLOW simplification: 55 secs??";
   1.119 +(*ClientCertKeyEx is to blame, causing case splits for A, B: lost*)
   1.120  by (ALLGOALS
   1.121      (asm_simp_tac (analz_image_keys_ss 
   1.122 -		   addsimps (analz_image_priK::certificate_def::
   1.123 -                             keys_distinct))));
   1.124 +		   addsimps [range_sessionkeys_not_priK, 
   1.125 +			     analz_image_priK, analz_insert_certificate])));
   1.126  by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
   1.127 -(*ClientCertKeyEx: a nonce is sent, but one needs a priK to read it.*)
   1.128 -by (Blast_tac 3);
   1.129  (*Fake*) 
   1.130  by (spy_analz_tac 2);
   1.131  (*Base*)
   1.132 @@ -374,29 +337,6 @@
   1.133  Addsimps [no_Notes_A_PRF];
   1.134  
   1.135  
   1.136 -(*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
   1.137 -goal thy
   1.138 - "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
   1.139 -\        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   1.140 -\            Nonce PMS ~: analz (sees Spy evs)";
   1.141 -by (analz_induct_tac 1);   (*47 seconds???*)
   1.142 -(*ClientHello*)
   1.143 -by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   1.144 -                               addSEs sees_Spy_partsEs) 3);
   1.145 -(*SpyKeys*)
   1.146 -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   1.147 -by (fast_tac (!claset addss (!simpset)) 2);
   1.148 -(*Fake*)
   1.149 -by (spy_analz_tac 1);
   1.150 -(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   1.151 -by (REPEAT (blast_tac (!claset addSEs partsEs
   1.152 -			       addDs  [Notes_Crypt_parts_sees,
   1.153 -				       impOfSubs analz_subset_parts,
   1.154 -				       Says_imp_sees_Spy RS analz.Inj]) 1));
   1.155 -bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
   1.156 -
   1.157 -
   1.158 -
   1.159  goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (sees Spy evs);  \
   1.160  \                   evs : tls |]  \
   1.161  \                ==> Nonce PMS : parts (sees Spy evs)";
   1.162 @@ -404,54 +344,24 @@
   1.163  by (parts_induct_tac 1);
   1.164  by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
   1.165  by (Fake_parts_insert_tac 1);
   1.166 -(*Client key exchange*)
   1.167 -by (Blast_tac 4);
   1.168 -(*Server Hello: by freshness*)
   1.169 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 3);
   1.170 -(*Client Hello: trivial*)
   1.171 -by (Blast_tac 2);
   1.172 -(*SpyKeys*)
   1.173 -by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
   1.174 +(*Six others, all trivial or by freshness*)
   1.175 +by (REPEAT (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   1.176 +                               addSEs sees_Spy_partsEs) 1));
   1.177  qed "MS_imp_PMS";
   1.178  AddSDs [MS_imp_PMS];
   1.179  
   1.180  
   1.181 -(*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
   1.182 -  will stay secret.*)
   1.183 -goal thy
   1.184 - "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
   1.185 -\        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   1.186 -\            Nonce (PRF(PMS,NA,NB)) ~: analz (sees Spy evs)";
   1.187 -by (analz_induct_tac 1);   (*47 seconds???*)
   1.188 -(*ClientHello*)
   1.189 -by (Blast_tac 3);
   1.190 -(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
   1.191 -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   1.192 -by (blast_tac (!claset addSDs [Spy_not_see_PMS, 
   1.193 -			       Says_imp_sees_Spy RS analz.Inj]) 2);
   1.194 -(*Fake*)
   1.195 -by (spy_analz_tac 1);
   1.196 -(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   1.197 -by (REPEAT (blast_tac (!claset addSEs partsEs
   1.198 -			       addDs  [MS_imp_PMS,
   1.199 -				       Notes_Crypt_parts_sees,
   1.200 -				       impOfSubs analz_subset_parts,
   1.201 -				       Says_imp_sees_Spy RS analz.Inj]) 1));
   1.202 -bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
   1.203 -
   1.204 -
   1.205  
   1.206  (*** Protocol goal: serverK(NA,NB,M) and clientK(NA,NB,M) remain secure ***)
   1.207  
   1.208 -(** First, some lemmas about those write keys.  The proofs for serverK are 
   1.209 -    nearly identical to those for clientK. **)
   1.210 +(** Some lemmas about session keys, comprising clientK and serverK **)
   1.211  
   1.212  (*Lemma: those write keys are never sent if M (MASTER SECRET) is secure.  
   1.213    Converse doesn't hold; betraying M doesn't force the keys to be sent!*)
   1.214  
   1.215  goal thy 
   1.216   "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]   \
   1.217 -\        ==> Key (clientK(NA,NB,M)) ~: parts (sees Spy evs)";
   1.218 +\        ==> Key (sessionK(b,NA,NB,M)) ~: parts (sees Spy evs)";
   1.219  by (etac rev_mp 1);
   1.220  by (analz_induct_tac 1);
   1.221  (*SpyKeys*)
   1.222 @@ -461,66 +371,35 @@
   1.223  by (spy_analz_tac 2);
   1.224  (*Base*)
   1.225  by (Blast_tac 1);
   1.226 -qed "clientK_notin_parts";
   1.227 -bind_thm ("clientK_in_partsE", clientK_notin_parts RSN (2, rev_notE));
   1.228 -Addsimps [clientK_notin_parts];
   1.229 -AddSEs [clientK_in_partsE, 
   1.230 -	impOfSubs analz_subset_parts RS clientK_in_partsE];
   1.231 +qed "sessionK_notin_parts";
   1.232 +bind_thm ("sessionK_in_partsE", sessionK_notin_parts RSN (2, rev_notE));
   1.233  
   1.234 -goal thy 
   1.235 - "!!evs. [| Nonce M ~: analz (sees Spy evs);  evs : tls |]   \
   1.236 -\        ==> Key (serverK(NA,NB,M)) ~: parts (sees Spy evs)";
   1.237 -by (etac rev_mp 1);
   1.238 -by (analz_induct_tac 1);
   1.239 -(*SpyKeys*)
   1.240 -by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 3);
   1.241 -by (blast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj]) 3);
   1.242 -(*Fake*) 
   1.243 -by (spy_analz_tac 2);
   1.244 -(*Base*)
   1.245 -by (Blast_tac 1);
   1.246 -qed "serverK_notin_parts";
   1.247 -bind_thm ("serverK_in_partsE", serverK_notin_parts RSN (2, rev_notE));
   1.248 -Addsimps [serverK_notin_parts];
   1.249 -AddSEs [serverK_in_partsE, 
   1.250 -	impOfSubs analz_subset_parts RS serverK_in_partsE];
   1.251 +Addsimps [sessionK_notin_parts];
   1.252 +AddSEs [sessionK_in_partsE, 
   1.253 +	impOfSubs analz_subset_parts RS sessionK_in_partsE];
   1.254  
   1.255  
   1.256 -(*Lemma: those write keys are never used if PMS is fresh.  
   1.257 +(*Lemma: session keys are never used if PMS is fresh.  
   1.258    Nonces don't have to agree, allowing session resumption.
   1.259    Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
   1.260    They are NOT suitable as safe elim rules.*)
   1.261  
   1.262  goal thy 
   1.263 - "!!evs. [| Nonce PMS ~: used evs;  evs : tls |]                           \
   1.264 -\  ==> Crypt (clientK(Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
   1.265 + "!!evs. [| Nonce PMS ~: parts (sees Spy evs);  evs : tls |]             \
   1.266 +\  ==> Crypt (sessionK(b, Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
   1.267  by (etac rev_mp 1);
   1.268  by (analz_induct_tac 1);
   1.269 -(*ClientFinished: since M is fresh, a different instance of clientK was used.*)
   1.270 -by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   1.271 -                       addSEs sees_Spy_partsEs) 3);
   1.272 +(*Fake*)
   1.273 +by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 2);
   1.274  by (Fake_parts_insert_tac 2);
   1.275 -(*Base*)
   1.276 -by (Blast_tac 1);
   1.277 -qed "Crypt_clientK_notin_parts";
   1.278 -Addsimps [Crypt_clientK_notin_parts];
   1.279 -AddEs [Crypt_clientK_notin_parts RSN (2, rev_notE)];
   1.280 +(*Base, ClientFinished, ServerFinished: trivial, e.g. by freshness*)
   1.281 +by (REPEAT 
   1.282 +    (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   1.283 +                        addSEs sees_Spy_partsEs) 1));
   1.284 +qed "Crypt_sessionK_notin_parts";
   1.285  
   1.286 -goal thy 
   1.287 - "!!evs. [| Nonce PMS ~: used evs;  evs : tls |]                           \
   1.288 -\  ==> Crypt (serverK(Na, Nb, PRF(PMS,NA,NB))) Y ~: parts (sees Spy evs)";
   1.289 -by (etac rev_mp 1);
   1.290 -by (analz_induct_tac 1);
   1.291 -(*ServerFinished: since M is fresh, a different instance of serverK was used.*)
   1.292 -by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   1.293 -                               addSEs sees_Spy_partsEs) 3);
   1.294 -by (Fake_parts_insert_tac 2);
   1.295 -(*Base*)
   1.296 -by (Blast_tac 1);
   1.297 -qed "Crypt_serverK_notin_parts";
   1.298 -
   1.299 -Addsimps [Crypt_serverK_notin_parts];
   1.300 -AddEs [Crypt_serverK_notin_parts RSN (2, rev_notE)];
   1.301 +Addsimps [Crypt_sessionK_notin_parts];
   1.302 +AddEs [Crypt_sessionK_notin_parts RSN (2, rev_notE)];
   1.303  
   1.304  
   1.305  (*NEEDED??*)
   1.306 @@ -559,7 +438,7 @@
   1.307  qed "unique_PMS";
   1.308  
   1.309  
   1.310 -(*In A's note to herself, PMS determines A and B.*)
   1.311 +(*In A's internal Note, PMS determines A and B.*)
   1.312  goal thy 
   1.313   "!!evs. [| Nonce PMS ~: analz (sees Spy evs);  evs : tls |]            \
   1.314  \ ==> EX A' B'. ALL A B.                                                   \
   1.315 @@ -583,6 +462,60 @@
   1.316  
   1.317  
   1.318  
   1.319 +(*If A sends ClientCertKeyEx to an honest B, then the PMS will stay secret.*)
   1.320 +goal thy
   1.321 + "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
   1.322 +\        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   1.323 +\            Nonce PMS ~: analz (sees Spy evs)";
   1.324 +by (analz_induct_tac 1);   (*30 seconds???*)
   1.325 +(*ClientAccepts and ServerAccepts: because PMS ~: range PRF*)
   1.326 +by (REPEAT (fast_tac (!claset addss (!simpset)) 6));
   1.327 +(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   1.328 +by (REPEAT (blast_tac (!claset addSEs partsEs
   1.329 +			       addDs  [Notes_Crypt_parts_sees,
   1.330 +				       impOfSubs analz_subset_parts,
   1.331 +				       Says_imp_sees_Spy RS analz.Inj]) 4));
   1.332 +(*ClientHello*)
   1.333 +by (blast_tac (!claset addSDs [Notes_Crypt_parts_sees]
   1.334 +                               addSEs sees_Spy_partsEs) 3);
   1.335 +(*SpyKeys*)
   1.336 +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   1.337 +by (fast_tac (!claset addss (!simpset)) 2);
   1.338 +(*Fake*)
   1.339 +by (spy_analz_tac 1);
   1.340 +bind_thm ("Spy_not_see_PMS", result() RSN (2, rev_mp));
   1.341 +
   1.342 +
   1.343 +
   1.344 +
   1.345 +
   1.346 +(*If A sends ClientCertKeyEx to an honest B, then the MASTER SECRET
   1.347 +  will stay secret.*)
   1.348 +goal thy
   1.349 + "!!evs. [| evs : tls;  A ~: lost;  B ~: lost |]           \
   1.350 +\        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
   1.351 +\            Nonce (PRF(PMS,NA,NB)) ~: analz (sees Spy evs)";
   1.352 +by (analz_induct_tac 1);   (*35 seconds*)
   1.353 +(*ClientAccepts and ServerAccepts: because PMS was already visible*)
   1.354 +by (REPEAT (blast_tac (!claset addDs [Spy_not_see_PMS, 
   1.355 +				      Says_imp_sees_Spy RS analz.Inj,
   1.356 +				      Notes_imp_sees_Spy RS analz.Inj]) 6));
   1.357 +(*ClientHello*)
   1.358 +by (Blast_tac 3);
   1.359 +(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
   1.360 +by (asm_simp_tac (analz_image_keys_ss addsimps [analz_image_keys]) 2);
   1.361 +by (blast_tac (!claset addSDs [Spy_not_see_PMS, 
   1.362 +			       Says_imp_sees_Spy RS analz.Inj]) 2);
   1.363 +(*Fake*)
   1.364 +by (spy_analz_tac 1);
   1.365 +(*ServerHello and ClientCertKeyEx: mostly freshness reasoning*)
   1.366 +by (REPEAT (blast_tac (!claset addSEs partsEs
   1.367 +			       addDs  [Notes_Crypt_parts_sees,
   1.368 +				       impOfSubs analz_subset_parts,
   1.369 +				       Says_imp_sees_Spy RS analz.Inj]) 1));
   1.370 +bind_thm ("Spy_not_see_MS", result() RSN (2, rev_mp));
   1.371 +
   1.372 +
   1.373  (*** Protocol goals: if A receives SERVER FINISHED, then B is present 
   1.374       and has used the quoted values XA, XB, etc.  Note that it is up to A
   1.375       to compare XA with what she originally sent.
   1.376 @@ -599,11 +532,12 @@
   1.377  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs --> \
   1.378  \        X : parts (sees Spy evs) --> Says B A X : set evs";
   1.379  by (hyp_subst_tac 1);
   1.380 -by (analz_induct_tac 1);
   1.381 +by (analz_induct_tac 1);	(*16 seconds*)
   1.382 +(*ClientCertKeyEx*)
   1.383 +by (Blast_tac 2);
   1.384  (*Fake: the Spy doesn't have the critical session key!*)
   1.385  by (REPEAT (rtac impI 1));
   1.386 -by (subgoal_tac 
   1.387 -    "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
   1.388 +by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(sees Spy evsa)" 1);
   1.389  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.390  				     not_parts_not_analz]) 2);
   1.391  by (Fake_parts_insert_tac 1);
   1.392 @@ -622,11 +556,12 @@
   1.393  \            Crypt (serverK(Na,Nb,M)) Y : parts (sees Spy evs)  -->  \
   1.394  \            (EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs)";
   1.395  by (hyp_subst_tac 1);
   1.396 -by (analz_induct_tac 1);
   1.397 +by (analz_induct_tac 1);	(*12 seconds*)
   1.398  by (REPEAT_FIRST (rtac impI));
   1.399 +(*ClientCertKeyEx*)
   1.400 +by (Blast_tac 2);
   1.401  (*Fake: the Spy doesn't have the critical session key!*)
   1.402 -by (subgoal_tac 
   1.403 -    "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
   1.404 +by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(sees Spy evsa)" 1);
   1.405  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.406  				     not_parts_not_analz]) 2);
   1.407  by (Fake_parts_insert_tac 1);
   1.408 @@ -635,7 +570,7 @@
   1.409  (*...otherwise delete induction hyp and use unicity of PMS.*)
   1.410  by (thin_tac "?PP-->?QQ" 1);
   1.411  by (Step_tac 1);
   1.412 -by (subgoal_tac "Nonce PMS ~: analz (sees Spy evsSF)" 1);
   1.413 +by (subgoal_tac "Nonce PMS ~: analz(sees Spy evsSF)" 1);
   1.414  by (asm_simp_tac (!simpset addsimps [Spy_not_see_PMS]) 2);
   1.415  by (blast_tac (!claset addSEs [MPair_parts]
   1.416  		       addDs  [Notes_Crypt_parts_sees,
   1.417 @@ -654,11 +589,12 @@
   1.418  \  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
   1.419  \      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (sees Spy evs) -->  \
   1.420  \      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
   1.421 -by (analz_induct_tac 1);
   1.422 +by (analz_induct_tac 1);	(*13 seconds*)
   1.423  by (REPEAT_FIRST (rtac impI));
   1.424 +(*ClientCertKeyEx*)
   1.425 +by (Blast_tac 2);
   1.426  (*Fake: the Spy doesn't have the critical session key!*)
   1.427 -by (subgoal_tac 
   1.428 -    "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz (sees Spy evsa)" 1);
   1.429 +by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(sees Spy evsa)" 1);
   1.430  by (asm_simp_tac (!simpset addsimps [Spy_not_see_MS, 
   1.431  				     not_parts_not_analz]) 2);
   1.432  by (Fake_parts_insert_tac 1);