src/HOL/Auth/TLS.ML
changeset 3961 6a8996fb7d99
parent 3919 c036caebfc75
child 4006 84a5efc95dcf
     1.1 --- a/src/HOL/Auth/TLS.ML	Tue Oct 21 10:36:23 1997 +0200
     1.2 +++ b/src/HOL/Auth/TLS.ML	Tue Oct 21 10:39:27 1997 +0200
     1.3 @@ -17,8 +17,13 @@
     1.4    rollback attacks).
     1.5  *)
     1.6  
     1.7 +open TLS;
     1.8  
     1.9 -open TLS;
    1.10 +val if_distrib_parts = 
    1.11 +    read_instantiate_sg (sign_of Message.thy) [("f", "parts")] if_distrib;
    1.12 +
    1.13 +val if_distrib_analz = 
    1.14 +    read_instantiate_sg (sign_of Message.thy) [("f", "analz")] if_distrib;
    1.15  
    1.16  proof_timing:=true;
    1.17  HOL_quantifiers := false;
    1.18 @@ -198,6 +203,7 @@
    1.19      ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
    1.20      ALLGOALS (asm_simp_tac 
    1.21                (!simpset addcongs [if_weak_cong]
    1.22 +                        addsimps (expand_ifs@pushes)
    1.23                          addsplits [expand_if]))  THEN
    1.24      (*Remove instances of pubK B:  the Spy already knows all public keys.
    1.25        Combining the two simplifier calls makes them run extremely slowly.*)
    1.26 @@ -396,7 +402,7 @@
    1.27   "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
    1.28  \        (X : analz (G Un H))  =  (X : analz H)";
    1.29  by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
    1.30 -val lemma = result();
    1.31 +val analz_image_keys_lemma = result();
    1.32  
    1.33  (** Strangely, the following version doesn't work:
    1.34  \    ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
    1.35 @@ -411,9 +417,10 @@
    1.36  by (etac tls.induct 1);
    1.37  by (ClientKeyExch_tac 7);
    1.38  by (REPEAT_FIRST (resolve_tac [allI, impI]));
    1.39 -by (REPEAT_FIRST (rtac lemma));
    1.40 -by (ALLGOALS    (*24 seconds*)
    1.41 +by (REPEAT_FIRST (rtac analz_image_keys_lemma));
    1.42 +by (ALLGOALS    (*15 seconds*)
    1.43      (asm_simp_tac (analz_image_keys_ss 
    1.44 +		   addsimps (expand_ifs@pushes)
    1.45  		   addsimps [range_sessionkeys_not_priK, 
    1.46                               analz_image_priK, certificate_def])));
    1.47  by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));