# HG changeset patch # User paulson # Date 988384581 -7200 # Node ID a315a3862bb4e4c0fac6d49a861563ca763b3c78 # Parent 4095353bd0d7fd95f8c4720796dad9c26e4c1eaa better treatment of methods: uses Method.ctxt_args to refer to current simpset and claset. Needed to fix problems with Recur.thy diff -r 4095353bd0d7 -r a315a3862bb4 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Wed Apr 25 10:31:39 2001 +0200 +++ b/src/HOL/Auth/Message.thy Fri Apr 27 17:16:21 2001 +0200 @@ -143,15 +143,23 @@ by (blast dest: Fake_parts_insert [THEN subsetD, dest]) method_setup spy_analz = {* - Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *} + Method.ctxt_args (fn ctxt => + Method.METHOD (fn facts => + gen_spy_analz_tac (Classical.get_local_claset ctxt, + Simplifier.get_local_simpset ctxt) 1)) *} "for proving the Fake case when analz is involved" method_setup atomic_spy_analz = {* - Method.no_args (Method.METHOD (fn facts => atomic_spy_analz_tac 1)) *} + Method.ctxt_args (fn ctxt => + Method.METHOD (fn facts => + atomic_spy_analz_tac (Classical.get_local_claset ctxt, + Simplifier.get_local_simpset ctxt) 1)) *} "for debugging spy_analz" method_setup Fake_insert_simp = {* - Method.no_args (Method.METHOD (fn facts => Fake_insert_simp_tac 1)) *} + Method.ctxt_args (fn ctxt => + Method.METHOD (fn facts => + Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1)) *} "for debugging spy_analz" end diff -r 4095353bd0d7 -r a315a3862bb4 src/HOL/Auth/Message_lemmas.ML --- a/src/HOL/Auth/Message_lemmas.ML Wed Apr 25 10:31:39 2001 +0200 +++ b/src/HOL/Auth/Message_lemmas.ML Fri Apr 27 17:16:21 2001 +0200 @@ -865,8 +865,8 @@ impOfSubs Fake_parts_insert] THEN' eresolve_tac [asm_rl, synth.Inj]; -fun Fake_insert_simp_tac i = - REPEAT (Fake_insert_tac i) THEN Asm_full_simp_tac i; +fun Fake_insert_simp_tac ss i = + REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i; (*Analysis of Fake cases. Also works for messages that forward unknown parts, @@ -874,14 +874,15 @@ Abstraction over i is ESSENTIAL: it delays the dereferencing of claset DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) -val atomic_spy_analz_tac = SELECT_GOAL - (Fake_insert_simp_tac 1 +fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL + (Fake_insert_simp_tac ss 1 THEN IF_UNSOLVED (Blast.depth_tac - (claset() addIs [analz_insertI, + (cs addIs [analz_insertI, impOfSubs analz_subset_parts]) 4 1)); -fun spy_analz_tac i = +(*The explicit claset and simpset arguments help it work with Isar*) +fun gen_spy_analz_tac (cs,ss) i = DETERM (SELECT_GOAL (EVERY @@ -889,9 +890,11 @@ (REPEAT o CHANGED) (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1), (*...allowing further simplifications*) - Simp_tac 1, + simp_tac ss 1, REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), - DEPTH_SOLVE (atomic_spy_analz_tac 1)]) i); + DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i); + +fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i; (*By default only o_apply is built-in. But in the presence of eta-expansion this means that some terms displayed as (f o g) will be rewritten, and others diff -r 4095353bd0d7 -r a315a3862bb4 src/HOL/Auth/Public.thy --- a/src/HOL/Auth/Public.thy Wed Apr 25 10:31:39 2001 +0200 +++ b/src/HOL/Auth/Public.thy Fri Apr 27 17:16:21 2001 +0200 @@ -40,7 +40,9 @@ (*Specialized methods*) method_setup possibility = {* - Method.no_args (Method.METHOD (fn facts => possibility_tac)) *} + Method.ctxt_args (fn ctxt => + Method.METHOD (fn facts => + gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *} "for proving possibility theorems" end diff -r 4095353bd0d7 -r a315a3862bb4 src/HOL/Auth/Public_lemmas.ML --- a/src/HOL/Auth/Public_lemmas.ML Wed Apr 25 10:31:39 2001 +0200 +++ b/src/HOL/Auth/Public_lemmas.ML Fri Apr 27 17:16:21 2001 +0200 @@ -139,14 +139,16 @@ by (Fast_tac 1); qed "Nonce_supply"; -(*Tactic for possibility theorems*) -fun possibility_tac st = st |> +(*Tactic for possibility theorems (Isar interface)*) +fun gen_possibility_tac ss state = state |> REPEAT (*omit used_Says so that Nonces start from different traces!*) - (ALLGOALS (simp_tac (simpset() delsimps [used_Says])) + (ALLGOALS (simp_tac (ss delsimps [used_Says])) THEN REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI, Nonce_supply])); +(*Tactic for possibility theorems (ML script version)*) +fun possibility_tac state = gen_possibility_tac (simpset()) state; (*** Specialized rewriting for the analz_image_... theorems ***) diff -r 4095353bd0d7 -r a315a3862bb4 src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Wed Apr 25 10:31:39 2001 +0200 +++ b/src/HOL/Auth/Recur.thy Fri Apr 27 17:16:21 2001 +0200 @@ -127,38 +127,44 @@ done -(*Case two: Alice, Bob and the server -WHY WON'T INSERT LET VARS REMAIN??? +(*Case two: Alice, Bob and the server*) lemma "\K. \NA. \evs \ recur. Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, END|} \ set evs" -apply (insert Nonce_supply2 Key_supply2) +apply (tactic "cut_facts_tac [Nonce_supply2, Key_supply2] 1") apply clarify apply (intro exI bexI) -apply (rule_tac [2] recur.Nil [THEN recur.RA1, THEN recur.RA2, - THEN recur.RA3 [OF _ _ respond.One]]) -apply possibility -apply (DEPTH_SOLVE (erule asm_rl less_not_refl2 less_not_refl3)) +apply (rule_tac [2] + recur.Nil [THEN recur.RA1, + THEN recur.RA2, + THEN recur.RA3 [OF _ _ respond.One [THEN respond.Cons]], + THEN recur.RA4]) +apply (tactic "basic_possibility_tac") +apply (tactic + "DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)") done -*) (*Case three: Alice, Bob, Charlie and the server - TOO SLOW to run every time! -Goal "\K. \NA. \evs \ recur. + Rather slow (16 seconds) to run every time... +lemma "\K. \NA. \evs \ recur. Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, END|} \ set evs" -by (cut_facts_tac [Nonce_supply3, Key_supply3] 1); -by (REPEAT (eresolve_tac [exE, conjE] 1)); -by (REPEAT (resolve_tac [exI,bexI] 1)); -by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS - (respond.One RS respond.Cons RS respond.Cons RSN - (3,recur.RA3)) RS recur.RA4 RS recur.RA4) 2); -by basic_possibility_tac; -by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 - ORELSE - eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)); -result(); -****) +apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1") +apply clarify +apply (intro exI bexI) +apply (rule_tac [2] + recur.Nil [THEN recur.RA1, + THEN recur.RA2, THEN recur.RA2, + THEN recur.RA3 + [OF _ _ respond.One + [THEN respond.Cons, THEN respond.Cons]], + THEN recur.RA4, THEN recur.RA4]) +apply (tactic "basic_possibility_tac") +apply (tactic + "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 ORELSE \ +\ eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)") +done +*) (**** Inductive proofs about recur ****) @@ -274,7 +280,8 @@ (*Everything that's hashed is already in past traffic. *) -lemma Hash_imp_body: "[| Hash {|Key(shrK A), X|} \ parts (spies evs); +lemma Hash_imp_body: + "[| Hash {|Key(shrK A), X|} \ parts (spies evs); evs \ recur; A \ bad |] ==> X \ parts (spies evs)" apply (erule rev_mp) apply (erule recur.induct, @@ -405,11 +412,6 @@ done -(*WHAT'S GOING ON??*) -method_setup newbla = {* - Method.no_args (Method.METHOD (fn facts => Blast_tac 1)) *} - "for debugging spy_analz" - lemma Spy_not_see_session_key: "[| Crypt (shrK A) {|Key K, Agent A', N|} \ parts (spies evs); A \ bad; A' \ bad; evs \ recur |] @@ -423,12 +425,7 @@ (*Base*) apply force (*Fake*) -apply (intro allI impI notI conjI iffI) -apply Fake_insert_simp -apply (blast ); -(*???ASK MARKUS WHY METHOD_SETUP DOESN'T WORK. Should be just apply spy_analz -*) (*RA2*) apply blast (*RA3 remains*) @@ -496,7 +493,8 @@ apply blast (*RA2: it cannot be a new Nonce, contradiction.*) apply blast -(*RA3*) +(*RA3*) (*Pity that the proof is so brittle: this step requires the rewriting, + which however would break all other steps.*) apply (simp add: parts_insert_spies, blast) (*RA4*) apply blast diff -r 4095353bd0d7 -r a315a3862bb4 src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Wed Apr 25 10:31:39 2001 +0200 +++ b/src/HOL/Auth/Shared.thy Fri Apr 27 17:16:21 2001 +0200 @@ -15,7 +15,7 @@ shrK :: "agent => key" (*symmetric keys*) axioms - isSym_keys: "K \\ symKeys" (*All keys are symmetric*) + isSym_keys: "K \ symKeys" (*All keys are symmetric*) inj_shrK: "inj shrK" (*No two agents have the same long-term key*) primrec @@ -38,7 +38,7 @@ (*Lets blast_tac perform this step without needing the simplifier*) lemma invKey_shrK_iff [iff]: - "(Key (invKey K) \\ X) = (Key K \\ X)" + "(Key (invKey K) \ X) = (Key K \ X)" by auto; (*Specialized methods*) @@ -52,7 +52,9 @@ "for proving the Session Key Compromise theorem" method_setup possibility = {* - Method.no_args (Method.METHOD (fn facts => possibility_tac)) *} + Method.ctxt_args (fn ctxt => + Method.METHOD (fn facts => + gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *} "for proving possibility theorems" end diff -r 4095353bd0d7 -r a315a3862bb4 src/HOL/Auth/Shared_lemmas.ML --- a/src/HOL/Auth/Shared_lemmas.ML Wed Apr 25 10:31:39 2001 +0200 +++ b/src/HOL/Auth/Shared_lemmas.ML Fri Apr 27 17:16:21 2001 +0200 @@ -201,14 +201,17 @@ (*Omitting used_Says makes the tactic much faster: it leaves expressions such as Nonce ?N \\ used evs that match Nonce_supply*) -fun possibility_tac st = st |> +fun gen_possibility_tac ss state = state |> (REPEAT - (ALLGOALS (simp_tac (simpset() delsimps [used_Says, used_Notes, used_Gets] + (ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets] setSolver safe_solver)) THEN REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI, Nonce_supply, Key_supply]))); +(*Tactic for possibility theorems (ML script version)*) +fun possibility_tac state = gen_possibility_tac (simpset()) state; + (*For harder protocols (such as Recur) where we have to set up some nonces and keys initially*) fun basic_possibility_tac st = st |>