Making proofs faster, especially using keysFor_parts_insert
authorpaulson
Fri Jan 02 17:15:19 1998 +0100 (1998-01-02)
changeset 4509828148415197
parent 4508 f102cb0140fe
child 4510 a37f515a0b25
Making proofs faster, especially using keysFor_parts_insert
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/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Fri Jan 02 13:24:53 1998 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Fri Jan 02 17:15:19 1998 +0100
     1.3 @@ -97,11 +97,7 @@
     1.4  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
     1.5  by (parts_induct_tac 1);
     1.6  (*Fake*)
     1.7 -by (best_tac
     1.8 -      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
     1.9 -                addIs  [impOfSubs analz_subset_parts]
    1.10 -                addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    1.11 -                addss  (simpset())) 1);
    1.12 +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    1.13  (*NS2, NS4, NS5*)
    1.14  by (ALLGOALS (Blast_tac));
    1.15  qed_spec_mp "new_keys_not_used";
    1.16 @@ -271,7 +267,7 @@
    1.17       (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @ 
    1.18  			  pushes @ expand_ifs))));
    1.19  (*Oops*)
    1.20 -by (blast_tac (claset() addDs [unique_session_keys]) 5);
    1.21 +by (blast_tac (claset() addSDs [unique_session_keys]) 5);
    1.22  (*NS3, replay sub-case*) 
    1.23  by (Blast_tac 4);
    1.24  (*NS2*)
     2.1 --- a/src/HOL/Auth/OtwayRees.ML	Fri Jan 02 13:24:53 1998 +0100
     2.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Jan 02 17:15:19 1998 +0100
     2.3 @@ -110,11 +110,7 @@
     2.4  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
     2.5  by (parts_induct_tac 1);
     2.6  (*Fake*)
     2.7 -by (best_tac
     2.8 -      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
     2.9 -		addIs  [impOfSubs analz_subset_parts]
    2.10 -		addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    2.11 -		addss  (simpset())) 1);
    2.12 +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    2.13  by (ALLGOALS Blast_tac);
    2.14  qed_spec_mp "new_keys_not_used";
    2.15  
    2.16 @@ -202,7 +198,7 @@
    2.17  by (expand_case_tac "K = ?y" 1);
    2.18  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    2.19  (*...we assume X is a recent message, and handle this case by contradiction*)
    2.20 -by (Blast_tac 1);
    2.21 +by (blast_tac (claset() addSEs spies_partsEs) 1);
    2.22  val lemma = result();
    2.23  
    2.24  goal thy 
    2.25 @@ -329,8 +325,8 @@
    2.26  by analz_spies_tac;
    2.27  by (ALLGOALS
    2.28      (asm_simp_tac (simpset() addcongs [conj_cong] 
    2.29 -                            addsimps [analz_insert_eq, analz_insert_freshK]
    2.30 -                            addsimps (pushes@expand_ifs))));
    2.31 +                             addsimps [analz_insert_eq, analz_insert_freshK]
    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	Fri Jan 02 13:24:53 1998 +0100
     3.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Jan 02 17:15:19 1998 +0100
     3.3 @@ -99,11 +99,7 @@
     3.4  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
     3.5  by (parts_induct_tac 1);
     3.6  (*Fake*)
     3.7 -by (best_tac
     3.8 -      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
     3.9 -		addIs  [impOfSubs analz_subset_parts]
    3.10 -		addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    3.11 -		addss  (simpset())) 1);
    3.12 +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    3.13  (*OR3*)
    3.14  by (Blast_tac 1);
    3.15  qed_spec_mp "new_keys_not_used";
    3.16 @@ -195,7 +191,7 @@
    3.17  by (expand_case_tac "K = ?y" 1);
    3.18  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    3.19  (*...we assume X is a recent message and handle this case by contradiction*)
    3.20 -by (Blast_tac 1);
    3.21 +by (blast_tac (claset() addSEs spies_partsEs) 1);
    3.22  val lemma = result();
    3.23  
    3.24  
    3.25 @@ -263,8 +259,8 @@
    3.26  by analz_spies_tac;
    3.27  by (ALLGOALS
    3.28      (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] 
    3.29 -                            addsimps [analz_insert_eq, analz_insert_freshK]
    3.30 -                            addsimps (pushes@expand_ifs))));
    3.31 +                             addsimps [analz_insert_eq, analz_insert_freshK]
    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	Fri Jan 02 13:24:53 1998 +0100
     4.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Fri Jan 02 17:15:19 1998 +0100
     4.3 @@ -107,11 +107,7 @@
     4.4  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
     4.5  by (parts_induct_tac 1);
     4.6  (*Fake*)
     4.7 -by (best_tac
     4.8 -      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
     4.9 -               addIs  [impOfSubs analz_subset_parts]
    4.10 -               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    4.11 -               addss  (simpset())) 1);
    4.12 +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    4.13  (*OR1-3*)
    4.14  by (ALLGOALS Blast_tac);
    4.15  qed_spec_mp "new_keys_not_used";
     5.1 --- a/src/HOL/Auth/Recur.ML	Fri Jan 02 13:24:53 1998 +0100
     5.2 +++ b/src/HOL/Auth/Recur.ML	Fri Jan 02 17:15:19 1998 +0100
     5.3 @@ -170,9 +170,10 @@
     5.4  
     5.5  (** Nobody can have used non-existent keys! **)
     5.6  
     5.7 +(*The special case of H={} has the same proof*)
     5.8  goal thy
     5.9 - "!!evs. [| K : keysFor (parts {RB});  (PB,RB,K') : respond evs |] \
    5.10 -\        ==> K : range shrK";
    5.11 + "!!evs. [| K : keysFor (parts (insert RB H));  (PB,RB,K') : respond evs |] \
    5.12 +\        ==> K : range shrK | K : keysFor (parts H)";
    5.13  by (etac rev_mp 1);
    5.14  by (etac (respond_imp_responses RS responses.induct) 1);
    5.15  by Auto_tac;
    5.16 @@ -183,14 +184,9 @@
    5.17  \                Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    5.18  by (parts_induct_tac 1);
    5.19  (*RA3*)
    5.20 -by (best_tac (claset() addDs  [Key_in_keysFor_parts]
    5.21 -	      addss  (simpset() addsimps [parts_insert_spies])) 2);
    5.22 +by (blast_tac (claset() addSDs [Key_in_keysFor_parts]) 2);
    5.23  (*Fake*)
    5.24 -by (best_tac
    5.25 -      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    5.26 -               addIs  [impOfSubs analz_subset_parts]
    5.27 -               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    5.28 -               addss  (simpset())) 1);
    5.29 +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    5.30  qed_spec_mp "new_keys_not_used";
    5.31  
    5.32  
     6.1 --- a/src/HOL/Auth/Shared.ML	Fri Jan 02 13:24:53 1998 +0100
     6.2 +++ b/src/HOL/Auth/Shared.ML	Fri Jan 02 17:15:19 1998 +0100
     6.3 @@ -28,6 +28,16 @@
     6.4  qed "keysFor_parts_initState";
     6.5  Addsimps [keysFor_parts_initState];
     6.6  
     6.7 +(*Specialized to shared-key model: no need for addss in protocol proofs*)
     6.8 +goal thy "!!X. [| K: keysFor (parts (insert X H));  X : synth (analz H) |] \
     6.9 +\              ==> K : keysFor (parts H) | Key K : parts H";
    6.10 +by (fast_tac
    6.11 +      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    6.12 +			impOfSubs (analz_subset_parts RS keysFor_mono)]
    6.13 +		addIs  [impOfSubs analz_subset_parts]
    6.14 +                addss  (simpset())) 1);
    6.15 +qed "keysFor_parts_insert";
    6.16 +
    6.17  goal thy "!!H. Crypt K X : H ==> K : keysFor H";
    6.18  by (dtac Crypt_imp_invKey_keysFor 1);
    6.19  by (Asm_full_simp_tac 1);
     7.1 --- a/src/HOL/Auth/Yahalom.ML	Fri Jan 02 13:24:53 1998 +0100
     7.2 +++ b/src/HOL/Auth/Yahalom.ML	Fri Jan 02 17:15:19 1998 +0100
     7.3 @@ -101,11 +101,7 @@
     7.4  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
     7.5  by (parts_induct_tac 1);
     7.6  (*Fake*)
     7.7 -by (best_tac
     7.8 -      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
     7.9 -                addIs  [impOfSubs analz_subset_parts]
    7.10 -                addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    7.11 -                addss  (simpset())) 1);
    7.12 +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    7.13  (*YM2-4: Because Key K is not fresh, etc.*)
    7.14  by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1));
    7.15  qed_spec_mp "new_keys_not_used";
    7.16 @@ -587,7 +583,7 @@
    7.17  by (ALLGOALS Asm_simp_tac);
    7.18  (*YM4*)
    7.19  by (Blast_tac 2);
    7.20 -(*YM3*)
    7.21 +(*YM3 [blast_tac is 50% slower] *)
    7.22  by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj]
    7.23  		       addSEs [MPair_parts]) 1);
    7.24  val lemma = result() RSN (2, rev_mp) RS mp |> standard;
     8.1 --- a/src/HOL/Auth/Yahalom2.ML	Fri Jan 02 13:24:53 1998 +0100
     8.2 +++ b/src/HOL/Auth/Yahalom2.ML	Fri Jan 02 17:15:19 1998 +0100
     8.3 @@ -105,11 +105,7 @@
     8.4  (*YM3*)
     8.5  by (blast_tac (claset() addss (simpset())) 2);
     8.6  (*Fake*)
     8.7 -by (best_tac
     8.8 -     (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
     8.9 -               addIs  [impOfSubs analz_subset_parts]
    8.10 -               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    8.11 -               addss  (simpset())) 1);
    8.12 +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    8.13  qed_spec_mp "new_keys_not_used";
    8.14  
    8.15  bind_thm ("new_keys_not_analzd",