--- 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"