# HG changeset patch # User wenzelm # Date 1185992716 -7200 # Node ID fc7f857d33c8c768bcca722a6e10b6d23e40b54f # Parent a93b0f4df8386a85554101be49c19001cca182c2 tuned ML bindings (for multithreading); diff -r a93b0f4df838 -r fc7f857d33c8 src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Wed Aug 01 19:59:12 2007 +0200 +++ b/src/HOL/Auth/Event.thy Wed Aug 01 20:25:16 2007 +0200 @@ -258,18 +258,6 @@ knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD] knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD] -ML -{* -val analz_mono_contra_tac = - let val analz_impI = inst "P" "?Y \ analz (knows Spy ?evs)" impI - in - rtac analz_impI THEN' - REPEAT1 o - (dresolve_tac (thms"analz_mono_contra")) - THEN' mp_tac - end -*} - lemma knows_subset_knows_Cons: "knows A evs \ knows A (e # evs)" by (induct e, auto simp: knows_Cons) @@ -289,6 +277,19 @@ analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD] intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD]) + +ML +{* +val analz_mono_contra_tac = + let val analz_impI = inst "P" "?Y \ analz (knows Spy ?evs)" impI + in + rtac analz_impI THEN' + REPEAT1 o + (dresolve_tac @{thms analz_mono_contra}) + THEN' mp_tac + end +*} + method_setup analz_mono_contra = {* Method.no_args (Method.SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac)) *} "for proving theorems of the form X \ analz (knows Spy evs) --> P" @@ -297,51 +298,15 @@ ML {* -val knows_Cons = thm "knows_Cons" -val used_Nil = thm "used_Nil" -val used_Cons = thm "used_Cons" - -val Notes_imp_used = thm "Notes_imp_used"; -val Says_imp_used = thm "Says_imp_used"; -val Says_imp_knows_Spy = thm "Says_imp_knows_Spy"; -val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy"; -val knows_Spy_partsEs = thms "knows_Spy_partsEs"; -val spies_partsEs = thms "spies_partsEs"; -val Says_imp_spies = thm "Says_imp_spies"; -val parts_insert_spies = thm "parts_insert_spies"; -val Says_imp_knows = thm "Says_imp_knows"; -val Notes_imp_knows = thm "Notes_imp_knows"; -val Gets_imp_knows_agents = thm "Gets_imp_knows_agents"; -val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState"; -val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState"; -val usedI = thm "usedI"; -val initState_into_used = thm "initState_into_used"; -val used_Says = thm "used_Says"; -val used_Notes = thm "used_Notes"; -val used_Gets = thm "used_Gets"; -val used_nil_subset = thm "used_nil_subset"; -val analz_mono_contra = thms "analz_mono_contra"; -val knows_subset_knows_Cons = thm "knows_subset_knows_Cons"; -val initState_subset_knows = thm "initState_subset_knows"; -val keysFor_parts_insert = thm "keysFor_parts_insert"; - - -val synth_analz_mono = thm "synth_analz_mono"; - -val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says"; -val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes"; -val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets"; - - val synth_analz_mono_contra_tac = let val syan_impI = inst "P" "?Y \ synth (analz (knows Spy ?evs))" impI in rtac syan_impI THEN' REPEAT1 o (dresolve_tac - [knows_Spy_subset_knows_Spy_Says RS synth_analz_mono RS contra_subsetD, - knows_Spy_subset_knows_Spy_Notes RS synth_analz_mono RS contra_subsetD, - knows_Spy_subset_knows_Spy_Gets RS synth_analz_mono RS contra_subsetD]) + [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}, + @{thm knows_Spy_subset_knows_Spy_Notes} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}, + @{thm knows_Spy_subset_knows_Spy_Gets} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}]) THEN' mp_tac end; diff -r a93b0f4df838 -r fc7f857d33c8 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Wed Aug 01 19:59:12 2007 +0200 +++ b/src/HOL/Auth/Message.thy Wed Aug 01 20:25:16 2007 +0200 @@ -840,21 +840,8 @@ subsection{*Tactics useful for many protocol proofs*} ML {* -val invKey = thm "invKey" -val keysFor_def = thm "keysFor_def" -val HPair_def = thm "HPair_def" -val symKeys_def = thm "symKeys_def" -val parts_mono = thm "parts_mono"; -val analz_mono = thm "analz_mono"; -val synth_mono = thm "synth_mono"; -val analz_increasing = thm "analz_increasing"; - -val analz_insertI = thm "analz_insertI"; -val analz_subset_parts = thm "analz_subset_parts"; -val Fake_parts_insert = thm "Fake_parts_insert"; -val Fake_analz_insert = thm "Fake_analz_insert"; -val pushes = thms "pushes"; - +structure Message = +struct (*Prove base case (subgoal i) and simplify others. A typical base case concerns Crypt K X \ Key`shrK`bad and cannot be proved by rewriting @@ -872,9 +859,9 @@ Y \ parts(insert X H) and Y \ analz(insert X H) *) val Fake_insert_tac = - dresolve_tac [impOfSubs Fake_analz_insert, - impOfSubs Fake_parts_insert] THEN' - eresolve_tac [asm_rl, thm"synth.Inj"]; + dresolve_tac [impOfSubs @{thm Fake_analz_insert}, + impOfSubs @{thm Fake_parts_insert}] THEN' + eresolve_tac [asm_rl, @{thm synth.Inj}]; fun Fake_insert_simp_tac ss i = REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i; @@ -883,8 +870,8 @@ (Fake_insert_simp_tac ss 1 THEN IF_UNSOLVED (Blast.depth_tac - (cs addIs [analz_insertI, - impOfSubs analz_subset_parts]) 4 1)) + (cs addIs [@{thm analz_insertI}, + impOfSubs @{thm analz_subset_parts}]) 4 1)) (*The explicit claset and simpset arguments help it work with Isar*) fun gen_spy_analz_tac (cs,ss) i = @@ -900,6 +887,8 @@ DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i) fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i + +end *} text{*By default only @{text o_apply} is built-in. But in the presence of @@ -951,18 +940,17 @@ method_setup spy_analz = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} + Method.SIMPLE_METHOD (Message.gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} "for proving the Fake case when analz is involved" method_setup atomic_spy_analz = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} + Method.SIMPLE_METHOD (Message.atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *} "for debugging spy_analz" method_setup Fake_insert_simp = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *} + Method.SIMPLE_METHOD (Message.Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *} "for debugging spy_analz" - end diff -r a93b0f4df838 -r fc7f857d33c8 src/HOL/Auth/OtwayReesBella.thy --- a/src/HOL/Auth/OtwayReesBella.thy Wed Aug 01 19:59:12 2007 +0200 +++ b/src/HOL/Auth/OtwayReesBella.thy Wed Aug 01 20:25:16 2007 +0200 @@ -130,14 +130,10 @@ ML {* -val Oops_parts_knows_Spy = thm "Oops_parts_knows_Spy" -val OR4_parts_knows_Spy = thm "OR4_parts_knows_Spy" -val OR2_parts_knows_Spy = thm "OR2_parts_knows_Spy" - fun parts_explicit_tac i = - forward_tac [Oops_parts_knows_Spy] (i+7) THEN - forward_tac [OR4_parts_knows_Spy] (i+6) THEN - forward_tac [OR2_parts_knows_Spy] (i+4) + forward_tac [@{thm Oops_parts_knows_Spy}] (i+7) THEN + forward_tac [@{thm OR4_parts_knows_Spy}] (i+6) THEN + forward_tac [@{thm OR2_parts_knows_Spy}] (i+4) *} method_setup parts_explicit = {* @@ -249,21 +245,24 @@ ML {* -val analz_image_freshCryptK_lemma = thm "analz_image_freshCryptK_lemma"; -val analz_image_freshK_simps = thms "analz_image_freshK_simps"; +structure OtwayReesBella = +struct val analz_image_freshK_ss = - simpset() delsimps [image_insert, image_Un] - delsimps [imp_disjL] (*reduces blow-up*) - addsimps thms "analz_image_freshK_simps" + @{simpset} delsimps [image_insert, image_Un] + delsimps [@{thm imp_disjL}] (*reduces blow-up*) + addsimps @{thms analz_image_freshK_simps} + +end *} method_setup analz_freshCryptK = {* Method.ctxt_args (fn ctxt => (Method.SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), - REPEAT_FIRST (rtac analz_image_freshCryptK_lemma), - ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *} + REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}), + ALLGOALS (asm_simp_tac + (Simplifier.context ctxt OtwayReesBella.analz_image_freshK_ss))]))) *} "for proving useful rewrite rule" diff -r a93b0f4df838 -r fc7f857d33c8 src/HOL/Auth/Public.thy --- a/src/HOL/Auth/Public.thy Wed Aug 01 19:59:12 2007 +0200 +++ b/src/HOL/Auth/Public.thy Wed Aug 01 20:25:16 2007 +0200 @@ -377,13 +377,6 @@ lemma insert_Key_image: "insert (Key K) (Key`KK \ C) = Key ` (insert K KK) \ C" by blast -ML -{* -val Key_not_used = thm "Key_not_used"; -val insert_Key_singleton = thm "insert_Key_singleton"; -val insert_Key_image = thm "insert_Key_image"; -*} - lemma Crypt_imp_keysFor :"[|Crypt K X \ H; K \ symKeys|] ==> K \ keysFor H" by (drule Crypt_imp_invKey_keysFor, simp) @@ -404,31 +397,17 @@ Key_not_used insert_Key_image Un_assoc [THEN sym] ML {* -val analz_image_freshK_lemma = thm "analz_image_freshK_lemma"; -val analz_image_freshK_simps = thms "analz_image_freshK_simps"; -val imp_disjL = thm "imp_disjL"; - -val analz_image_freshK_ss = simpset() delsimps [image_insert, image_Un] - delsimps [imp_disjL] (*reduces blow-up*) - addsimps thms "analz_image_freshK_simps" -*} +structure Public = +struct -method_setup analz_freshK = {* - Method.ctxt_args (fn ctxt => - (Method.SIMPLE_METHOD - (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), - REPEAT_FIRST (rtac analz_image_freshK_lemma), - ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *} - "for proving the Session Key Compromise theorem" +val analz_image_freshK_ss = @{simpset} delsimps [image_insert, image_Un] + delsimps [@{thm imp_disjL}] (*reduces blow-up*) + addsimps @{thms analz_image_freshK_simps} -subsection{*Specialized Methods for Possibility Theorems*} - -ML -{* (*Tactic for possibility theorems*) fun possibility_tac ctxt = REPEAT (*omit used_Says so that Nonces start from different traces!*) - (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says])) + (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [@{thm used_Says}])) THEN REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI, @{thm Nonce_supply}])) @@ -440,16 +419,29 @@ (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver)) THEN REPEAT_FIRST (resolve_tac [refl, conjI])) + +end *} +method_setup analz_freshK = {* + Method.ctxt_args (fn ctxt => + (Method.SIMPLE_METHOD + (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), + REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), + ALLGOALS (asm_simp_tac (Simplifier.context ctxt Public.analz_image_freshK_ss))]))) *} + "for proving the Session Key Compromise theorem" + + +subsection{*Specialized Methods for Possibility Theorems*} + method_setup possibility = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (possibility_tac ctxt)) *} + Method.SIMPLE_METHOD (Public.possibility_tac ctxt)) *} "for proving possibility theorems" method_setup basic_possibility = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (basic_possibility_tac ctxt)) *} + Method.SIMPLE_METHOD (Public.basic_possibility_tac ctxt)) *} "for proving possibility theorems" end diff -r a93b0f4df838 -r fc7f857d33c8 src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Wed Aug 01 19:59:12 2007 +0200 +++ b/src/HOL/Auth/Recur.thy Wed Aug 01 20:25:16 2007 +0200 @@ -95,7 +95,7 @@ (*No "oops" message can easily be expressed. Each session key is associated--in two separate messages--with two nonces. This is one try, but it isn't that useful. Re domino attack, note that - Recur.ML proves that each session key is secure provided the two + Recur.thy proves that each session key is secure provided the two peers are, even if there are compromised agents elsewhere in the chain. Oops cases proved using parts_cut, Key_in_keysFor_parts, etc. diff -r a93b0f4df838 -r fc7f857d33c8 src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Wed Aug 01 19:59:12 2007 +0200 +++ b/src/HOL/Auth/Shared.thy Wed Aug 01 20:25:16 2007 +0200 @@ -163,55 +163,6 @@ possibility theorems must assume the existence of a few keys.*} -subsection{*Tactics for possibility theorems*} - -ML -{* -val inj_shrK = thm "inj_shrK"; -val isSym_keys = thm "isSym_keys"; -val Nonce_supply = thm "Nonce_supply"; -val invKey_K = thm "invKey_K"; -val analz_Decrypt' = thm "analz_Decrypt'"; -val keysFor_parts_initState = thm "keysFor_parts_initState"; -val keysFor_parts_insert = thm "keysFor_parts_insert"; -val Crypt_imp_keysFor = thm "Crypt_imp_keysFor"; -val Spy_knows_Spy_bad = thm "Spy_knows_Spy_bad"; -val Crypt_Spy_analz_bad = thm "Crypt_Spy_analz_bad"; -val shrK_in_initState = thm "shrK_in_initState"; -val shrK_in_used = thm "shrK_in_used"; -val Key_not_used = thm "Key_not_used"; -val shrK_neq = thm "shrK_neq"; -val Nonce_notin_initState = thm "Nonce_notin_initState"; -val Nonce_notin_used_empty = thm "Nonce_notin_used_empty"; -val Nonce_supply_lemma = thm "Nonce_supply_lemma"; -val Nonce_supply1 = thm "Nonce_supply1"; -val Nonce_supply2 = thm "Nonce_supply2"; -val Nonce_supply3 = thm "Nonce_supply3"; -val Nonce_supply = thm "Nonce_supply"; -*} - - -ML -{* -(*Omitting used_Says makes the tactic much faster: it leaves expressions - such as Nonce ?N \ used evs that match Nonce_supply*) -fun possibility_tac ctxt = - (REPEAT - (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says, used_Notes, used_Gets] - setSolver safe_solver)) - THEN - REPEAT_FIRST (eq_assume_tac ORELSE' - resolve_tac [refl, conjI, Nonce_supply]))) - -(*For harder protocols (such as Recur) where we have to set up some - nonces and keys initially*) -fun basic_possibility_tac ctxt = - REPEAT - (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver)) - THEN - REPEAT_FIRST (resolve_tac [refl, conjI])) -*} - subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*} lemma subset_Compl_range: "A <= - (range shrK) ==> shrK x \ A" @@ -241,14 +192,40 @@ (Key K \ analz (Key`nE \ H)) = (K \ nE | Key K \ analz H)" by (blast intro: analz_mono [THEN [2] rev_subsetD]) + +subsection{*Tactics for possibility theorems*} + ML {* -val analz_image_freshK_lemma = thm "analz_image_freshK_lemma"; +structure Shared = +struct + +(*Omitting used_Says makes the tactic much faster: it leaves expressions + such as Nonce ?N \ used evs that match Nonce_supply*) +fun possibility_tac ctxt = + (REPEAT + (ALLGOALS (simp_tac (local_simpset_of ctxt + delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets}] + setSolver safe_solver)) + THEN + REPEAT_FIRST (eq_assume_tac ORELSE' + resolve_tac [refl, conjI, @{thm Nonce_supply}]))) -val analz_image_freshK_ss = - simpset() delsimps [image_insert, image_Un] - delsimps [imp_disjL] (*reduces blow-up*) - addsimps thms "analz_image_freshK_simps" +(*For harder protocols (such as Recur) where we have to set up some + nonces and keys initially*) +fun basic_possibility_tac ctxt = + REPEAT + (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver)) + THEN + REPEAT_FIRST (resolve_tac [refl, conjI])) + + +val analz_image_freshK_ss = + @{simpset} delsimps [image_insert, image_Un] + delsimps [@{thm imp_disjL}] (*reduces blow-up*) + addsimps @{thms analz_image_freshK_simps} + +end *} @@ -264,18 +241,18 @@ Method.ctxt_args (fn ctxt => (Method.SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), - REPEAT_FIRST (rtac analz_image_freshK_lemma), - ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *} + REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), + ALLGOALS (asm_simp_tac (Simplifier.context ctxt Shared.analz_image_freshK_ss))]))) *} "for proving the Session Key Compromise theorem" method_setup possibility = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (possibility_tac ctxt)) *} + Method.SIMPLE_METHOD (Shared.possibility_tac ctxt)) *} "for proving possibility theorems" method_setup basic_possibility = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (basic_possibility_tac ctxt)) *} + Method.SIMPLE_METHOD (Shared.basic_possibility_tac ctxt)) *} "for proving possibility theorems" lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)" diff -r a93b0f4df838 -r fc7f857d33c8 src/HOL/Auth/Smartcard/ShoupRubin.thy --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Wed Aug 01 19:59:12 2007 +0200 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Wed Aug 01 20:25:16 2007 +0200 @@ -272,7 +272,7 @@ -(*Begin lemmas on secure means, from Event.ML, proved for shouprubin. They help +(*Begin lemmas on secure means, from Event.thy, proved for shouprubin. They help the simplifier, especially in analz_image_freshK*) @@ -741,47 +741,43 @@ ML {* -val Outpts_B_Card_form_7 = thm "Outpts_B_Card_form_7" -val Outpts_A_Card_form_4 = thm "Outpts_A_Card_form_4" -val Outpts_A_Card_form_10 = thm "Outpts_A_Card_form_10" -val Gets_imp_knows_Spy = thm "Gets_imp_knows_Spy" -val Outpts_B_Card_form_7 = thm "Outpts_B_Card_form_7" -val Gets_imp_knows_Spy_parts_Snd = thm "Gets_imp_knows_Spy_parts_Snd" -val Gets_imp_knows_Spy_analz_Snd = thm "Gets_imp_knows_Spy_analz_Snd" +structure ShoupRubin = +struct val prepare_tac = - (*SR8*) forward_tac [Outpts_B_Card_form_7] 14 THEN + (*SR8*) forward_tac [@{thm Outpts_B_Card_form_7}] 14 THEN eresolve_tac [exE] 15 THEN eresolve_tac [exE] 15 THEN - (*SR9*) forward_tac [Outpts_A_Card_form_4] 16 THEN - (*SR11*) forward_tac [Outpts_A_Card_form_10] 21 THEN + (*SR9*) forward_tac [@{thm Outpts_A_Card_form_4}] 16 THEN + (*SR11*) forward_tac [@{thm Outpts_A_Card_form_10}] 21 THEN eresolve_tac [exE] 22 THEN eresolve_tac [exE] 22 fun parts_prepare_tac ctxt = prepare_tac THEN - (*SR9*) dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 18 THEN - (*SR9*) dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 19 THEN - (*Oops1*) dresolve_tac [Outpts_B_Card_form_7] 25 THEN - (*Oops2*) dresolve_tac [Outpts_A_Card_form_10] 27 THEN + (*SR9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 18 THEN + (*SR9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN + (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25 THEN + (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN (*Base*) (force_tac (local_clasimpset_of ctxt)) 1 val analz_prepare_tac = prepare_tac THEN - dtac (Gets_imp_knows_Spy_analz_Snd) 18 THEN - (*SR9*) dtac (Gets_imp_knows_Spy_analz_Snd) 19 THEN + dtac @{thm Gets_imp_knows_Spy_analz_Snd} 18 THEN + (*SR9*) dtac @{thm Gets_imp_knows_Spy_analz_Snd} 19 THEN REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac) +end *} method_setup prepare = {* - Method.no_args (Method.SIMPLE_METHOD prepare_tac) *} + Method.no_args (Method.SIMPLE_METHOD ShoupRubin.prepare_tac) *} "to launch a few simple facts that'll help the simplifier" method_setup parts_prepare = {* - Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (parts_prepare_tac ctxt)) *} + Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubin.parts_prepare_tac ctxt)) *} "additional facts to reason about parts" method_setup analz_prepare = {* - Method.no_args (Method.SIMPLE_METHOD analz_prepare_tac) *} + Method.no_args (Method.SIMPLE_METHOD ShoupRubin.analz_prepare_tac) *} "additional facts to reason about analz" @@ -825,24 +821,17 @@ apply auto done -ML -{* -val knows_Spy_Inputs_secureM_sr_Spy = thm "knows_Spy_Inputs_secureM_sr_Spy" -val knows_Spy_Outpts_secureM_sr_Spy = thm "knows_Spy_Outpts_secureM_sr_Spy" -val shouprubin_assumes_securemeans = thm "shouprubin_assumes_securemeans" -val analz_image_Key_Un_Nonce= thm "analz_image_Key_Un_Nonce" -*} - method_setup sc_analz_freshK = {* Method.ctxt_args (fn ctxt => (Method.SIMPLE_METHOD - (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), - REPEAT_FIRST (rtac analz_image_freshK_lemma), - ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss - addsimps [knows_Spy_Inputs_secureM_sr_Spy, - knows_Spy_Outpts_secureM_sr_Spy, - shouprubin_assumes_securemeans, - analz_image_Key_Un_Nonce]))]))) *} + (EVERY [REPEAT_FIRST + (resolve_tac [allI, ballI, impI]), + REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), + ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss + addsimps [@{thm knows_Spy_Inputs_secureM_sr_Spy}, + @{thm knows_Spy_Outpts_secureM_sr_Spy}, + @{thm shouprubin_assumes_securemeans}, + @{thm analz_image_Key_Un_Nonce}]))]))) *} "for proving the Session Key Compromise theorem for smartcard protocols" diff -r a93b0f4df838 -r fc7f857d33c8 src/HOL/Auth/Smartcard/ShoupRubinBella.thy --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Wed Aug 01 19:59:12 2007 +0200 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Wed Aug 01 20:25:16 2007 +0200 @@ -277,7 +277,7 @@ -(*Begin lemmas on secure means, from Event.ML, proved for shouprubin. They help +(*Begin lemmas on secure means, from Event.thy, proved for shouprubin. They help the simplifier, especially in analz_image_freshK*) @@ -750,46 +750,42 @@ ML {* -val Outpts_B_Card_form_7 = thm "Outpts_B_Card_form_7" -val Outpts_A_Card_form_4 = thm "Outpts_A_Card_form_4" -val Outpts_A_Card_form_10 = thm "Outpts_A_Card_form_10" -val Gets_imp_knows_Spy = thm "Gets_imp_knows_Spy" -val Outpts_B_Card_form_7 = thm "Outpts_B_Card_form_7" -val Gets_imp_knows_Spy_parts_Snd = thm "Gets_imp_knows_Spy_parts_Snd" -val Gets_imp_knows_Spy_analz_Snd = thm "Gets_imp_knows_Spy_analz_Snd" +structure ShoupRubinBella = +struct fun prepare_tac ctxt = - (*SR_U8*) forward_tac [Outpts_B_Card_form_7] 14 THEN + (*SR_U8*) forward_tac [@{thm Outpts_B_Card_form_7}] 14 THEN (*SR_U8*) clarify_tac (local_claset_of ctxt) 15 THEN - (*SR_U9*) forward_tac [Outpts_A_Card_form_4] 16 THEN - (*SR_U11*) forward_tac [Outpts_A_Card_form_10] 21 + (*SR_U9*) forward_tac [@{thm Outpts_A_Card_form_4}] 16 THEN + (*SR_U11*) forward_tac [@{thm Outpts_A_Card_form_10}] 21 fun parts_prepare_tac ctxt = prepare_tac ctxt THEN - (*SR_U9*) dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 18 THEN - (*SR_U9*) dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 19 THEN - (*Oops1*) dresolve_tac [Outpts_B_Card_form_7] 25 THEN - (*Oops2*) dresolve_tac [Outpts_A_Card_form_10] 27 THEN + (*SR_U9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 18 THEN + (*SR_U9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN + (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25 THEN + (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN (*Base*) (force_tac (local_clasimpset_of ctxt)) 1 fun analz_prepare_tac ctxt = prepare_tac ctxt THEN - dtac (Gets_imp_knows_Spy_analz_Snd) 18 THEN - (*SR_U9*) dtac (Gets_imp_knows_Spy_analz_Snd) 19 THEN + dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 18 THEN + (*SR_U9*) dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 19 THEN REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac) +end *} method_setup prepare = {* - Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (prepare_tac ctxt)) *} + Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *} "to launch a few simple facts that'll help the simplifier" method_setup parts_prepare = {* - Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (parts_prepare_tac ctxt)) *} + Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *} "additional facts to reason about parts" method_setup analz_prepare = {* - Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (analz_prepare_tac ctxt)) *} + Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *} "additional facts to reason about analz" @@ -834,24 +830,16 @@ apply auto done -ML -{* -val knows_Spy_Inputs_secureM_srb_Spy = thm "knows_Spy_Inputs_secureM_srb_Spy" -val knows_Spy_Outpts_secureM_srb_Spy = thm "knows_Spy_Outpts_secureM_srb_Spy" -val shouprubin_assumes_securemeans = thm "shouprubin_assumes_securemeans" -val analz_image_Key_Un_Nonce= thm "analz_image_Key_Un_Nonce" -*} - method_setup sc_analz_freshK = {* Method.ctxt_args (fn ctxt => (Method.SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), - REPEAT_FIRST (rtac analz_image_freshK_lemma), - ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss - addsimps [knows_Spy_Inputs_secureM_srb_Spy, - knows_Spy_Outpts_secureM_srb_Spy, - shouprubin_assumes_securemeans, - analz_image_Key_Un_Nonce]))]))) *} + REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), + ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss + addsimps [@{thm knows_Spy_Inputs_secureM_srb_Spy}, + @{thm knows_Spy_Outpts_secureM_srb_Spy}, + @{thm shouprubin_assumes_securemeans}, + @{thm analz_image_Key_Un_Nonce}]))]))) *} "for proving the Session Key Compromise theorem for smartcard protocols" diff -r a93b0f4df838 -r fc7f857d33c8 src/HOL/Auth/Smartcard/Smartcard.thy --- a/src/HOL/Auth/Smartcard/Smartcard.thy Wed Aug 01 19:59:12 2007 +0200 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy Wed Aug 01 20:25:16 2007 +0200 @@ -322,61 +322,6 @@ possibility theorems must assume the existence of a few keys.*} -subsection{*Tactics for possibility theorems*} - -ML -{* -val inj_shrK = thm "inj_shrK"; -val isSym_keys = thm "isSym_keys"; -val Nonce_supply = thm "Nonce_supply"; -val invKey_K = thm "invKey_K"; -val analz_Decrypt' = thm "analz_Decrypt'"; -val keysFor_parts_initState = thm "keysFor_parts_initState"; -val keysFor_parts_insert = thm "keysFor_parts_insert"; -val Crypt_imp_keysFor = thm "Crypt_imp_keysFor"; -val Spy_knows_Spy_bad = thm "Spy_knows_Spy_bad"; -val Crypt_Spy_analz_bad = thm "Crypt_Spy_analz_bad"; -val shrK_in_initState = thm "shrK_in_initState"; -val shrK_in_used = thm "shrK_in_used"; -val Key_not_used = thm "Key_not_used"; -val shrK_neq = thm "shrK_neq"; -val Nonce_notin_initState = thm "Nonce_notin_initState"; -val Nonce_supply1 = thm "Nonce_supply1"; -val Nonce_supply2 = thm "Nonce_supply2"; -val Nonce_supply3 = thm "Nonce_supply3"; -val Nonce_supply = thm "Nonce_supply"; -val used_Says = thm "used_Says"; -val used_Gets = thm "used_Gets"; -val used_Notes = thm "used_Notes"; -val used_Inputs = thm "used_Inputs"; -val used_C_Gets = thm "used_C_Gets"; -val used_Outpts = thm "used_Outpts"; -val used_A_Gets = thm "used_A_Gets"; -*} - - -ML -{* -(*Omitting used_Says makes the tactic much faster: it leaves expressions - such as Nonce ?N \ used evs that match Nonce_supply*) -fun possibility_tac ctxt = - (REPEAT - (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says, used_Notes, used_Gets, - used_Inputs, used_C_Gets, used_Outpts, used_A_Gets] - setSolver safe_solver)) - THEN - REPEAT_FIRST (eq_assume_tac ORELSE' - resolve_tac [refl, conjI, Nonce_supply]))) - -(*For harder protocols (such as Recur) where we have to set up some - nonces and keys initially*) -fun basic_possibility_tac ctxt = - REPEAT - (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver)) - THEN - REPEAT_FIRST (resolve_tac [refl, conjI])) -*} - subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*} lemma subset_Compl_range_shrK: "A \ - (range shrK) \ shrK x \ A" @@ -418,18 +363,42 @@ (Key K \ analz (Key`nE \ H)) = (K \ nE | Key K \ analz H)" by (blast intro: analz_mono [THEN [2] rev_subsetD]) + +subsection{*Tactics for possibility theorems*} + ML {* -val analz_image_freshK_lemma = thm "analz_image_freshK_lemma"; +structure Smartcard = +struct + +(*Omitting used_Says makes the tactic much faster: it leaves expressions + such as Nonce ?N \ used evs that match Nonce_supply*) +fun possibility_tac ctxt = + (REPEAT + (ALLGOALS (simp_tac (local_simpset_of ctxt + delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets}, + @{thm used_Inputs}, @{thm used_C_Gets}, @{thm used_Outpts}, @{thm used_A_Gets}] + setSolver safe_solver)) + THEN + REPEAT_FIRST (eq_assume_tac ORELSE' + resolve_tac [refl, conjI, @{thm Nonce_supply}]))) + +(*For harder protocols (such as Recur) where we have to set up some + nonces and keys initially*) +fun basic_possibility_tac ctxt = + REPEAT + (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver)) + THEN + REPEAT_FIRST (resolve_tac [refl, conjI])) val analz_image_freshK_ss = @{simpset} delsimps [image_insert, image_Un] delsimps [@{thm imp_disjL}] (*reduces blow-up*) - addsimps thms "analz_image_freshK_simps" + addsimps @{thms analz_image_freshK_simps} +end *} - (*Lets blast_tac perform this step without needing the simplifier*) lemma invKey_shrK_iff [iff]: "(Key (invKey K) \ X) = (Key K \ X)" @@ -441,18 +410,18 @@ Method.ctxt_args (fn ctxt => (Method.SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), - REPEAT_FIRST (rtac analz_image_freshK_lemma), - ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *} + REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), + ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss))]))) *} "for proving the Session Key Compromise theorem" method_setup possibility = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (possibility_tac ctxt)) *} + Method.SIMPLE_METHOD (Smartcard.possibility_tac ctxt)) *} "for proving possibility theorems" method_setup basic_possibility = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD (basic_possibility_tac ctxt)) *} + Method.SIMPLE_METHOD (Smartcard.basic_possibility_tac ctxt)) *} "for proving possibility theorems" lemma knows_subset_knows_Cons: "knows A evs \ knows A (e # evs)"