Deleted an obsolete step in TrustServerFinished
authorpaulson
Thu Sep 25 12:20:24 1997 +0200 (1997-09-25)
changeset 37112f86b403d975
parent 3710 ea830f6e3c2d
child 3712 242546f35f8e
Deleted an obsolete step in TrustServerFinished
src/HOL/Auth/TLS.ML
     1.1 --- a/src/HOL/Auth/TLS.ML	Thu Sep 25 12:19:41 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Thu Sep 25 12:20:24 1997 +0200
     1.3 @@ -253,7 +253,7 @@
     1.4  \        |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)";
     1.5  by (etac rev_mp 1);
     1.6  by (parts_induct_tac 1);
     1.7 -by clarify_tac;
     1.8 +by (ALLGOALS Clarify_tac);
     1.9  (*Fake*)
    1.10  by (blast_tac (!claset addIs [parts_insertI]) 1);
    1.11  (*Client, Server Accept*)
    1.12 @@ -610,7 +610,7 @@
    1.13  \      Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
    1.14  \      A = A'";
    1.15  by (analz_induct_tac 1);	(*17 seconds*)
    1.16 -by clarify_tac;
    1.17 +by (ALLGOALS Clarify_tac);
    1.18  (*ClientFinished, ClientResume: by unicity of PMS*)
    1.19  by (REPEAT 
    1.20      (blast_tac (!claset addSDs [Notes_master_imp_Notes_PMS]
    1.21 @@ -632,7 +632,7 @@
    1.22  by (etac tls.induct 1);
    1.23  (*This roundabout proof sequence avoids looping in simplification*)
    1.24  by (ALLGOALS Simp_tac);
    1.25 -by clarify_tac;
    1.26 +by (ALLGOALS Clarify_tac);
    1.27  by (Fake_parts_insert_tac 1);
    1.28  by (ALLGOALS Asm_simp_tac);
    1.29  (*Oops*)
    1.30 @@ -654,7 +654,7 @@
    1.31  \      Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
    1.32  \      B = B'";
    1.33  by (analz_induct_tac 1);	(*17 seconds*)
    1.34 -by clarify_tac;
    1.35 +by (ALLGOALS Clarify_tac);
    1.36  (*ServerResume, ServerFinished: by unicity of PMS*)
    1.37  by (REPEAT
    1.38      (blast_tac (!claset addSEs [MPair_parts]
    1.39 @@ -679,7 +679,7 @@
    1.40  by (etac tls.induct 1);
    1.41  (*This roundabout proof sequence avoids looping in simplification*)
    1.42  by (ALLGOALS Simp_tac);
    1.43 -by clarify_tac;
    1.44 +by (ALLGOALS Clarify_tac);
    1.45  by (Fake_parts_insert_tac 1);
    1.46  by (ALLGOALS Asm_simp_tac);
    1.47  (*Oops*)
    1.48 @@ -711,9 +711,8 @@
    1.49  by (hyp_subst_tac 1);
    1.50  by (analz_induct_tac 1);        (*27 seconds*)
    1.51  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
    1.52 -by clarify_tac;
    1.53 -(*ServerResume*)
    1.54 -by (Blast_tac 3);
    1.55 +(*proves ServerResume*)
    1.56 +by (ALLGOALS Clarify_tac);
    1.57  (*ClientCertKeyEx*)
    1.58  by (fast_tac  (*blast_tac gives PROOF FAILED*)
    1.59      (!claset addSEs [PMS_Crypt_sessionK_not_spied RSN (2,rev_notE)]) 2);
    1.60 @@ -758,7 +757,7 @@
    1.61  by (hyp_subst_tac 1);
    1.62  by (analz_induct_tac 1);	(*20 seconds*)
    1.63  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
    1.64 -by clarify_tac;
    1.65 +by (ALLGOALS Clarify_tac);
    1.66  (*ServerResume, ServerFinished: by unicity of PMS*)
    1.67  by (REPEAT
    1.68      (blast_tac (!claset addSEs [MPair_parts]
    1.69 @@ -805,7 +804,7 @@
    1.70  \      Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y : parts (spies evs) -->  \
    1.71  \      Says A B (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs";
    1.72  by (analz_induct_tac 1);	(*23 seconds*)
    1.73 -by clarify_tac;
    1.74 +by (ALLGOALS Clarify_tac);
    1.75  (*ClientFinished, ClientResume: by unicity of PMS*)
    1.76  by (REPEAT (blast_tac (!claset delrules [conjI]
    1.77  		               addSDs [Notes_master_imp_Notes_PMS]
    1.78 @@ -852,5 +851,6 @@
    1.79  qed "AuthClientFinished";
    1.80  
    1.81  (*22/9/97: loads in 622s, which is 10 minutes 22 seconds*)
    1.82 +(*24/9/97: loads in 672s, which is 11 minutes 12 seconds [stronger theorems]*)
    1.83  
    1.84