# HG changeset patch # User wenzelm # Date 1185995436 -7200 # Node ID a0fc58900606f202dbdf4fa4460f7815521d8462 # Parent fc7f857d33c8c768bcca722a6e10b6d23e40b54f tuned ML bindings (for multithreading); updated timings; diff -r fc7f857d33c8 -r a0fc58900606 src/HOL/SET-Protocol/Cardholder_Registration.thy --- 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 \ analz (Key`KK Un H)) = (K \ KK | Key K \ 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 \ bad & CA i \ bad)" apply (erule_tac P = "U \ ?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 @@ \ parts (knows Spy evs) --> Nonce CardSecret \ 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 @@ \ parts (knows Spy evs) --> Nonce NonceCCA \ 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) \ 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*} diff -r fc7f857d33c8 -r a0fc58900606 src/HOL/SET-Protocol/EventSET.thy --- 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 \ 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 *} diff -r fc7f857d33c8 -r a0fc58900606 src/HOL/SET-Protocol/Merchant_Registration.thy --- 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 diff -r fc7f857d33c8 -r a0fc58900606 src/HOL/SET-Protocol/MessageSET.thy --- 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 \ Key`shrK`bad and cannot be proved by rewriting @@ -859,9 +854,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; @@ -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 diff -r fc7f857d33c8 -r a0fc58900606 src/HOL/SET-Protocol/PublicSET.thy --- 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" diff -r fc7f857d33c8 -r a0fc58900606 src/HOL/SET-Protocol/Purchase.thy --- 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 \ used evs --> K \ symKeys --> K \ 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