# HG changeset patch # User paulson # Date 883757719 -3600 # Node ID 8281484151972d9c95a53c858c5f395b82e5bcc8 # Parent f102cb0140fe74f3f7e37c494faec25d02fa0cb7 Making proofs faster, especially using keysFor_parts_insert diff -r f102cb0140fe -r 828148415197 src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Fri Jan 02 13:24:53 1998 +0100 +++ b/src/HOL/Auth/NS_Shared.ML Fri Jan 02 17:15:19 1998 +0100 @@ -97,11 +97,7 @@ \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; by (parts_induct_tac 1); (*Fake*) -by (best_tac - (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] - addIs [impOfSubs analz_subset_parts] - addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] - addss (simpset())) 1); +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); (*NS2, NS4, NS5*) by (ALLGOALS (Blast_tac)); qed_spec_mp "new_keys_not_used"; @@ -271,7 +267,7 @@ (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes @ expand_ifs)))); (*Oops*) -by (blast_tac (claset() addDs [unique_session_keys]) 5); +by (blast_tac (claset() addSDs [unique_session_keys]) 5); (*NS3, replay sub-case*) by (Blast_tac 4); (*NS2*) diff -r f102cb0140fe -r 828148415197 src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Fri Jan 02 13:24:53 1998 +0100 +++ b/src/HOL/Auth/OtwayRees.ML Fri Jan 02 17:15:19 1998 +0100 @@ -110,11 +110,7 @@ \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; by (parts_induct_tac 1); (*Fake*) -by (best_tac - (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] - addIs [impOfSubs analz_subset_parts] - addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] - addss (simpset())) 1); +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); by (ALLGOALS Blast_tac); qed_spec_mp "new_keys_not_used"; @@ -202,7 +198,7 @@ by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); (*...we assume X is a recent message, and handle this case by contradiction*) -by (Blast_tac 1); +by (blast_tac (claset() addSEs spies_partsEs) 1); val lemma = result(); goal thy @@ -329,8 +325,8 @@ by analz_spies_tac; by (ALLGOALS (asm_simp_tac (simpset() addcongs [conj_cong] - addsimps [analz_insert_eq, analz_insert_freshK] - addsimps (pushes@expand_ifs)))); + addsimps [analz_insert_eq, analz_insert_freshK] + addsimps (pushes@expand_ifs)))); (*Oops*) by (blast_tac (claset() addSDs [unique_session_keys]) 4); (*OR4*) diff -r f102cb0140fe -r 828148415197 src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Fri Jan 02 13:24:53 1998 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.ML Fri Jan 02 17:15:19 1998 +0100 @@ -99,11 +99,7 @@ \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; by (parts_induct_tac 1); (*Fake*) -by (best_tac - (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] - addIs [impOfSubs analz_subset_parts] - addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] - addss (simpset())) 1); +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); (*OR3*) by (Blast_tac 1); qed_spec_mp "new_keys_not_used"; @@ -195,7 +191,7 @@ by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); (*...we assume X is a recent message and handle this case by contradiction*) -by (Blast_tac 1); +by (blast_tac (claset() addSEs spies_partsEs) 1); val lemma = result(); @@ -263,8 +259,8 @@ by analz_spies_tac; by (ALLGOALS (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] - addsimps [analz_insert_eq, analz_insert_freshK] - addsimps (pushes@expand_ifs)))); + addsimps [analz_insert_eq, analz_insert_freshK] + addsimps (pushes@expand_ifs)))); (*Oops*) by (blast_tac (claset() addSDs [unique_session_keys]) 4); (*OR4*) diff -r f102cb0140fe -r 828148415197 src/HOL/Auth/OtwayRees_Bad.ML --- a/src/HOL/Auth/OtwayRees_Bad.ML Fri Jan 02 13:24:53 1998 +0100 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Fri Jan 02 17:15:19 1998 +0100 @@ -107,11 +107,7 @@ \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; by (parts_induct_tac 1); (*Fake*) -by (best_tac - (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] - addIs [impOfSubs analz_subset_parts] - addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] - addss (simpset())) 1); +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); (*OR1-3*) by (ALLGOALS Blast_tac); qed_spec_mp "new_keys_not_used"; diff -r f102cb0140fe -r 828148415197 src/HOL/Auth/Recur.ML --- a/src/HOL/Auth/Recur.ML Fri Jan 02 13:24:53 1998 +0100 +++ b/src/HOL/Auth/Recur.ML Fri Jan 02 17:15:19 1998 +0100 @@ -170,9 +170,10 @@ (** Nobody can have used non-existent keys! **) +(*The special case of H={} has the same proof*) goal thy - "!!evs. [| K : keysFor (parts {RB}); (PB,RB,K') : respond evs |] \ -\ ==> K : range shrK"; + "!!evs. [| K : keysFor (parts (insert RB H)); (PB,RB,K') : respond evs |] \ +\ ==> K : range shrK | K : keysFor (parts H)"; by (etac rev_mp 1); by (etac (respond_imp_responses RS responses.induct) 1); by Auto_tac; @@ -183,14 +184,9 @@ \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; by (parts_induct_tac 1); (*RA3*) -by (best_tac (claset() addDs [Key_in_keysFor_parts] - addss (simpset() addsimps [parts_insert_spies])) 2); +by (blast_tac (claset() addSDs [Key_in_keysFor_parts]) 2); (*Fake*) -by (best_tac - (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] - addIs [impOfSubs analz_subset_parts] - addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] - addss (simpset())) 1); +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); qed_spec_mp "new_keys_not_used"; diff -r f102cb0140fe -r 828148415197 src/HOL/Auth/Shared.ML --- a/src/HOL/Auth/Shared.ML Fri Jan 02 13:24:53 1998 +0100 +++ b/src/HOL/Auth/Shared.ML Fri Jan 02 17:15:19 1998 +0100 @@ -28,6 +28,16 @@ qed "keysFor_parts_initState"; Addsimps [keysFor_parts_initState]; +(*Specialized to shared-key model: no need for addss in protocol proofs*) +goal thy "!!X. [| K: keysFor (parts (insert X H)); X : synth (analz H) |] \ +\ ==> K : keysFor (parts H) | Key K : parts H"; +by (fast_tac + (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono), + impOfSubs (analz_subset_parts RS keysFor_mono)] + addIs [impOfSubs analz_subset_parts] + addss (simpset())) 1); +qed "keysFor_parts_insert"; + goal thy "!!H. Crypt K X : H ==> K : keysFor H"; by (dtac Crypt_imp_invKey_keysFor 1); by (Asm_full_simp_tac 1); diff -r f102cb0140fe -r 828148415197 src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Fri Jan 02 13:24:53 1998 +0100 +++ b/src/HOL/Auth/Yahalom.ML Fri Jan 02 17:15:19 1998 +0100 @@ -101,11 +101,7 @@ \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; by (parts_induct_tac 1); (*Fake*) -by (best_tac - (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] - addIs [impOfSubs analz_subset_parts] - addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] - addss (simpset())) 1); +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); (*YM2-4: Because Key K is not fresh, etc.*) by (REPEAT (blast_tac (claset() addSEs spies_partsEs) 1)); qed_spec_mp "new_keys_not_used"; @@ -587,7 +583,7 @@ by (ALLGOALS Asm_simp_tac); (*YM4*) by (Blast_tac 2); -(*YM3*) +(*YM3 [blast_tac is 50% slower] *) by (best_tac (claset() addSDs [B_Said_YM2, Says_imp_spies RS parts.Inj] addSEs [MPair_parts]) 1); val lemma = result() RSN (2, rev_mp) RS mp |> standard; diff -r f102cb0140fe -r 828148415197 src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Fri Jan 02 13:24:53 1998 +0100 +++ b/src/HOL/Auth/Yahalom2.ML Fri Jan 02 17:15:19 1998 +0100 @@ -105,11 +105,7 @@ (*YM3*) by (blast_tac (claset() addss (simpset())) 2); (*Fake*) -by (best_tac - (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] - addIs [impOfSubs analz_subset_parts] - addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] - addss (simpset())) 1); +by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd",