--- a/src/HOL/SET-Protocol/Cardholder_Registration.thy Wed Aug 01 20:25:16 2007 +0200
+++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy Wed Aug 01 21:10:36 2007 +0200
@@ -263,7 +263,7 @@
THEN set_cr.SET_CR5 [of concl: C i KC3 NC3 KC2 CardSecret],
THEN Says_to_Gets,
THEN set_cr.SET_CR6 [of concl: i C KC2]])
-apply (tactic "basic_possibility_tac")
+apply (tactic "PublicSET.basic_possibility_tac")
apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq)
done
@@ -540,15 +540,12 @@
P --> (Key K \<in> analz (Key`KK Un H)) = (K \<in> KK | Key K \<in> analz H)"
by (blast intro: analz_mono [THEN [2] rev_subsetD])
-ML
-{*
-val Gets_certificate_valid = thm "Gets_certificate_valid";
-
-fun valid_certificate_tac i =
- EVERY [ftac Gets_certificate_valid i,
+method_setup valid_certificate_tac = {*
+ Method.goal_args (Scan.succeed ()) (fn () => fn i =>
+ EVERY [ftac @{thm Gets_certificate_valid} i,
assume_tac i,
- etac conjE i, REPEAT (hyp_subst_tac i)];
-*}
+ etac conjE i, REPEAT (hyp_subst_tac i)])
+*} ""
text{*The @{text "(no_asm)"} attribute is essential, since it retains
the quantifier and allows the simprule's condition to itself be simplified.*}
@@ -560,8 +557,8 @@
apply (erule set_cr.induct)
apply (rule_tac [!] allI) +
apply (rule_tac [!] impI [THEN Key_analz_image_Key_lemma, THEN impI])+
-apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
-apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
+apply (valid_certificate_tac [8]) --{*for message 5*}
+apply (valid_certificate_tac [6]) --{*for message 5*}
apply (erule_tac [9] msg6_KeyCryptKey_disj [THEN disjE])
apply (simp_all
del: image_insert image_Un imp_disjL
@@ -570,7 +567,7 @@
K_fresh_not_KeyCryptKey
DK_fresh_not_KeyCryptKey ball_conj_distrib
analz_image_priEK disj_simps)
- --{*46 seconds on a 1.8GHz machine*}
+ --{*9 seconds on a 1.6GHz machine*}
apply spy_analz
apply blast --{*3*}
apply blast --{*5*}
@@ -596,7 +593,7 @@
K_fresh_not_KeyCryptKey
DK_fresh_not_KeyCryptKey
analz_image_priEK)
- --{*13 seconds on a 1.8GHz machine*}
+ --{*2.5 seconds on a 1.6GHz machine*}
apply spy_analz --{*Fake*}
apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)
done
@@ -739,7 +736,7 @@
N_fresh_not_KeyCryptNonce
DK_fresh_not_KeyCryptNonce K_fresh_not_KeyCryptKey
ball_conj_distrib analz_image_priEK)
- --{*71 seconds on a 1.8GHz machine*}
+ --{*14 seconds on a 1.6GHz machine*}
apply spy_analz --{*Fake*}
apply blast --{*3*}
apply blast --{*5*}
@@ -779,11 +776,11 @@
Cardholder k \<notin> bad & CA i \<notin> bad)"
apply (erule_tac P = "U \<in> ?H" in rev_mp)
apply (erule set_cr.induct)
-apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
+apply (valid_certificate_tac [8]) --{*for message 5*}
apply (simp_all del: image_insert image_Un imp_disjL
add: analz_image_keys_simps analz_knows_absorb
analz_knows_absorb2 notin_image_iff)
- --{*19 seconds on a 1.8GHz machine*}
+ --{*4 seconds on a 1.6GHz machine*}
apply (simp_all (no_asm_simp)) --{*leaves 4 subgoals*}
apply (blast intro!: analz_insertI)+
done
@@ -804,8 +801,8 @@
\<in> parts (knows Spy evs) -->
Nonce CardSecret \<notin> analz (knows Spy evs)"
apply (erule set_cr.induct, analz_mono_contra)
-apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
-apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
+apply (valid_certificate_tac [8]) --{*for message 5*}
+apply (valid_certificate_tac [6]) --{*for message 5*}
apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
apply (simp_all
del: image_insert image_Un imp_disjL
@@ -815,7 +812,7 @@
N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
ball_conj_distrib Nonce_compromise symKey_compromise
analz_image_priEK)
- --{*12 seconds on a 1.8GHz machine*}
+ --{*2.5 seconds on a 1.6GHz machine*}
apply spy_analz --{*Fake*}
apply (simp_all (no_asm_simp))
apply blast --{*1*}
@@ -870,8 +867,8 @@
\<in> parts (knows Spy evs) -->
Nonce NonceCCA \<notin> analz (knows Spy evs)"
apply (erule set_cr.induct, analz_mono_contra)
-apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
-apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
+apply (valid_certificate_tac [8]) --{*for message 5*}
+apply (valid_certificate_tac [6]) --{*for message 5*}
apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
apply (simp_all
del: image_insert image_Un imp_disjL
@@ -881,7 +878,7 @@
N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
ball_conj_distrib Nonce_compromise symKey_compromise
analz_image_priEK)
- --{*15 seconds on a 1.8GHz machine*}
+ --{*3 seconds on a 1.6GHz machine*}
apply spy_analz --{*Fake*}
apply blast --{*1*}
apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) --{*2*}
@@ -941,14 +938,14 @@
apply (erule set_cr.induct)
apply (rule_tac [!] allI impI)+
apply (rule_tac [!] analz_image_pan_lemma)
-apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
-apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
+apply (valid_certificate_tac [8]) --{*for message 5*}
+apply (valid_certificate_tac [6]) --{*for message 5*}
apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
apply (simp_all
del: image_insert image_Un
add: analz_image_keys_simps disjoint_image_iff
notin_image_iff analz_image_priEK)
- --{*33 seconds on a 1.8GHz machine*}
+ --{*6 seconds on a 1.6GHz machine*}
apply spy_analz
apply (simp add: insert_absorb) --{*6*}
done
@@ -972,14 +969,14 @@
& (CA i) \<in> bad"
apply (erule rev_mp)
apply (erule set_cr.induct)
-apply (tactic{*valid_certificate_tac 8*}) --{*for message 5*}
-apply (tactic{*valid_certificate_tac 6*}) --{*for message 5*}
+apply (valid_certificate_tac [8]) --{*for message 5*}
+apply (valid_certificate_tac [6]) --{*for message 5*}
apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
apply (simp_all
del: image_insert image_Un
add: analz_image_keys_simps analz_insert_pan analz_image_pan
notin_image_iff analz_image_priEK)
- --{*18 seconds on a 1.8GHz machine*}
+ --{*3.5 seconds on a 1.6GHz machine*}
apply spy_analz --{*fake*}
apply blast --{*3*}
apply blast --{*5*}
--- a/src/HOL/SET-Protocol/EventSET.thy Wed Aug 01 20:25:16 2007 +0200
+++ b/src/HOL/SET-Protocol/EventSET.thy Wed Aug 01 21:10:36 2007 +0200
@@ -182,7 +182,7 @@
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'
+ REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) THEN'
mp_tac
end
*}
--- a/src/HOL/SET-Protocol/Merchant_Registration.thy Wed Aug 01 20:25:16 2007 +0200
+++ b/src/HOL/SET-Protocol/Merchant_Registration.thy Wed Aug 01 21:10:36 2007 +0200
@@ -289,7 +289,7 @@
add: analz_image_keys_simps abbrev_simps analz_knows_absorb
analz_knows_absorb2 analz_Key_image_insert_eq notin_image_iff
Spy_analz_private_Key analz_image_priEK)
- --{*23 seconds on a 1.8GHz machine*}
+ --{*5 seconds on a 1.6GHz machine*}
apply spy_analz --{*Fake*}
apply auto --{*Message 3*}
done
--- a/src/HOL/SET-Protocol/MessageSET.thy Wed Aug 01 20:25:16 2007 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy Wed Aug 01 21:10:36 2007 +0200
@@ -835,13 +835,8 @@
(*<*)
ML
{*
-val analz_increasing = thm "analz_increasing";
-val analz_subset_parts = thm "analz_subset_parts";
-val parts_analz = thm "parts_analz";
-val analz_parts = thm "analz_parts";
-val analz_insertI = thm "analz_insertI";
-val Fake_parts_insert = thm "Fake_parts_insert";
-val Fake_analz_insert = thm "Fake_analz_insert";
+structure MessageSET =
+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
@@ -859,9 +854,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;
@@ -870,8 +865,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 =
@@ -887,6 +882,8 @@
DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
+
+end
*}
(*>*)
@@ -938,17 +935,17 @@
method_setup spy_analz = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD' (gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
+ Method.SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
"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))) *}
+ Method.SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *}
"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))) *}
+ Method.SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *}
"for debugging spy_analz"
end
--- a/src/HOL/SET-Protocol/PublicSET.thy Wed Aug 01 20:25:16 2007 +0200
+++ b/src/HOL/SET-Protocol/PublicSET.thy Wed Aug 01 21:10:36 2007 +0200
@@ -345,19 +345,16 @@
ML
{*
-val Nonce_supply1 = thm "Nonce_supply1";
-val Nonce_supply = thm "Nonce_supply";
-
-val used_Says = thm "used_Says";
-val used_Notes = thm "used_Notes";
+structure PublicSET =
+struct
(*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 (ss delsimps [used_Says,used_Notes]))
+ (ALLGOALS (simp_tac (ss delsimps [@{thm used_Says}, @{thm used_Notes}]))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
- resolve_tac [refl, conjI, Nonce_supply]))
+ resolve_tac [refl, conjI, @{thm Nonce_supply}]))
(*Tactic for possibility theorems (ML script version)*)
fun possibility_tac state = gen_possibility_tac (simpset_of (Thm.theory_of_thm state)) state
@@ -369,11 +366,13 @@
(ALLGOALS (asm_simp_tac (simpset_of (Thm.theory_of_thm st) setSolver safe_solver))
THEN
REPEAT_FIRST (resolve_tac [refl, conjI]))
+
+end
*}
method_setup possibility = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (gen_possibility_tac (local_simpset_of ctxt))) *}
+ Method.SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *}
"for proving possibility theorems"
--- a/src/HOL/SET-Protocol/Purchase.thy Wed Aug 01 20:25:16 2007 +0200
+++ b/src/HOL/SET-Protocol/Purchase.thy Wed Aug 01 21:10:36 2007 +0200
@@ -335,7 +335,7 @@
THEN set_pur.AuthResUns [of concl: "PG j" M KP LID_M XID],
THEN Says_to_Gets,
THEN set_pur.PRes])
-apply (tactic "basic_possibility_tac")
+apply (tactic "PublicSET.basic_possibility_tac")
apply (simp_all add: used_Cons symKeys_neq_imp_neq)
done
@@ -371,7 +371,7 @@
THEN set_pur.AuthResS [of concl: "PG j" M KP LID_M XID],
THEN Says_to_Gets,
THEN set_pur.PRes])
-apply (tactic "basic_possibility_tac")
+apply (tactic "PublicSET.basic_possibility_tac")
apply (auto simp add: used_Cons symKeys_neq_imp_neq)
done
@@ -476,14 +476,11 @@
==> EK = pubEK C"
by (frule Gets_imp_Says, auto)
-ML
-{*
-val Gets_certificate_valid = thm "Gets_certificate_valid";
-
-fun valid_certificate_tac i =
- EVERY [ftac Gets_certificate_valid i,
- assume_tac i, REPEAT (hyp_subst_tac i)];
-*}
+method_setup valid_certificate_tac = {*
+ Method.goal_args (Scan.succeed ()) (fn () => fn i =>
+ EVERY [ftac @{thm Gets_certificate_valid} i,
+ assume_tac i, REPEAT (hyp_subst_tac i)])
+*} ""
subsection{*Proofs on Symmetric Keys*}
@@ -494,8 +491,8 @@
==> Key K \<notin> used evs --> K \<in> symKeys -->
K \<notin> keysFor (parts (knows Spy evs))"
apply (erule set_pur.induct)
-apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
-apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
+apply (valid_certificate_tac [8]) --{*PReqS*}
+apply (valid_certificate_tac [7]) --{*PReqUns*}
apply auto
apply (force dest!: usedI keysFor_parts_insert) --{*Fake*}
done
@@ -556,14 +553,14 @@
apply (rule_tac [!] allI)+
apply (rule_tac [!] impI [THEN Key_analz_image_Key_lemma, THEN impI])+
apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
-apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
-apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
+apply (valid_certificate_tac [8]) --{*PReqS*}
+apply (valid_certificate_tac [7]) --{*PReqUns*}
apply (simp_all
del: image_insert image_Un imp_disjL
add: analz_image_keys_simps disj_simps
analz_Key_image_insert_eq notin_image_iff
analz_insert_simps analz_image_priEK)
- --{*35 seconds on a 1.8GHz machine*}
+ --{*8 seconds on a 1.6GHz machine*}
apply spy_analz --{*Fake*}
apply (blast elim!: ballE)+ --{*PReq: unsigned and signed*}
done
@@ -589,14 +586,14 @@
apply (rule_tac [!] allI)+
apply (rule_tac [!] impI [THEN Nonce_analz_image_Key_lemma])+
apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
-apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
-apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
+apply (valid_certificate_tac [8]) --{*PReqS*}
+apply (valid_certificate_tac [7]) --{*PReqUns*}
apply (simp_all
del: image_insert image_Un imp_disjL
add: analz_image_keys_simps disj_simps symKey_compromise
analz_Key_image_insert_eq notin_image_iff
analz_insert_simps analz_image_priEK)
- --{*35 seconds on a 1.8GHz machine*}
+ --{*8 seconds on a 1.6GHz machine*}
apply spy_analz --{*Fake*}
apply (blast elim!: ballE) --{*PReqS*}
done
@@ -611,14 +608,14 @@
apply (erule rev_mp)
apply (erule set_pur.induct)
apply (frule_tac [9] AuthReq_msg_in_analz_spies)
-apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
+apply (valid_certificate_tac [8]) --{*PReqS*}
apply (simp_all
del: image_insert image_Un imp_disjL
add: analz_image_keys_simps disj_simps
symKey_compromise pushes sign_def Nonce_compromise
analz_Key_image_insert_eq notin_image_iff
analz_insert_simps analz_image_priEK)
- --{*13 seconds on a 1.8GHz machine*}
+ --{*2.5 seconds on a 1.6GHz machine*}
apply spy_analz
apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj]
@@ -653,15 +650,15 @@
apply (rule_tac [!] allI impI)+
apply (rule_tac [!] analz_image_pan_lemma)+
apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
-apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
-apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
+apply (valid_certificate_tac [8]) --{*PReqS*}
+apply (valid_certificate_tac [7]) --{*PReqUns*}
apply (simp_all
del: image_insert image_Un imp_disjL
add: analz_image_keys_simps
symKey_compromise pushes sign_def
analz_Key_image_insert_eq notin_image_iff
analz_insert_simps analz_image_priEK)
- --{*32 seconds on a 1.8GHz machine*}
+ --{*7 seconds on a 1.6GHz machine*}
apply spy_analz --{*Fake*}
apply auto
done
@@ -684,14 +681,14 @@
apply (erule rev_mp)
apply (erule set_pur.induct)
apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
-apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
-apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
+apply (valid_certificate_tac [8]) --{*PReqS*}
+apply (valid_certificate_tac [7]) --{*PReqUns*}
apply (simp_all
del: image_insert image_Un imp_disjL
add: analz_image_keys_simps analz_insert_pan analz_image_pan
notin_image_iff
analz_insert_simps analz_image_priEK)
- --{*15 seconds on a 1.8GHz machine*}
+ --{*3 seconds on a 1.6GHz machine*}
apply spy_analz --{*Fake*}
apply blast --{*PReqUns: unsigned*}
apply force --{*PReqS: signed*}
@@ -708,14 +705,14 @@
apply (erule rev_mp)
apply (erule set_pur.induct)
apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
-apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
-apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
+apply (valid_certificate_tac [8]) --{*PReqS*}
+apply (valid_certificate_tac [7]) --{*PReqUns*}
apply (simp_all
del: image_insert image_Un imp_disjL
add: analz_image_keys_simps analz_insert_pan analz_image_pan
notin_image_iff
analz_insert_simps analz_image_priEK)
- --{*17 seconds on a 1.8GHz machine*}
+ --{*3 seconds on a 1.6GHz machine*}
apply spy_analz --{*Fake*}
apply force --{*PReqUns: unsigned*}
apply blast --{*PReqS: signed*}
@@ -861,7 +858,7 @@
apply clarify
apply (erule rev_mp)
apply (erule set_pur.induct, simp_all)
-apply (tactic{*valid_certificate_tac 2*}) --{*PReqUns*}
+apply (valid_certificate_tac [2]) --{*PReqUns*}
apply auto
apply (blast dest: Gets_imp_Says Says_C_PInitRes)
done