--- 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 \<notin> 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 \<subseteq> 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 \<notin> 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 \<notin> 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 \<notin> 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;
--- 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 \<notin> Key`shrK`bad and cannot be proved by rewriting
@@ -872,9 +859,9 @@
Y \<in> parts(insert X H) and Y \<in> 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
--- 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"
--- 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 \<union> C) = Key ` (insert K KK) \<union> 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 \<in> H; K \<in> symKeys|] ==> K \<in> 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
--- 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.
--- 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 \<notin> 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 \<notin> A"
@@ -241,14 +192,40 @@
(Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> 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 \<notin> 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)"
--- 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"
--- 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"
--- 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 \<notin> 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 \<subseteq> - (range shrK) \<Longrightarrow> shrK x \<notin> A"
@@ -418,18 +363,42 @@
(Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> 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 \<notin> 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) \<in> X) = (Key K \<in> 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 \<subseteq> knows A (e # evs)"