Many minor speedups:
authorpaulson
Tue Oct 21 10:39:27 1997 +0200 (1997-10-21)
changeset 39616a8996fb7d99
parent 3960 7a38fae985f9
child 3962 69c76eb80273
Many minor speedups:
1. Some use of rewriting with expand_ifs instead of addsplits[expand_if]
2. Faster proof of new_keys_not_used
3. New version of shrK_neq (no longer refers to "range")
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/TLS.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Tue Oct 21 10:36:23 1997 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Tue Oct 21 10:39:27 1997 +0200
     1.3 @@ -74,7 +74,7 @@
     1.4   "!!evs. evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
     1.5  by (parts_induct_tac 1);
     1.6  by (Fake_parts_insert_tac 1);
     1.7 -by (Blast_tac 1);
     1.8 +by (ALLGOALS Blast_tac);
     1.9  qed "Spy_see_shrK";
    1.10  Addsimps [Spy_see_shrK];
    1.11  
    1.12 @@ -99,10 +99,10 @@
    1.13  by (parts_induct_tac 1);
    1.14  (*Fake*)
    1.15  by (best_tac
    1.16 -      (!claset addIs [impOfSubs analz_subset_parts]
    1.17 -               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.18 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.19 -               addss (!simpset)) 1);
    1.20 +      (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.21 +               addIs  [impOfSubs analz_subset_parts]
    1.22 +               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    1.23 +               addss  (!simpset)) 1);
    1.24  (*NS2, NS4, NS5*)
    1.25  by (ALLGOALS (blast_tac (!claset addSEs spies_partsEs)));
    1.26  qed_spec_mp "new_keys_not_used";
    1.27 @@ -203,8 +203,8 @@
    1.28  by (etac ns_shared.induct 1);
    1.29  by analz_spies_tac;
    1.30  by (REPEAT_FIRST (resolve_tac [allI, impI]));
    1.31 -by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
    1.32 -(*Takes 24 secs*)
    1.33 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
    1.34 +(*Takes 9 secs*)
    1.35  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
    1.36  (*Fake*) 
    1.37  by (spy_analz_tac 2);
    1.38 @@ -255,7 +255,7 @@
    1.39  (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
    1.40  
    1.41  goal thy 
    1.42 - "!!evs. [| A ~: bad;  B ~: bad;  evs : ns_shared |]            \
    1.43 + "!!evs. [| A ~: bad;  B ~: bad;  evs : ns_shared |]                   \
    1.44  \        ==> Says Server A                                             \
    1.45  \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
    1.46  \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
    1.47 @@ -266,8 +266,8 @@
    1.48  by analz_spies_tac;
    1.49  by (ALLGOALS 
    1.50      (asm_simp_tac 
    1.51 -     (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes)
    1.52 -               addsplits [expand_if])));
    1.53 +     (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ 
    1.54 +			 pushes @ expand_ifs))));
    1.55  (*Oops*)
    1.56  by (blast_tac (!claset addDs [unique_session_keys]) 5);
    1.57  (*NS3, replay sub-case*) 
     2.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Oct 21 10:36:23 1997 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Oct 21 10:39:27 1997 +0200
     2.3 @@ -86,7 +86,7 @@
     2.4   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
     2.5  by (parts_induct_tac 1);
     2.6  by (Fake_parts_insert_tac 1);
     2.7 -by (Blast_tac 1);
     2.8 +by (ALLGOALS Blast_tac);
     2.9  qed "Spy_see_shrK";
    2.10  Addsimps [Spy_see_shrK];
    2.11  
    2.12 @@ -110,10 +110,10 @@
    2.13  by (parts_induct_tac 1);
    2.14  (*Fake*)
    2.15  by (best_tac
    2.16 -      (!claset addIs [impOfSubs analz_subset_parts]
    2.17 -               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    2.18 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    2.19 -               addss (!simpset)) 1);
    2.20 +      (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    2.21 +               addIs  [impOfSubs analz_subset_parts]
    2.22 +               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    2.23 +               addss  (!simpset)) 1);
    2.24  by (ALLGOALS Blast_tac);
    2.25  qed_spec_mp "new_keys_not_used";
    2.26  
    2.27 @@ -339,7 +339,7 @@
    2.28  by (ALLGOALS
    2.29      (asm_simp_tac (!simpset addcongs [conj_cong] 
    2.30                              addsimps [analz_insert_eq, analz_insert_freshK]
    2.31 -                            addsplits [expand_if])));
    2.32 +                            addsimps (pushes@expand_ifs))));
    2.33  (*Oops*)
    2.34  by (blast_tac (!claset addSDs [unique_session_keys]) 4);
    2.35  (*OR4*) 
     3.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Oct 21 10:36:23 1997 +0200
     3.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Oct 21 10:39:27 1997 +0200
     3.3 @@ -76,7 +76,7 @@
     3.4   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
     3.5  by (parts_induct_tac 1);
     3.6  by (Fake_parts_insert_tac 1);
     3.7 -by (Blast_tac 1);
     3.8 +by (ALLGOALS Blast_tac);
     3.9  qed "Spy_see_shrK";
    3.10  Addsimps [Spy_see_shrK];
    3.11  
    3.12 @@ -100,10 +100,10 @@
    3.13  by (parts_induct_tac 1);
    3.14  (*Fake*)
    3.15  by (best_tac
    3.16 -      (!claset addIs [impOfSubs analz_subset_parts]
    3.17 -               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    3.18 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    3.19 -               addss (!simpset)) 1);
    3.20 +      (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    3.21 +               addIs  [impOfSubs analz_subset_parts]
    3.22 +               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    3.23 +               addss  (!simpset)) 1);
    3.24  (*OR3*)
    3.25  by (Blast_tac 1);
    3.26  qed_spec_mp "new_keys_not_used";
    3.27 @@ -268,7 +268,7 @@
    3.28  by (ALLGOALS
    3.29      (asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong] 
    3.30                              addsimps [analz_insert_eq, analz_insert_freshK]
    3.31 -                            addsplits [expand_if])));
    3.32 +                            addsimps (pushes@expand_ifs))));
    3.33  (*Oops*)
    3.34  by (blast_tac (!claset addSDs [unique_session_keys]) 4);
    3.35  (*OR4*) 
     4.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Oct 21 10:36:23 1997 +0200
     4.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Oct 21 10:39:27 1997 +0200
     4.3 @@ -88,7 +88,7 @@
     4.4   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
     4.5  by (parts_induct_tac 1);
     4.6  by (Fake_parts_insert_tac 1);
     4.7 -by (Blast_tac 1);
     4.8 +by (ALLGOALS Blast_tac);
     4.9  qed "Spy_see_shrK";
    4.10  Addsimps [Spy_see_shrK];
    4.11  
    4.12 @@ -112,10 +112,10 @@
    4.13  by (parts_induct_tac 1);
    4.14  (*Fake*)
    4.15  by (best_tac
    4.16 -      (!claset addIs [impOfSubs analz_subset_parts]
    4.17 -               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    4.18 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    4.19 -               addss (!simpset)) 1);
    4.20 +      (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    4.21 +               addIs  [impOfSubs analz_subset_parts]
    4.22 +               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    4.23 +               addss  (!simpset)) 1);
    4.24  (*OR1-3*)
    4.25  by (ALLGOALS Blast_tac);
    4.26  qed_spec_mp "new_keys_not_used";
    4.27 @@ -231,7 +231,7 @@
    4.28  by (ALLGOALS
    4.29      (asm_simp_tac (!simpset addcongs [conj_cong] 
    4.30                              addsimps [analz_insert_eq, analz_insert_freshK]
    4.31 -                            addsplits [expand_if])));
    4.32 +                            addsimps (pushes@expand_ifs))));
    4.33  (*Oops*)
    4.34  by (blast_tac (!claset addSDs [unique_session_keys]) 4);
    4.35  (*OR4*) 
     5.1 --- a/src/HOL/Auth/Recur.ML	Tue Oct 21 10:36:23 1997 +0200
     5.2 +++ b/src/HOL/Auth/Recur.ML	Tue Oct 21 10:39:27 1997 +0200
     5.3 @@ -192,10 +192,10 @@
     5.4  	      addss  (!simpset addsimps [parts_insert_spies])) 2);
     5.5  (*Fake*)
     5.6  by (best_tac
     5.7 -      (!claset addIs [impOfSubs analz_subset_parts]
     5.8 -               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
     5.9 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    5.10 -               addss (!simpset)) 1);
    5.11 +      (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    5.12 +               addIs  [impOfSubs analz_subset_parts]
    5.13 +               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    5.14 +               addss  (!simpset)) 1);
    5.15  qed_spec_mp "new_keys_not_used";
    5.16  
    5.17  
    5.18 @@ -263,7 +263,7 @@
    5.19  *)
    5.20  bind_thm ("resp_analz_image_freshK",
    5.21            raw_analz_image_freshK RSN
    5.22 -            (2, resp_analz_image_freshK_lemma) RS spec RS spec);
    5.23 +            (2, resp_analz_image_freshK_lemma) RS spec RS spec RS mp);
    5.24  
    5.25  goal thy
    5.26   "!!evs. [| evs : recur;  KAB ~: range shrK |] ==>              \
    5.27 @@ -422,25 +422,26 @@
    5.28  by (etac respond.induct 1);
    5.29  by (forward_tac [respond_imp_responses] 2);
    5.30  by (forward_tac [respond_imp_not_used] 2);
    5.31 -by (ALLGOALS (*12 seconds*)
    5.32 +by (ALLGOALS (*6 seconds*)
    5.33      (asm_simp_tac 
    5.34 -     (analz_image_freshK_ss addsimps 
    5.35 -       [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2])));
    5.36 +     (analz_image_freshK_ss 
    5.37 +        addsimps expand_ifs
    5.38 +	addsimps 
    5.39 +          [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2])));
    5.40  by (ALLGOALS (simp_tac (!simpset addsimps [ex_disj_distrib])));
    5.41  (** LEVEL 5 **)
    5.42  by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
    5.43 -by (safe_tac (!claset addSEs [MPair_parts]));
    5.44 -by (REPEAT (blast_tac (!claset addSDs [respond_certificate]
    5.45 -		               addDs [resp_analz_insert]
    5.46 -			       addIs  [impOfSubs analz_subset_parts]) 4));
    5.47 -by (Blast_tac 3);
    5.48 -by (blast_tac (!claset addSEs partsEs
    5.49 -                       addDs [Key_in_parts_respond]) 2);
    5.50 -(*by unicity, either B=Aa or B=A', a contradiction since B: bad*)
    5.51 -by (dtac unique_session_keys 1);
    5.52 -by (etac respond_certificate 1);
    5.53 -by (assume_tac 1);
    5.54 -by (Blast_tac 1);
    5.55 +by (REPEAT_FIRST (resolve_tac [allI, conjI, impI]));
    5.56 +by (ALLGOALS Clarify_tac);
    5.57 +by (blast_tac (!claset addSDs  [resp_analz_insert]
    5.58 +		       addIs  [impOfSubs analz_subset_parts]) 2);
    5.59 +by (blast_tac (!claset addSDs [respond_certificate]) 1);
    5.60 +by (Asm_full_simp_tac 1);
    5.61 +(*by unicity, either B=Aa or B=A', a contradiction if B: bad*)
    5.62 +by (blast_tac
    5.63 +    (!claset addSEs [MPair_parts]
    5.64 +	     addDs [parts.Body,
    5.65 +		    respond_certificate RSN (2, unique_session_keys)]) 1);
    5.66  qed_spec_mp "respond_Spy_not_see_session_key";
    5.67  
    5.68  
    5.69 @@ -453,9 +454,9 @@
    5.70  by analz_spies_tac;
    5.71  by (ALLGOALS
    5.72      (asm_simp_tac
    5.73 -     (!simpset addsimps [analz_insert_eq, parts_insert_spies, 
    5.74 -			 analz_insert_freshK] 
    5.75 -               addsplits [expand_if])));
    5.76 +     (!simpset addsimps (expand_ifs @
    5.77 +			 [analz_insert_eq, parts_insert_spies, 
    5.78 +			  analz_insert_freshK]))));
    5.79  (*RA4*)
    5.80  by (spy_analz_tac 5);
    5.81  (*RA2*)
     6.1 --- a/src/HOL/Auth/Shared.ML	Tue Oct 21 10:36:23 1997 +0200
     6.2 +++ b/src/HOL/Auth/Shared.ML	Tue Oct 21 10:39:27 1997 +0200
     6.3 @@ -81,13 +81,12 @@
     6.4  by (Blast_tac 1);
     6.5  qed "Key_not_used";
     6.6  
     6.7 -(*A session key cannot clash with a long-term shared key*)
     6.8 -goal thy "!!K. K ~: range shrK ==> shrK B ~= K";
     6.9 +goal thy "!!K. Key K ~: used evs ==> shrK B ~= K";
    6.10  by (Blast_tac 1);
    6.11  qed "shrK_neq";
    6.12  
    6.13  Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
    6.14 -Delsimps [image_eqI]; (* loops together with shrK_neq *)
    6.15 +
    6.16  
    6.17  (*** Fresh nonces ***)
    6.18  
     7.1 --- a/src/HOL/Auth/TLS.ML	Tue Oct 21 10:36:23 1997 +0200
     7.2 +++ b/src/HOL/Auth/TLS.ML	Tue Oct 21 10:39:27 1997 +0200
     7.3 @@ -17,8 +17,13 @@
     7.4    rollback attacks).
     7.5  *)
     7.6  
     7.7 +open TLS;
     7.8  
     7.9 -open TLS;
    7.10 +val if_distrib_parts = 
    7.11 +    read_instantiate_sg (sign_of Message.thy) [("f", "parts")] if_distrib;
    7.12 +
    7.13 +val if_distrib_analz = 
    7.14 +    read_instantiate_sg (sign_of Message.thy) [("f", "analz")] if_distrib;
    7.15  
    7.16  proof_timing:=true;
    7.17  HOL_quantifiers := false;
    7.18 @@ -198,6 +203,7 @@
    7.19      ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
    7.20      ALLGOALS (asm_simp_tac 
    7.21                (!simpset addcongs [if_weak_cong]
    7.22 +                        addsimps (expand_ifs@pushes)
    7.23                          addsplits [expand_if]))  THEN
    7.24      (*Remove instances of pubK B:  the Spy already knows all public keys.
    7.25        Combining the two simplifier calls makes them run extremely slowly.*)
    7.26 @@ -396,7 +402,7 @@
    7.27   "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
    7.28  \        (X : analz (G Un H))  =  (X : analz H)";
    7.29  by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
    7.30 -val lemma = result();
    7.31 +val analz_image_keys_lemma = result();
    7.32  
    7.33  (** Strangely, the following version doesn't work:
    7.34  \    ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \
    7.35 @@ -411,9 +417,10 @@
    7.36  by (etac tls.induct 1);
    7.37  by (ClientKeyExch_tac 7);
    7.38  by (REPEAT_FIRST (resolve_tac [allI, impI]));
    7.39 -by (REPEAT_FIRST (rtac lemma));
    7.40 -by (ALLGOALS    (*24 seconds*)
    7.41 +by (REPEAT_FIRST (rtac analz_image_keys_lemma));
    7.42 +by (ALLGOALS    (*15 seconds*)
    7.43      (asm_simp_tac (analz_image_keys_ss 
    7.44 +		   addsimps (expand_ifs@pushes)
    7.45  		   addsimps [range_sessionkeys_not_priK, 
    7.46                               analz_image_priK, certificate_def])));
    7.47  by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb])));
     8.1 --- a/src/HOL/Auth/Yahalom.ML	Tue Oct 21 10:36:23 1997 +0200
     8.2 +++ b/src/HOL/Auth/Yahalom.ML	Tue Oct 21 10:39:27 1997 +0200
     8.3 @@ -82,7 +82,7 @@
     8.4   "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
     8.5  by (parts_induct_tac 1);
     8.6  by (Fake_parts_insert_tac 1);
     8.7 -by (Blast_tac 1);
     8.8 +by (ALLGOALS Blast_tac);
     8.9  qed "Spy_see_shrK";
    8.10  Addsimps [Spy_see_shrK];
    8.11  
    8.12 @@ -105,16 +105,14 @@
    8.13  goal thy "!!evs. evs : yahalom ==>          \
    8.14  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    8.15  by (parts_induct_tac 1);
    8.16 -(*YM4: Key K is not fresh!*)
    8.17 -by (blast_tac (!claset addSEs spies_partsEs) 3);
    8.18 -(*YM3*)
    8.19 -by (Blast_tac 2);
    8.20  (*Fake*)
    8.21  by (best_tac
    8.22 -      (!claset addIs [impOfSubs analz_subset_parts]
    8.23 -               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    8.24 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    8.25 -               addss (!simpset)) 1);
    8.26 +      (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    8.27 +               addIs  [impOfSubs analz_subset_parts]
    8.28 +               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    8.29 +               addss  (!simpset)) 1);
    8.30 +(*YM2-4: Because Key K is not fresh, etc.*)
    8.31 +by (REPEAT (blast_tac (!claset addSEs spies_partsEs) 1));
    8.32  qed_spec_mp "new_keys_not_used";
    8.33  
    8.34  bind_thm ("new_keys_not_analzd",
    8.35 @@ -226,8 +224,8 @@
    8.36  by analz_spies_tac;
    8.37  by (ALLGOALS
    8.38      (asm_simp_tac 
    8.39 -     (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
    8.40 -               addsplits [expand_if])));
    8.41 +     (!simpset addsimps (expand_ifs@pushes)
    8.42 +	       addsimps [analz_insert_eq, analz_insert_freshK])));
    8.43  (*Oops*)
    8.44  by (blast_tac (!claset addDs [unique_session_keys]) 3);
    8.45  (*YM3*)
    8.46 @@ -365,7 +363,7 @@
    8.47   "!!evs. P --> (X : analz (G Un H)) --> (X : analz H)  ==> \
    8.48  \        P --> (X : analz (G Un H)) = (X : analz H)";
    8.49  by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
    8.50 -val lemma = result();
    8.51 +val Nonce_secrecy_lemma = result();
    8.52  
    8.53  goal thy 
    8.54   "!!evs. evs : yahalom ==>                                         \
    8.55 @@ -376,17 +374,18 @@
    8.56  by (etac yahalom.induct 1);
    8.57  by analz_spies_tac;
    8.58  by (REPEAT_FIRST (resolve_tac [impI RS allI]));
    8.59 -by (REPEAT_FIRST (rtac lemma));
    8.60 +by (REPEAT_FIRST (rtac Nonce_secrecy_lemma));
    8.61  (*For Oops, simplification proves NBa~=NB.  By Says_Server_KeyWithNonce,
    8.62    we get (~ KeyWithNonce K NB evsa); then simplification can apply the
    8.63    induction hypothesis with KK = {K}.*)
    8.64 -by (ALLGOALS  (*17 seconds*)
    8.65 +by (ALLGOALS  (*12 seconds*)
    8.66      (asm_simp_tac 
    8.67 -     (analz_image_freshK_ss addsimps
    8.68 -        [all_conj_distrib, analz_image_freshK,
    8.69 -	 KeyWithNonce_Says, fresh_not_KeyWithNonce, 
    8.70 -	 imp_disj_not1,			      (*Moves NBa~=NB to the front*)
    8.71 -	 Says_Server_KeyWithNonce])));
    8.72 +     (analz_image_freshK_ss 
    8.73 +       addsimps expand_ifs
    8.74 +       addsimps [all_conj_distrib, analz_image_freshK,
    8.75 +		 KeyWithNonce_Says, fresh_not_KeyWithNonce, 
    8.76 +		 imp_disj_not1,		     (*Moves NBa~=NB to the front*)
    8.77 +		 Says_Server_KeyWithNonce])));
    8.78  (*Base*)
    8.79  by (Blast_tac 1);
    8.80  (*Fake*) 
    8.81 @@ -498,8 +497,8 @@
    8.82  by analz_spies_tac;
    8.83  by (ALLGOALS
    8.84      (asm_simp_tac 
    8.85 -     (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
    8.86 -               addsplits [expand_if])));
    8.87 +     (!simpset addsimps (expand_ifs@pushes)
    8.88 +	       addsimps [analz_insert_eq, analz_insert_freshK])));
    8.89  (*Prove YM3 by showing that no NB can also be an NA*)
    8.90  by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj]
    8.91  	               addSEs [MPair_parts]
     9.1 --- a/src/HOL/Auth/Yahalom.thy	Tue Oct 21 10:36:23 1997 +0200
     9.2 +++ b/src/HOL/Auth/Yahalom.thy	Tue Oct 21 10:39:27 1997 +0200
     9.3 @@ -49,7 +49,8 @@
     9.4                  # evs3 : yahalom"
     9.5  
     9.6           (*Alice receives the Server's (?) message, checks her Nonce, and
     9.7 -           uses the new session key to send Bob his Nonce.*)
     9.8 +           uses the new session key to send Bob his Nonce.  The premise
     9.9 +           A ~= Server is needed to prove Says_Server_message_form.*)
    9.10      YM4  "[| evs4: yahalom;  A ~= Server;  
    9.11               Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|},
    9.12                          X|}  : set evs4;
    10.1 --- a/src/HOL/Auth/Yahalom2.ML	Tue Oct 21 10:36:23 1997 +0200
    10.2 +++ b/src/HOL/Auth/Yahalom2.ML	Tue Oct 21 10:39:27 1997 +0200
    10.3 @@ -111,10 +111,10 @@
    10.4  by (blast_tac (!claset addss (!simpset)) 2);
    10.5  (*Fake*)
    10.6  by (best_tac
    10.7 -      (!claset addIs [impOfSubs analz_subset_parts]
    10.8 -               addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    10.9 -                      impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   10.10 -               addss (!simpset)) 1);
   10.11 +      (!claset addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
   10.12 +               addIs  [impOfSubs analz_subset_parts]
   10.13 +               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
   10.14 +               addss  (!simpset)) 1);
   10.15  qed_spec_mp "new_keys_not_used";
   10.16  
   10.17  bind_thm ("new_keys_not_analzd",
   10.18 @@ -164,7 +164,7 @@
   10.19  by (etac yahalom.induct 1);
   10.20  by analz_spies_tac;
   10.21  by (REPEAT_FIRST (resolve_tac [allI, impI]));
   10.22 -by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
   10.23 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
   10.24  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
   10.25  (*Fake*) 
   10.26  by (spy_analz_tac 2);
   10.27 @@ -226,7 +226,8 @@
   10.28  by analz_spies_tac;
   10.29  by (ALLGOALS
   10.30      (asm_simp_tac 
   10.31 -     (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
   10.32 +     (!simpset addsimps expand_ifs
   10.33 +	       addsimps [analz_insert_eq, analz_insert_freshK]
   10.34                 addsplits [expand_if])));
   10.35  (*Oops*)
   10.36  by (blast_tac (!claset addDs [unique_session_keys]) 3);