src/HOL/Auth/TLS.ML
changeset 4422 21238c9d363e
parent 4201 858b3ec2c9db
child 4423 a129b817b58a
     1.1 --- a/src/HOL/Auth/TLS.ML	Tue Dec 16 15:15:38 1997 +0100
     1.2 +++ b/src/HOL/Auth/TLS.ML	Tue Dec 16 15:17:26 1997 +0100
     1.3 @@ -197,14 +197,14 @@
     1.4      ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
     1.5      ALLGOALS (asm_simp_tac 
     1.6                (simpset() addcongs [if_weak_cong]
     1.7 -                        addsimps (expand_ifs@pushes)
     1.8 -                        addsplits [expand_if]))  THEN
     1.9 +                         addsimps (expand_ifs@pushes)
    1.10 +                         addsplits [expand_if]))  THEN
    1.11      (*Remove instances of pubK B:  the Spy already knows all public keys.
    1.12        Combining the two simplifier calls makes them run extremely slowly.*)
    1.13      ALLGOALS (asm_simp_tac 
    1.14                (simpset() addcongs [if_weak_cong]
    1.15 -			addsimps [insert_absorb]
    1.16 -                        addsplits [expand_if]));
    1.17 +			 addsimps [insert_absorb]
    1.18 +                         addsplits [expand_if]));
    1.19  
    1.20  
    1.21  (*** Properties of items found in Notes ***)
    1.22 @@ -228,7 +228,7 @@
    1.23  by (blast_tac (claset() addIs [parts_insertI]) 1);
    1.24  (*Client, Server Accept*)
    1.25  by (REPEAT (blast_tac (claset() addSEs spies_partsEs
    1.26 -                               addSDs [Notes_Crypt_parts_spies]) 1));
    1.27 +                                addSDs [Notes_Crypt_parts_spies]) 1));
    1.28  qed "Notes_master_imp_Crypt_PMS";
    1.29  
    1.30  (*Compared with the theorem above, both premise and conclusion are stronger*)
    1.31 @@ -380,9 +380,7 @@
    1.32      (asm_simp_tac (analz_image_keys_ss
    1.33  		   addsimps (certificate_def::keys_distinct))));
    1.34  (*Fake*) 
    1.35 -by (spy_analz_tac 2);
    1.36 -(*Base*)
    1.37 -by (Blast_tac 1);
    1.38 +by (spy_analz_tac 1);
    1.39  qed_spec_mp "analz_image_priK";
    1.40  
    1.41  
    1.42 @@ -412,16 +410,14 @@
    1.43  by (ClientKeyExch_tac 7);
    1.44  by (REPEAT_FIRST (resolve_tac [allI, impI]));
    1.45  by (REPEAT_FIRST (rtac analz_image_keys_lemma));
    1.46 -by (ALLGOALS    (*15 seconds*)
    1.47 +by (ALLGOALS    (*18 seconds*)
    1.48      (asm_simp_tac (analz_image_keys_ss 
    1.49  		   addsimps (expand_ifs@pushes)
    1.50  		   addsimps [range_sessionkeys_not_priK, 
    1.51                               analz_image_priK, certificate_def])));
    1.52  by (ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb])));
    1.53  (*Fake*) 
    1.54 -by (spy_analz_tac 2);
    1.55 -(*Base*)
    1.56 -by (Blast_tac 1);
    1.57 +by (spy_analz_tac 1);
    1.58  qed_spec_mp "analz_image_keys";
    1.59  
    1.60  (*Knowing some session keys is no help in getting new nonces*)
    1.61 @@ -542,7 +538,7 @@
    1.62  by (Blast_tac 3);
    1.63  (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
    1.64  by (blast_tac (claset() addSDs [Spy_not_see_PMS, 
    1.65 -			       Says_imp_spies RS analz.Inj]) 2);
    1.66 +				Says_imp_spies RS analz.Inj]) 2);
    1.67  (*Fake*)
    1.68  by (spy_analz_tac 1);
    1.69  (*ServerHello and ClientKeyExch: mostly freshness reasoning*)
    1.70 @@ -659,7 +655,7 @@
    1.71  \            Notes A {|Agent B, Nonce PMS|} : set evs --> \
    1.72  \            X : parts (spies evs) --> Says B A X : set evs";
    1.73  by (hyp_subst_tac 1);
    1.74 -by (analz_induct_tac 1);        (*22 seconds*)
    1.75 +by (analz_induct_tac 1);        (*26 seconds*)
    1.76  by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
    1.77  (*proves ServerResume*)
    1.78  by (ALLGOALS Clarify_tac);
    1.79 @@ -668,7 +664,7 @@
    1.80  (*Fake: the Spy doesn't have the critical session key!*)
    1.81  by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
    1.82  by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
    1.83 -				     not_parts_not_analz]) 2);
    1.84 +				      not_parts_not_analz]) 2);
    1.85  by (Fake_parts_insert_tac 1);
    1.86  val lemma = normalize_thm [RSmp] (result());
    1.87  
    1.88 @@ -731,7 +727,7 @@
    1.89  \           evs : tls;  A ~: bad;  B ~: bad |]          \
    1.90  \        ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs";
    1.91  by (blast_tac (claset() addIs [lemma]
    1.92 -                       addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
    1.93 +                        addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
    1.94  qed_spec_mp "TrustServerMsg";
    1.95  
    1.96  
    1.97 @@ -760,7 +756,7 @@
    1.98  (*Fake: the Spy doesn't have the critical session key!*)
    1.99  by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
   1.100  by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS, 
   1.101 -				     not_parts_not_analz]) 2);
   1.102 +				      not_parts_not_analz]) 2);
   1.103  by (Fake_parts_insert_tac 1);
   1.104  val lemma = normalize_thm [RSmp] (result());
   1.105