# HG changeset patch # User paulson # Date 863002903 -7200 # Node ID cbb6c0c1c58ae91ff5046b9cc6df9ed4c3fc7666 # Parent c58423c207408f7485717a28cf82bec00b8ee175 Conversion to use blast_tac (with other improvements) diff -r c58423c20740 -r cbb6c0c1c58a src/HOL/Auth/Message.ML --- a/src/HOL/Auth/Message.ML Wed May 07 12:50:26 1997 +0200 +++ b/src/HOL/Auth/Message.ML Wed May 07 13:01:43 1997 +0200 @@ -35,7 +35,7 @@ goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))"; by (Blast_tac 1); -qed "keysFor_UN"; +qed "keysFor_UN1"; (*Monotonicity*) goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)"; @@ -67,9 +67,11 @@ by (Auto_tac()); qed "keysFor_insert_Crypt"; -Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, +Addsimps [keysFor_empty, keysFor_Un, keysFor_UN1, keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt]; +AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE, + keysFor_UN1 RS equalityD1 RS subsetD RS UN1_E]; goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H"; by (Blast_tac 1); @@ -173,8 +175,12 @@ by (simp_tac (!simpset addsimps [UNION1_def, parts_UN]) 1); qed "parts_UN1"; -(*Added to simplify arguments to parts, analz and synth*) +(*Added to simplify arguments to parts, analz and synth. + NOTE: the UN versions are no longer used!*) Addsimps [parts_Un, parts_UN, parts_UN1]; +AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE, + parts_UN RS equalityD1 RS subsetD RS UN_E, + parts_UN1 RS equalityD1 RS subsetD RS UN1_E]; goal thy "insert X (parts H) <= parts(insert X H)"; by (blast_tac (!claset addIs [impOfSubs parts_mono]) 1); @@ -809,6 +815,21 @@ (*Cannot be added with Addsimps -- we don't always want to re-order messages*) val pushes = pushKeys@pushCrypts; + +(*** Tactics useful for many protocol proofs ***) + +(*Prove base case (subgoal i) and simplify others*) +fun prove_simple_subgoals_tac i = + fast_tac (!claset addss (!simpset)) i THEN + ALLGOALS Asm_simp_tac; + +fun Fake_parts_insert_tac i = + blast_tac (!claset addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert]) i; + +(*Apply rules to break down assumptions of the form + 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' diff -r c58423c20740 -r cbb6c0c1c58a src/HOL/Auth/NS_Public.ML --- a/src/HOL/Auth/NS_Public.ML Wed May 07 12:50:26 1997 +0200 +++ b/src/HOL/Auth/NS_Public.ML Wed May 07 13:01:43 1997 +0200 @@ -12,15 +12,12 @@ proof_timing:=true; HOL_quantifiers := false; -val op addss = op unsafe_addss; - AddIffs [Spy_in_lost]; (*Replacing the variable by a constant improves search speed by 50%!*) val Says_imp_sees_Spy' = read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy; - (*A "possibility property": there are traces that reach the end*) goal thy "!!A B. A ~= B ==> EX NB. EX evs: ns_public. \ @@ -42,17 +39,6 @@ AddSEs [not_Says_to_self RSN (2, rev_notE)]; -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) -fun parts_induct_tac i = SELECT_GOAL - (DETERM (etac ns_public.induct 1 THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 2)) THEN - (*Base case*) - fast_tac (!claset addss (!simpset)) 1 THEN - ALLGOALS Asm_simp_tac) i; - (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY sends messages containing X! **) @@ -60,8 +46,9 @@ goal thy "!!evs. evs : ns_public \ \ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)"; -by (parts_induct_tac 1); -by (Auto_tac()); +by (etac ns_public.induct 1); +by (prove_simple_subgoals_tac 1); +by (Fake_parts_insert_tac 1); qed "Spy_see_priK"; Addsimps [Spy_see_priK]; @@ -74,7 +61,7 @@ goal thy "!!A. [| Key (priK A) : parts (sees lost Spy evs); \ \ evs : ns_public |] ==> A:lost"; -by (fast_tac (!claset addDs [Spy_see_priK]) 1); +by (blast_tac (!claset addDs [Spy_see_priK]) 1); qed "Spy_see_priK_D"; bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D); @@ -82,7 +69,7 @@ fun analz_induct_tac i = - etac ns_public.induct i THEN + etac ns_public.induct i THEN ALLGOALS (asm_simp_tac (!simpset addsimps [not_parts_not_analz] setloop split_tac [expand_if])); @@ -100,16 +87,15 @@ by (etac rev_mp 1); by (analz_induct_tac 1); (*NS3*) -by (fast_tac (!claset addSEs partsEs) 4); +by (blast_tac (!claset addSEs partsEs) 4); (*NS2*) -by (fast_tac (!claset addSEs partsEs) 3); +by (blast_tac (!claset addSEs partsEs) 3); (*Fake*) -by (deepen_tac (!claset addSIs [analz_insertI] +by (blast_tac (!claset addSIs [analz_insertI] addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 0 2); + impOfSubs Fake_parts_insert]) 2); (*Base*) -by (fast_tac (!claset addss (!simpset)) 1); +by (Blast_tac 1); qed "no_nonce_NS1_NS2"; @@ -124,17 +110,16 @@ (*NS1*) by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); by (expand_case_tac "NA = ?y" 3 THEN - REPEAT (fast_tac (!claset addSEs partsEs) 3)); + REPEAT (blast_tac (!claset addSEs partsEs) 3)); (*Base*) -by (fast_tac (!claset addss (!simpset)) 1); +by (Blast_tac 1); (*Fake*) by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1); by (step_tac (!claset addSIs [analz_insertI]) 1); by (ex_strip_tac 1); -by (best_tac (!claset delrules [conjI] +by (blast_tac (!claset delrules [conjI] addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); + addDs [impOfSubs analz_subset_parts]) 1); val lemma = result(); goal thy @@ -155,14 +140,14 @@ by (etac rev_mp 1); by (analz_induct_tac 1); (*NS3*) -by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] - addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj] + addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); (*NS2*) -by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] - addSEs [MPair_parts] - addDs [parts.Body, unique_NA]) 0 3); +by (blast_tac (!claset addSEs [MPair_parts] + addDs [Says_imp_sees_Spy' RS parts.Inj, + parts.Body, unique_NA]) 3); (*NS1*) -by (fast_tac (!claset addSEs sees_Spy_partsEs +by (blast_tac (!claset addSEs sees_Spy_partsEs addIs [impOfSubs analz_subset_parts]) 2); (*Fake*) by (spy_analz_tac 1); @@ -184,15 +169,11 @@ by (etac ns_public.induct 1); by (ALLGOALS Asm_simp_tac); (*NS1*) -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); (*Fake*) -by (REPEAT_FIRST (resolve_tac [impI, conjI])); -by (fast_tac (!claset addss (!simpset)) 1); -by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); -by (best_tac (!claset addSIs [disjI2] - addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); +by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] + addDs [Spy_not_see_NA, + impOfSubs analz_subset_parts]) 1); qed "A_trusts_NS2"; (*If the encrypted message appears then it originated with Alice in NS1*) @@ -205,13 +186,11 @@ by (etac rev_mp 1); by (analz_induct_tac 1); (*Fake*) -by (best_tac (!claset addSIs [disjI2] - addSDs [impOfSubs Fake_parts_insert] - addIs [analz_insertI] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 2); +by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] + addIs [analz_insertI] + addDs [impOfSubs analz_subset_parts]) 2); (*Base*) -by (fast_tac (!claset addss (!simpset)) 1); +by (Blast_tac 1); qed "B_trusts_NS1"; @@ -231,17 +210,16 @@ (*NS2*) by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); by (expand_case_tac "NB = ?y" 3 THEN - REPEAT (fast_tac (!claset addSEs partsEs) 3)); + REPEAT (blast_tac (!claset addSEs partsEs) 3)); (*Base*) -by (fast_tac (!claset addss (!simpset)) 1); +by (Blast_tac 1); (*Fake*) by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1); by (step_tac (!claset addSIs [analz_insertI]) 1); by (ex_strip_tac 1); -by (best_tac (!claset delrules [conjI] +by (blast_tac (!claset delrules [conjI] addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); + addDs [impOfSubs analz_subset_parts]) 1); val lemma = result(); goal thy @@ -265,26 +243,21 @@ by (etac rev_mp 1); by (analz_induct_tac 1); (*NS3*) -by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] - addDs [unique_NB]) 4); +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj, + unique_NB]) 4); (*NS1*) -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); (*Fake*) by (spy_analz_tac 1); (*NS2*) by (Step_tac 1); -by (fast_tac (!claset addSEs sees_Spy_partsEs) 3); -by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] - addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2); -by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 3); +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2); +by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1); qed "Spy_not_see_NB"; -(*Matches only NS2, not NS1 (or NS3)*) -val Says_imp_sees_Spy'' = - read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy'; - - (*Authentication for B: if he receives message 3 and has used NB in message 2, then A has sent message 3.*) goal thy @@ -296,28 +269,27 @@ by (etac rev_mp 1); (*prepare induction over Crypt (pubK B) NB : parts H*) by (etac (Says_imp_sees_Spy' RS parts.Inj RS rev_mp) 1); -by (etac ns_public.induct 1); -by (ALLGOALS Asm_simp_tac); +by (analz_induct_tac 1); (*NS1*) -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); (*Fake*) -by (REPEAT_FIRST (resolve_tac [impI, conjI])); -by (fast_tac (!claset addss (!simpset)) 1); -by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); -by (best_tac (!claset addSIs [disjI2] - addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); -(*NS3*) +by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] + addDs [Spy_not_see_NB, + impOfSubs analz_subset_parts]) 1); +(*NS3; not clear why blast_tac needs to be preceeded by Step_tac*) by (Step_tac 1); -by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); -by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj] - addDs [unique_NB]) 1); +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj, + Spy_not_see_NB, unique_NB]) 1); qed "B_trusts_NS3"; (**** Overall guarantee for B*) +(*Matches only NS2, not NS1 (or NS3)*) +val Says_imp_sees_Spy'' = + read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy'; + + (*If B receives NS3 and the nonce NB agrees with the nonce he joined with NA, then A initiated the run using NA. SAME proof as B_trusts_NS3!*) goal thy @@ -333,19 +305,18 @@ by (ALLGOALS Asm_simp_tac); (*Fake, NS2, NS3*) (*NS1*) -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); (*Fake*) by (REPEAT_FIRST (resolve_tac [impI, conjI])); -by (fast_tac (!claset addss (!simpset)) 1); +by (Blast_tac 1); by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); -by (best_tac (!claset addSIs [disjI2] +by (blast_tac (!claset addSIs [disjI2] addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 1); + impOfSubs Fake_parts_insert]) 1); (*NS3*) by (Step_tac 1); by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); -by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj] - addDs [unique_NB]) 1); +by (blast_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj] + addDs [unique_NB]) 1); qed "B_trusts_protocol"; diff -r c58423c20740 -r cbb6c0c1c58a src/HOL/Auth/NS_Public_Bad.ML --- a/src/HOL/Auth/NS_Public_Bad.ML Wed May 07 12:50:26 1997 +0200 +++ b/src/HOL/Auth/NS_Public_Bad.ML Wed May 07 13:01:43 1997 +0200 @@ -16,15 +16,12 @@ proof_timing:=true; HOL_quantifiers := false; -val op addss = op unsafe_addss; - AddIffs [Spy_in_lost]; (*Replacing the variable by a constant improves search speed by 50%!*) val Says_imp_sees_Spy' = read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy; - (*A "possibility property": there are traces that reach the end*) goal thy "!!A B. A ~= B ==> EX NB. EX evs: ns_public. \ @@ -46,17 +43,6 @@ AddSEs [not_Says_to_self RSN (2, rev_notE)]; -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) -fun parts_induct_tac i = SELECT_GOAL - (DETERM (etac ns_public.induct 1 THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 2)) THEN - (*Base case*) - fast_tac (!claset addss (!simpset)) 1 THEN - ALLGOALS Asm_simp_tac) i; - (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY sends messages containing X! **) @@ -64,8 +50,9 @@ goal thy "!!evs. evs : ns_public \ \ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)"; -by (parts_induct_tac 1); -by (Auto_tac()); +by (etac ns_public.induct 1); +by (prove_simple_subgoals_tac 1); +by (Fake_parts_insert_tac 1); qed "Spy_see_priK"; Addsimps [Spy_see_priK]; @@ -78,7 +65,7 @@ goal thy "!!A. [| Key (priK A) : parts (sees lost Spy evs); \ \ evs : ns_public |] ==> A:lost"; -by (fast_tac (!claset addDs [Spy_see_priK]) 1); +by (blast_tac (!claset addDs [Spy_see_priK]) 1); qed "Spy_see_priK_D"; bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D); @@ -86,7 +73,7 @@ fun analz_induct_tac i = - etac ns_public.induct i THEN + etac ns_public.induct i THEN ALLGOALS (asm_simp_tac (!simpset addsimps [not_parts_not_analz] setloop split_tac [expand_if])); @@ -105,16 +92,15 @@ by (etac rev_mp 1); by (analz_induct_tac 1); (*NS3*) -by (fast_tac (!claset addSEs partsEs) 4); +by (blast_tac (!claset addSEs partsEs) 4); (*NS2*) -by (fast_tac (!claset addSEs partsEs) 3); +by (blast_tac (!claset addSEs partsEs) 3); (*Fake*) -by (deepen_tac (!claset addSIs [analz_insertI] +by (blast_tac (!claset addSIs [analz_insertI] addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 0 2); + impOfSubs Fake_parts_insert]) 2); (*Base*) -by (fast_tac (!claset addss (!simpset)) 1); +by (Blast_tac 1); qed "no_nonce_NS1_NS2"; @@ -129,17 +115,16 @@ (*NS1*) by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); by (expand_case_tac "NA = ?y" 3 THEN - REPEAT (fast_tac (!claset addSEs partsEs) 3)); + REPEAT (blast_tac (!claset addSEs partsEs) 3)); (*Base*) -by (fast_tac (!claset addss (!simpset)) 1); +by (Blast_tac 1); (*Fake*) by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1); by (step_tac (!claset addSIs [analz_insertI]) 1); by (ex_strip_tac 1); -by (best_tac (!claset delrules [conjI] +by (blast_tac (!claset delrules [conjI] addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); + addDs [impOfSubs analz_subset_parts]) 1); val lemma = result(); goal thy @@ -160,15 +145,15 @@ by (etac rev_mp 1); by (analz_induct_tac 1); (*NS3*) -by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] - addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj] + addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); (*NS2*) -by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] - addSEs [MPair_parts] - addDs [parts.Body, unique_NA]) 0 3); +by (blast_tac (!claset addSEs [MPair_parts] + addDs [Says_imp_sees_Spy' RS parts.Inj, + parts.Body, unique_NA]) 3); (*NS1*) -by (fast_tac (!claset addSEs sees_Spy_partsEs - addIs [impOfSubs analz_subset_parts]) 2); +by (blast_tac (!claset addSEs sees_Spy_partsEs + addIs [impOfSubs analz_subset_parts]) 2); (*Fake*) by (spy_analz_tac 1); qed "Spy_not_see_NA"; @@ -187,20 +172,15 @@ by (etac ns_public.induct 1); by (ALLGOALS Asm_simp_tac); (*NS1*) -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); (*Fake*) -by (REPEAT_FIRST (resolve_tac [impI, conjI])); -by (fast_tac (!claset addss (!simpset)) 1); -by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); -by (best_tac (!claset addSIs [disjI2] - addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); -(*NS2*) +by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] + addDs [Spy_not_see_NA, + impOfSubs analz_subset_parts]) 1); +(*NS2; not clear why blast_tac needs to be preceeded by Step_tac*) by (Step_tac 1); -by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); -by (deepen_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] - addDs [unique_NA]) 1 1); +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj, + Spy_not_see_NA, unique_NA]) 1); qed "A_trusts_NS2"; (*If the encrypted message appears then it originated with Alice in NS1*) @@ -213,14 +193,12 @@ by (etac rev_mp 1); by (analz_induct_tac 1); (*Fake*) -by (best_tac (!claset addSIs [disjI2] - addSDs [impOfSubs Fake_parts_insert] - addIs [analz_insertI] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 2); +by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] + addIs [analz_insertI] + addDs [impOfSubs analz_subset_parts]) 2); (*Base*) -by (fast_tac (!claset addss (!simpset)) 1); -qed_spec_mp "B_trusts_NS1"; +by (Blast_tac 1); +qed "B_trusts_NS1"; @@ -238,17 +216,16 @@ (*NS2*) by (simp_tac (!simpset addsimps [all_conj_distrib]) 3); by (expand_case_tac "NB = ?y" 3 THEN - REPEAT (fast_tac (!claset addSEs partsEs) 3)); + REPEAT (blast_tac (!claset addSEs partsEs) 3)); (*Base*) -by (fast_tac (!claset addss (!simpset)) 1); +by (Blast_tac 1); (*Fake*) by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1); by (step_tac (!claset addSIs [analz_insertI]) 1); by (ex_strip_tac 1); -by (best_tac (!claset delrules [conjI] +by (blast_tac (!claset delrules [conjI] addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); + addDs [impOfSubs analz_subset_parts]) 1); val lemma = result(); goal thy @@ -271,22 +248,21 @@ by (etac rev_mp 1); by (analz_induct_tac 1); (*NS1*) -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); (*Fake*) by (spy_analz_tac 1); (*NS2 and NS3*) by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); by (step_tac (!claset delrules [allI]) 1); -by (Fast_tac 5); -by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1); +by (Blast_tac 5); +(*NS3*) +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj, + Spy_not_see_NB, unique_NB]) 4); (*NS2*) -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); -by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] - addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); -(*NS3*) -by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1 - THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1)); -by (Fast_tac 1); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 3); +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2); +by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts]) 1); qed "Spy_not_see_NB"; @@ -305,22 +281,15 @@ by (analz_induct_tac 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); (*NS1*) -by (fast_tac (!claset addSEs sees_Spy_partsEs) 2); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 2); (*Fake*) -by (REPEAT_FIRST (resolve_tac [impI, conjI])); -by (fast_tac (!claset addss (!simpset)) 1); -by (rtac (ccontr RS disjI2) 1); -by (forward_tac [Spy_not_see_NB] 1 THEN (REPEAT_FIRST assume_tac) - THEN Fast_tac 1); -by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); -(*NS3*) +by (blast_tac (!claset addSDs [impOfSubs Fake_parts_insert] + addDs [Spy_not_see_NB, + impOfSubs analz_subset_parts]) 1); +(*NS3; not clear why blast_tac needs to be preceeded by Step_tac*) by (Step_tac 1); -by (forward_tac [Spy_not_see_NB] 1 THEN (REPEAT_FIRST assume_tac) - THEN Fast_tac 1); -by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] - addDs [unique_NB]) 1); +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj, + Spy_not_see_NB, unique_NB]) 1); qed "B_trusts_NS3"; @@ -331,18 +300,18 @@ \ --> Nonce NB ~: analz (sees lost Spy evs)"; by (analz_induct_tac 1); (*NS1*) -by (fast_tac (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); +by (blast_tac (!claset addSEs partsEs + addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); (*Fake*) by (spy_analz_tac 1); (*NS2 and NS3*) by (Step_tac 1); -by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1); +by (blast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1); (*NS2*) -by (fast_tac (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); -by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] - addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); +by (blast_tac (!claset addSEs partsEs + addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2); +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); (*NS3*) by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1 THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1)); diff -r c58423c20740 -r cbb6c0c1c58a src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Wed May 07 12:50:26 1997 +0200 +++ b/src/HOL/Auth/NS_Shared.ML Wed May 07 13:01:43 1997 +0200 @@ -15,6 +15,9 @@ proof_timing:=true; HOL_quantifiers := false; +(*Replacing the variable by a constant improves search speed by 50%!*) +val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy; + (*A "possibility property": there are traces that reach the end*) goal thy @@ -35,7 +38,7 @@ by (rtac subsetI 1); by (etac ns_shared.induct 1); by (REPEAT_FIRST - (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono) + (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono) :: ns_shared.intrs)))); qed "ns_shared_mono"; @@ -51,29 +54,23 @@ (*For reasoning about the encrypted portion of message NS3*) goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set_of_list evs \ \ ==> X : parts (sees lost Spy evs)"; -by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); qed "NS3_msg_in_parts_sees_Spy"; goal thy "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set_of_list evs \ \ ==> K : parts (sees lost Spy evs)"; -by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); qed "Oops_parts_sees_Spy"; -val parts_Fake_tac = - dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5 THEN - forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8; - -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) -fun parts_induct_tac i = SELECT_GOAL - (DETERM (etac ns_shared.induct 1 THEN parts_Fake_tac THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 2)) THEN - (*Base case*) - fast_tac (!claset addss (!simpset)) 1 THEN - ALLGOALS Asm_simp_tac) i; +(*For proving the easier theorems about X ~: parts (sees lost Spy evs). + We instantiate the variable to "lost" since leaving it as a Var would + interfere with simplification.*) +val parts_induct_tac = + etac ns_shared.induct 1 THEN + dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5 THEN + forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8 THEN + prove_simple_subgoals_tac 1; (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY @@ -83,8 +80,9 @@ goal thy "!!evs. evs : ns_shared lost \ \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; -by (parts_induct_tac 1); -by (Auto_tac()); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -97,7 +95,7 @@ goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ \ evs : ns_shared lost |] ==> A:lost"; -by (fast_tac (!claset addDs [Spy_see_shrK]) 1); +by (blast_tac (!claset addDs [Spy_see_shrK]) 1); qed "Spy_see_shrK_D"; bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); @@ -107,15 +105,15 @@ (*Nobody can have used non-existent keys!*) goal thy "!!evs. evs : ns_shared lost ==> \ \ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; -by (parts_induct_tac 1); +by parts_induct_tac; (*Fake*) by (best_tac (!claset addIs [impOfSubs analz_subset_parts] addDs [impOfSubs (analz_subset_parts RS keysFor_mono), impOfSubs (parts_insert_subset_Un RS keysFor_mono)] - unsafe_addss (!simpset)) 1); + addss (!simpset)) 1); (*NS2, NS4, NS5*) -by (REPEAT (fast_tac (!claset addSEs sees_Spy_partsEs addss (!simpset)) 1)); +by (ALLGOALS (blast_tac (!claset addSEs sees_Spy_partsEs))); qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", @@ -152,7 +150,8 @@ \ Crypt (shrK B) {|Key K, Agent A|}|}) \ \ : set_of_list evs"; by (etac rev_mp 1); -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); by (Auto_tac()); qed "A_trusts_NS2"; @@ -163,20 +162,19 @@ goal thy "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \ \ : set_of_list evs; evs : ns_shared lost |] \ -\ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \ +\ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \ \ | X : analz (sees lost Spy evs)"; by (case_tac "A : lost" 1); -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] - unsafe_addss (!simpset)) 1); +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj] + addss (!simpset)) 1); by (forward_tac [Says_imp_sees_Spy RS parts.Inj] 1); -by (fast_tac (!claset addEs partsEs - addSDs [A_trusts_NS2, Says_Server_message_form] - addss (!simpset)) 1); +by (blast_tac (!claset addEs partsEs + addSDs [A_trusts_NS2, Says_Server_message_form]) 1); qed "Says_S_message_form"; (*For proofs involving analz. We again instantiate the variable to "lost".*) -val analz_Fake_tac = +val analz_sees_tac = forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac); @@ -200,15 +198,12 @@ "!!evs. [| evs : ns_shared lost; Kab ~: range shrK |] ==> \ \ (Crypt KAB X) : parts (sees lost Spy evs) & \ \ Key K : parts {X} --> Key K : parts (sees lost Spy evs)"; -by (etac ns_shared.induct 1); -by parts_Fake_tac; -by (ALLGOALS Asm_simp_tac); +by parts_induct_tac; (*Deals with Faked messages*) -by (best_tac (!claset addSEs partsEs - addDs [impOfSubs parts_insert_subset_Un] - addss (!simpset)) 2); +by (blast_tac (!claset addSEs partsEs + addDs [impOfSubs parts_insert_subset_Un]) 1); (*Base, NS4 and NS5*) -by (ALLGOALS (fast_tac (!claset addss (!simpset)))); +by (Auto_tac()); result(); @@ -221,7 +216,7 @@ \ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ \ (K : KK | Key K : analz (sees lost Spy evs))"; by (etac ns_shared.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); (*Takes 24 secs*) @@ -229,7 +224,7 @@ (*NS4, Fake*) by (EVERY (map spy_analz_tac [3,2])); (*Base*) -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); +by (Blast_tac 1); qed_spec_mp "analz_image_freshK"; @@ -253,13 +248,12 @@ by (Step_tac 1); (*NS3*) by (ex_strip_tac 2); -by (Fast_tac 2); +by (Blast_tac 2); (*NS2: it can't be a new key*) by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); -by (fast_tac (!claset delrules [conjI] (*prevent split-up into 4 subgoals*) - addSEs sees_Spy_partsEs - addss (!simpset addsimps [parts_insertI])) 1); +by (blast_tac (!claset delrules [conjI] (*prevent split-up into 4 subgoals*) + addSEs sees_Spy_partsEs) 1); val lemma = result(); (*In messages of this form, the session key uniquely identifies the rest*) @@ -286,7 +280,7 @@ \ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) --> \ \ Key K ~: analz (sees lost Spy evs)"; by (etac ns_shared.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (ALLGOALS (asm_simp_tac (!simpset addsimps ([not_parts_not_analz, analz_insert_freshK] @ pushes) @@ -294,17 +288,16 @@ (*NS4, Fake*) by (EVERY (map spy_analz_tac [4,1])); (*NS2*) -by (fast_tac (!claset addSEs sees_Spy_partsEs - addIs [parts_insertI, impOfSubs analz_subset_parts] - addss (!simpset)) 1); +by (blast_tac (!claset addSEs sees_Spy_partsEs + addIs [parts_insertI, impOfSubs analz_subset_parts]) 1); (*Oops*) -by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 2); +by (blast_tac (!claset addDs [unique_session_keys]) 2); (*NS3*) (**LEVEL 6 **) by (step_tac (!claset delrules [impCE]) 1); -by (forward_tac [Says_imp_sees_Spy RS parts.Inj RS A_trusts_NS2] 1); +by (forward_tac [Says_imp_sees_Spy' RS parts.Inj RS A_trusts_NS2] 1); by (assume_tac 2); -by (fast_tac (!claset addSEs [Says_Crypt_not_lost]) 1); -by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1); +by (blast_tac (!claset addSDs [Says_Crypt_not_lost]) 1); +by (blast_tac (!claset addDs [unique_session_keys]) 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); @@ -316,7 +309,7 @@ \ A ~: lost; B ~: lost; evs : ns_shared lost \ \ |] ==> Key K ~: analz (sees lost Spy evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); -by (fast_tac (!claset addSEs [lemma]) 1); +by (blast_tac (!claset addSDs [lemma]) 1); qed "Spy_not_see_encrypted_key"; @@ -330,7 +323,7 @@ by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); -by (REPEAT_FIRST (fast_tac (!claset addIs [ns_shared_mono RS subsetD]))); +by (REPEAT_FIRST (blast_tac (!claset addIs [ns_shared_mono RS subsetD]))); qed "Agent_not_see_encrypted_key"; @@ -349,13 +342,10 @@ \ Crypt (shrK B) {|Key K, Agent A|}|}) \ \ : set_of_list evs"; by (etac rev_mp 1); -by (etac ns_shared.induct 1); -by parts_Fake_tac; +by parts_induct_tac; +by (Fake_parts_insert_tac 1); (*Fake case*) -by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 2); -by (Auto_tac()); +by (ALLGOALS Blast_tac); qed "B_trusts_NS3"; @@ -368,28 +358,28 @@ \ Says B A (Crypt K (Nonce NB)) : set_of_list evs"; by (etac ns_shared.induct 1); by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); -by parts_Fake_tac; +by (dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5); +by (forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8); by (TRYALL (rtac impI)); by (REPEAT_FIRST (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD))); by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); -(**LEVEL 6**) -by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert] - addDs [impOfSubs analz_subset_parts]) 1); -by (Fast_tac 2); +(**LEVEL 7**) +by (blast_tac (!claset addSDs [Crypt_Fake_parts_insert] + addDs [impOfSubs analz_subset_parts]) 1); +by (Blast_tac 2); by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac)); (*Subgoal 1: contradiction from the assumptions Key K ~: used evsa and Crypt K (Nonce NB) : parts (sees lost Spy evsa) *) by (dtac Crypt_imp_invKey_keysFor 1); -(**LEVEL 10**) +(**LEVEL 11**) by (Asm_full_simp_tac 1); by (rtac disjI1 1); by (thin_tac "?PP-->?QQ" 1); by (case_tac "Ba : lost" 1); -by (dtac Says_Crypt_lost 1 THEN assume_tac 1 THEN Fast_tac 1); -by (dtac (Says_imp_sees_Spy RS parts.Inj RS B_trusts_NS3) 1 THEN - REPEAT (assume_tac 1)); -by (best_tac (!claset addDs [unique_session_keys]) 1); +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS B_trusts_NS3, + unique_session_keys]) 2); +by (blast_tac (!claset addDs [Says_Crypt_lost]) 1); val lemma = result(); goal thy @@ -399,6 +389,6 @@ \ ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs; \ \ A ~: lost; B ~: lost; evs : ns_shared lost |] \ \ ==> Says B A (Crypt K (Nonce NB)) : set_of_list evs"; -by (fast_tac (!claset addSIs [lemma RS mp RS mp RS mp] - addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1); +by (blast_tac (!claset addSIs [lemma RS mp RS mp RS mp] + addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1); qed "A_trusts_NS4"; diff -r c58423c20740 -r cbb6c0c1c58a src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Wed May 07 12:50:26 1997 +0200 +++ b/src/HOL/Auth/OtwayRees.ML Wed May 07 13:01:43 1997 +0200 @@ -18,8 +18,7 @@ HOL_quantifiers := false; (*Replacing the variable by a constant improves search speed by 50%!*) -val Says_imp_sees_Spy' = - read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy; +val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy; (*A "possibility property": there are traces that reach the end*) @@ -81,35 +80,30 @@ bind_thm ("OR4_parts_sees_Spy", OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); -(*We instantiate the variable to "lost". Leaving it as a Var makes proofs - harder to complete, since simplification does less for us.*) -val parts_Fake_tac = +(*For proving the easier theorems about X ~: parts (sees lost Spy evs). + We instantiate the variable to "lost" since leaving it as a Var would + interfere with simplification.*) +val parts_induct_tac = let val tac = forw_inst_tac [("lost","lost")] - in tac OR2_parts_sees_Spy 4 THEN + in etac otway.induct 1 THEN + tac OR2_parts_sees_Spy 4 THEN tac OR4_parts_sees_Spy 6 THEN - tac Oops_parts_sees_Spy 7 + tac Oops_parts_sees_Spy 7 THEN + prove_simple_subgoals_tac 1 end; -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) -fun parts_induct_tac i = SELECT_GOAL - (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - unsafe_addss (!simpset)) 2)) THEN - (*Base case*) - fast_tac (!claset unsafe_addss (!simpset)) 1 THEN - ALLGOALS Asm_simp_tac) i; (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY sends messages containing X! **) + (*Spy never sees another agent's shared key! (unless it's lost at start)*) goal thy "!!evs. evs : otway lost \ \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; -by (parts_induct_tac 1); -by (Auto_tac()); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -132,7 +126,7 @@ (*Nobody can have used non-existent keys!*) goal thy "!!evs. evs : otway lost ==> \ \ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; -by (parts_induct_tac 1); +by parts_induct_tac; (*Fake*) by (best_tac (!claset addIs [impOfSubs analz_subset_parts] @@ -167,7 +161,7 @@ (*For proofs involving analz. We again instantiate the variable to "lost".*) -val analz_Fake_tac = +val analz_sees_tac = dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN @@ -194,7 +188,7 @@ \ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ \ (K : KK | Key K : analz (sees lost Spy evs))"; by (etac otway.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); @@ -254,7 +248,8 @@ \ Says A B {|NA, Agent A, Agent B, \ \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ \ : set_of_list evs"; -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); qed_spec_mp "Crypt_imp_OR1"; @@ -265,7 +260,8 @@ \ ==> EX B'. ALL B. \ \ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (sees lost Spy evs) \ \ --> B = B'"; -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); (*OR1: creation of new Nonce. Move assertion into global context*) by (expand_case_tac "NA = ?y" 1); @@ -290,7 +286,8 @@ \ : parts (sees lost Spy evs) --> \ \ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ \ ~: parts (sees lost Spy evs)"; -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); by (REPEAT (blast_tac (!claset addSEs sees_Spy_partsEs addSDs [impOfSubs parts_insert_subset_Un]) 1)); qed_spec_mp"no_nonce_OR1_OR2"; @@ -309,7 +306,8 @@ \ Crypt (shrK A) {|NA, Key K|}, \ \ Crypt (shrK B) {|NB, Key K|}|} \ \ : set_of_list evs)"; -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); (*OR1: it cannot be a new Nonce, contradiction.*) by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1); (*OR3 and OR4*) @@ -364,7 +362,7 @@ \ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \ \ Key K ~: analz (sees lost Spy evs)"; by (etac otway.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong] addsimps [not_parts_not_analz, analz_insert_freshK] @@ -418,7 +416,8 @@ \ {|NA, Agent A, Agent B, X, \ \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ \ : set_of_list evs)"; -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); by (ALLGOALS Blast_tac); bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE); @@ -430,7 +429,8 @@ \ ==> EX NA' A'. ALL NA A. \ \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(sees lost Spy evs) \ \ --> NA = NA' & A = A'"; -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); (*OR2: creation of new Nonce. Move assertion into global context*) by (expand_case_tac "NB = ?y" 1); @@ -461,7 +461,8 @@ \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ \ Crypt (shrK B) {|NB, Key K|}|} \ \ : set_of_list evs)"; -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); (*OR1: it cannot be a new Nonce, contradiction.*) by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1); (*OR4*) diff -r c58423c20740 -r cbb6c0c1c58a src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Wed May 07 12:50:26 1997 +0200 +++ b/src/HOL/Auth/OtwayRees_AN.ML Wed May 07 13:01:43 1997 +0200 @@ -69,22 +69,17 @@ bind_thm ("OR4_parts_sees_Spy", OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); -(*We instantiate the variable to "lost". Leaving it as a Var makes proofs - harder to complete, since simplification does less for us.*) -val parts_Fake_tac = - forw_inst_tac [("lost","lost")] OR4_parts_sees_Spy 6 THEN - forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 7; +(*For proving the easier theorems about X ~: parts (sees lost Spy evs). + We instantiate the variable to "lost" since leaving it as a Var would + interfere with simplification.*) +val parts_induct_tac = + let val tac = forw_inst_tac [("lost","lost")] + in etac otway.induct 1 THEN + tac OR4_parts_sees_Spy 6 THEN + tac Oops_parts_sees_Spy 7 THEN + prove_simple_subgoals_tac 1 + end; -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) -fun parts_induct_tac i = SELECT_GOAL - (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 2)) THEN - (*Base case*) - fast_tac (!claset addss (!simpset)) 1 THEN - ALLGOALS Asm_simp_tac) i; (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY sends messages containing X! **) @@ -93,8 +88,9 @@ goal thy "!!evs. evs : otway lost \ \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; -by (parts_induct_tac 1); -by (Auto_tac()); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -117,7 +113,7 @@ (*Nobody can have used non-existent keys!*) goal thy "!!evs. evs : otway lost ==> \ \ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; -by (parts_induct_tac 1); +by parts_induct_tac; (*Fake*) by (best_tac (!claset addIs [impOfSubs analz_subset_parts] @@ -154,7 +150,7 @@ (*For proofs involving analz. We again instantiate the variable to "lost".*) -val analz_Fake_tac = +val analz_sees_tac = dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN assume_tac 7 THEN @@ -180,7 +176,7 @@ \ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ \ (K : KK | Key K : analz (sees lost Spy evs))"; by (etac otway.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); (*14 seconds*) @@ -250,7 +246,8 @@ \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ \ : set_of_list evs)"; -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); (*OR3*) by (Blast_tac 1); @@ -285,7 +282,7 @@ \ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \ \ Key K ~: analz (sees lost Spy evs)"; by (etac otway.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong] addsimps [not_parts_not_analz, @@ -340,7 +337,8 @@ \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ \ : set_of_list evs)"; -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); (*OR3*) by (Blast_tac 1); diff -r c58423c20740 -r cbb6c0c1c58a src/HOL/Auth/OtwayRees_Bad.ML --- a/src/HOL/Auth/OtwayRees_Bad.ML Wed May 07 12:50:26 1997 +0200 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Wed May 07 13:01:43 1997 +0200 @@ -20,9 +20,11 @@ proof_timing:=true; HOL_quantifiers := false; -(*No need to declare Says_imp_sees_Spy' because "lost" is a CONSTANT*) +(*Replacing the variable by a constant improves search speed by 50%!*) +val Says_imp_sees_Spy' = + read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy; -(*Weak liveness: there are traces that reach the end*) +(*A "possibility property": there are traces that reach the end*) goal thy "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ \ ==> EX K. EX NA. EX evs: otway. \ @@ -49,12 +51,12 @@ goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \ \ X : analz (sees lost Spy evs)"; -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1); qed "OR2_analz_sees_Spy"; goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set_of_list evs ==> \ \ X : analz (sees lost Spy evs)"; -by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1); qed "OR4_analz_sees_Spy"; goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set_of_list evs \ @@ -72,21 +74,13 @@ bind_thm ("OR4_parts_sees_Spy", OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); -val parts_Fake_tac = +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) +val parts_induct_tac = + etac otway.induct 1 THEN forward_tac [OR2_parts_sees_Spy] 4 THEN forward_tac [OR4_parts_sees_Spy] 6 THEN - forward_tac [Oops_parts_sees_Spy] 7; - -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) -fun parts_induct_tac i = SELECT_GOAL - (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 2)) THEN - (*Base case*) - fast_tac (!claset addss (!simpset)) 1 THEN - ALLGOALS Asm_simp_tac) i; + forward_tac [Oops_parts_sees_Spy] 7 THEN + prove_simple_subgoals_tac 1; (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY @@ -96,8 +90,9 @@ goal thy "!!evs. evs : otway \ \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; -by (parts_induct_tac 1); -by (Auto_tac()); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -120,7 +115,7 @@ (*Nobody can have used non-existent keys!*) goal thy "!!evs. evs : otway ==> \ \ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; -by (parts_induct_tac 1); +by parts_induct_tac; (*Fake*) by (best_tac (!claset addIs [impOfSubs analz_subset_parts] @@ -128,7 +123,7 @@ impOfSubs (parts_insert_subset_Un RS keysFor_mono)] unsafe_addss (!simpset)) 1); (*OR1-3*) -by (REPEAT (fast_tac (!claset addss (!simpset)) 1)); +by (ALLGOALS Blast_tac); qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", @@ -150,12 +145,13 @@ \ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; by (etac rev_mp 1); by (etac otway.induct 1); -by (ALLGOALS (fast_tac (!claset addss (!simpset)))); +by (prove_simple_subgoals_tac 1); +by (Blast_tac 1); qed "Says_Server_message_form"; (*For proofs involving analz.*) -val analz_Fake_tac = +val analz_sees_tac = dtac OR2_analz_sees_Spy 4 THEN dtac OR4_analz_sees_Spy 6 THEN forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN @@ -181,12 +177,12 @@ \ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ \ (K : KK | Key K : analz (sees lost Spy evs))"; by (etac otway.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); (*Base*) -by (blast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); +by (Blast_tac 1); (*Fake, OR2, OR4*) by (REPEAT (spy_analz_tac 1)); qed_spec_mp "analz_image_freshK"; @@ -217,8 +213,7 @@ by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); (*...we assume X is a recent message, and handle this case by contradiction*) by (blast_tac (!claset addSEs sees_Spy_partsEs - delrules [conjI] (*prevent split-up into 4 subgoals*) - addss (!simpset addsimps [parts_insertI])) 1); + delrules [conjI] (*no split-up to 4 subgoals*)) 1); val lemma = result(); goal thy @@ -240,7 +235,7 @@ \ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \ \ Key K ~: analz (sees lost Spy evs)"; by (etac otway.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong] addsimps [not_parts_not_analz, analz_insert_freshK] @@ -280,7 +275,8 @@ \ Says A B {|NA, Agent A, Agent B, \ \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ \ : set_of_list evs"; -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); by (Blast_tac 1); qed_spec_mp "Crypt_imp_OR1"; @@ -300,7 +296,8 @@ \ Crypt (shrK A) {|NA, Key K|}, \ \ Crypt (shrK B) {|NB, Key K|}|} \ \ : set_of_list evs)"; -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); (*OR1: it cannot be a new Nonce, contradiction.*) by (blast_tac (!claset addSIs [parts_insertI] addSEs sees_Spy_partsEs) 1); diff -r c58423c20740 -r cbb6c0c1c58a src/HOL/Auth/Public.ML --- a/src/HOL/Auth/Public.ML Wed May 07 12:50:26 1997 +0200 +++ b/src/HOL/Auth/Public.ML Wed May 07 13:01:43 1997 +0200 @@ -80,7 +80,7 @@ (*Added for Yahalom/lost_tac*) goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs); A: lost |] \ \ ==> X : analz (sees lost Spy evs)"; -by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1); +by (blast_tac (!claset addSDs [analz.Decrypt]) 1); qed "Crypt_Spy_analz_lost"; (** Specialized rewrite rules for (sees lost A (Says...#evs)) **) @@ -120,8 +120,8 @@ by (Step_tac 1); by (etac rev_mp 1); (*split_tac does not work on assumptions*) by (ALLGOALS - (fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons] - setloop split_tac [expand_if])))); + (fast_tac (!claset unsafe_addss (!simpset addsimps [parts_Un, sees_Cons] + setloop split_tac [expand_if])))); qed "UN_parts_sees_Says"; goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs"; @@ -136,16 +136,14 @@ goal thy "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs; C : lost |] \ \ ==> X : analz (sees lost Spy evs)"; -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] - addss (!simpset)) 1); +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); qed "Says_Crypt_lost"; goal thy "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs; \ \ X ~: analz (sees lost Spy evs) |] \ \ ==> C ~: lost"; -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] - addss (!simpset)) 1); +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); qed "Says_Crypt_not_lost"; Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy]; diff -r c58423c20740 -r cbb6c0c1c58a src/HOL/Auth/ROOT.ML --- a/src/HOL/Auth/ROOT.ML Wed May 07 12:50:26 1997 +0200 +++ b/src/HOL/Auth/ROOT.ML Wed May 07 13:01:43 1997 +0200 @@ -12,6 +12,9 @@ proof_timing := true; goals_limit := 1; +(*New version of addss isn't ready--too slow*) +val op addss = op unsafe_addss; + (*Shared-key protocols*) time_use_thy "NS_Shared"; time_use_thy "OtwayRees"; diff -r c58423c20740 -r cbb6c0c1c58a src/HOL/Auth/Recur.ML --- a/src/HOL/Auth/Recur.ML Wed May 07 12:50:26 1997 +0200 +++ b/src/HOL/Auth/Recur.ML Wed May 07 13:01:43 1997 +0200 @@ -82,7 +82,7 @@ by (rtac subsetI 1); by (etac recur.induct 1); by (REPEAT_FIRST - (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono) + (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono) :: recur.intrs)))); qed "recur_mono"; @@ -128,7 +128,7 @@ goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set_of_list evs \ \ ==> RA : analz (sees lost Spy evs)"; -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); qed "RA4_analz_sees_Spy"; (*RA2_analz... and RA4_analz... let us treat those cases using the same @@ -141,26 +141,19 @@ bind_thm ("RA4_parts_sees_Spy", RA4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); -(*We instantiate the variable to "lost". Leaving it as a Var makes proofs - harder to complete, since simplification does less for us.*) -val parts_Fake_tac = +(*For proving the easier theorems about X ~: parts (sees lost Spy evs). + We instantiate the variable to "lost" since leaving it as a Var would + interfere with simplification.*) +val parts_induct_tac = let val tac = forw_inst_tac [("lost","lost")] - in tac RA2_parts_sees_Spy 4 THEN + in etac recur.induct 1 THEN + tac RA2_parts_sees_Spy 4 THEN etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN forward_tac [respond_imp_responses] 5 THEN - tac RA4_parts_sees_Spy 6 + tac RA4_parts_sees_Spy 6 THEN + prove_simple_subgoals_tac 1 end; -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) -fun parts_induct_tac i = SELECT_GOAL - (DETERM (etac recur.induct 1 THEN parts_Fake_tac THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - unsafe_addss (!simpset)) 2)) THEN - (*Base case*) - fast_tac (!claset unsafe_addss (!simpset)) 1 THEN - ALLGOALS Asm_simp_tac) i; (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY sends messages containing X! **) @@ -171,14 +164,14 @@ goal thy "!!evs. evs : recur lost \ \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; -by (parts_induct_tac 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees]))); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); +by (ALLGOALS + (asm_simp_tac (!simpset addsimps [parts_insert2, parts_insert_sees]))); (*RA3*) -by (fast_tac (!claset addDs [Key_in_parts_respond] - addss (!simpset addsimps [parts_insert_sees])) 2); +by (blast_tac (!claset addDs [Key_in_parts_respond]) 2); (*RA2*) -by (best_tac (!claset addSEs partsEs addSDs [parts_cut] - unsafe_addss (!simpset)) 1); +by (blast_tac (!claset addSEs partsEs addDs [parts_cut]) 1); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -191,7 +184,7 @@ goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ \ evs : recur lost |] ==> A:lost"; -by (fast_tac (!claset addDs [Spy_see_shrK]) 1); +by (blast_tac (!claset addDs [Spy_see_shrK]) 1); qed "Spy_see_shrK_D"; bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); @@ -212,10 +205,10 @@ goal thy "!!evs. evs : recur lost ==> \ \ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; -by (parts_induct_tac 1); +by parts_induct_tac; (*RA3*) by (best_tac (!claset addDs [Key_in_keysFor_parts] - unsafe_addss (!simpset addsimps [parts_insert_sees])) 2); + unsafe_addss (!simpset addsimps [parts_insert_sees])) 2); (*Fake*) by (best_tac (!claset addIs [impOfSubs analz_subset_parts] @@ -236,7 +229,7 @@ (*** Proofs involving analz ***) (*For proofs involving analz. We again instantiate the variable to "lost".*) -val analz_Fake_tac = +val analz_sees_tac = etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN dres_inst_tac [("lost","lost")] RA2_analz_sees_Spy 4 THEN forward_tac [respond_imp_responses] 5 THEN @@ -267,14 +260,14 @@ \ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ \ (K : KK | Key K : analz (sees lost Spy evs))"; by (etac recur.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); by (ALLGOALS (asm_simp_tac (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); (*Base*) -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); +by (Blast_tac 1); (*RA4, RA2, Fake*) by (REPEAT (spy_analz_tac 1)); val raw_analz_image_freshK = result(); @@ -304,17 +297,13 @@ \ evs : recur lost; A ~: lost |] \ \ ==> X : parts (sees lost Spy evs)"; by (etac rev_mp 1); -by (etac recur.induct 1); -by parts_Fake_tac; +by parts_induct_tac; (*RA3 requires a further induction*) -by (etac responses.induct 5); +by (etac responses.induct 2); by (ALLGOALS Asm_simp_tac); (*Fake*) -by (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset addsimps [parts_insert_sees])) 2); -(*Two others*) -by (REPEAT (fast_tac (!claset addss (!simpset)) 1)); +by (simp_tac (!simpset addsimps [parts_insert_sees]) 1); +by (Fake_parts_insert_tac 1); qed "Hash_imp_body"; @@ -329,14 +318,15 @@ \ ==> EX B' P'. ALL B P. \ \ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (sees lost Spy evs) \ \ --> B=B' & P=P'"; -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); by (etac responses.induct 3); by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib]))); by (step_tac (!claset addSEs partsEs) 1); (*RA1,2: creation of new Nonce. Move assertion into global context*) by (ALLGOALS (expand_case_tac "NA = ?y")); by (REPEAT_FIRST (ares_tac [exI])); -by (REPEAT (best_tac (!claset addSDs [Hash_imp_body] +by (REPEAT (blast_tac (!claset addSDs [Hash_imp_body] addSEs sees_Spy_partsEs) 1)); val lemma = result(); @@ -379,7 +369,7 @@ (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); (*Simplification using two distinct treatments of "image"*) by (simp_tac (!simpset addsimps [parts_insert2]) 1); -by (fast_tac (!claset delrules [allE]) 1); +by (blast_tac (!claset delrules [allE]) 1); qed "resp_analz_insert_lemma"; bind_thm ("resp_analz_insert", @@ -417,11 +407,11 @@ by (etac respond.induct 1); by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib]))); (*Base case*) -by (Fast_tac 1); +by (Blast_tac 1); by (Step_tac 1); by (expand_case_tac "K = KBC" 1); by (dtac respond_Key_in_parts 1); -by (best_tac (!claset addSIs [exI] +by (blast_tac (!claset addSIs [exI] addSEs partsEs addDs [Key_in_parts_respond]) 1); by (expand_case_tac "K = KAB" 1); @@ -457,19 +447,18 @@ (analz_image_freshK_ss addsimps [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2]))); by (ALLGOALS Simp_tac); -by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1); +by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1); by (step_tac (!claset addSEs [MPair_parts]) 1); (** LEVEL 7 **) -by (fast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond] +by (blast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond] addDs [impOfSubs analz_subset_parts]) 4); -by (fast_tac (!claset addSDs [respond_certificate]) 3); -by (best_tac (!claset addSEs partsEs - addDs [Key_in_parts_respond] - addss (!simpset)) 2); +by (blast_tac (!claset addSDs [respond_certificate]) 3); +by (blast_tac (!claset addSEs partsEs + addDs [Key_in_parts_respond]) 2); by (dtac unique_session_keys 1); by (etac respond_certificate 1); by (assume_tac 1); -by (Fast_tac 1); +by (Blast_tac 1); qed_spec_mp "respond_Spy_not_see_session_key"; @@ -480,7 +469,7 @@ \ ==> Key K ~: analz (sees lost Spy evs)"; by (etac rev_mp 1); by (etac recur.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees, analz_insert_freshK] @@ -492,17 +481,16 @@ (*Fake*) by (spy_analz_tac 2); (*Base*) -by (fast_tac (!claset addss (!simpset)) 1); +by (Blast_tac 1); (*RA3 remains*) by (step_tac (!claset delrules [impCE]) 1); (*RA3, case 2: K is an old key*) -by (best_tac (!claset addSDs [resp_analz_insert] - addSEs partsEs - addDs [Key_in_parts_respond] - addss (!simpset)) 2); +by (blast_tac (!claset addSDs [resp_analz_insert] + addSEs partsEs + addDs [Key_in_parts_respond]) 2); (*RA3, case 1: use lemma previously proved by induction*) -by (fast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN - (2,rev_notE)]) 1); +by (blast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN + (2,rev_notE)]) 1); qed "Spy_not_see_session_key"; @@ -516,8 +504,8 @@ by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); by (FIRSTGOAL (rtac Spy_not_see_session_key)); by (REPEAT_FIRST - (deepen_tac - (!claset addIs (map impOfSubs [recur_mono, parts_mono, sees_mono])) 0)); + (blast_tac + (!claset addIs (map impOfSubs [recur_mono, parts_mono, sees_mono])))); qed "Agent_not_see_session_key"; @@ -544,9 +532,10 @@ \ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \ \ : set_of_list evs"; by (etac rev_mp 1); -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); (*RA3*) -by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 1); +by (blast_tac (!claset addSDs [Hash_in_parts_respond]) 1); qed_spec_mp "Hash_auth_sender"; (** These two results subsume (for all agents) the guarantees proved @@ -561,18 +550,15 @@ \ ==> EX C RC. Says Server C RC : set_of_list evs & \ \ Crypt (shrK A) Y : parts {RC}"; by (etac rev_mp 1); -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); (*RA4*) -by (Fast_tac 4); +by (Blast_tac 4); (*RA3*) by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 3 - THEN Fast_tac 3); + THEN Blast_tac 3); (*RA1*) -by (Fast_tac 1); +by (Blast_tac 1); (*RA2: it cannot be a new Nonce, contradiction.*) -by (deepen_tac (!claset delrules [impCE] - addSIs [disjI2] - addSEs [MPair_parts] - addDs [parts.Body] - unsafe_addss (!simpset)) 0 1); +by (Blast_tac 1); qed "Cert_imp_Server_msg"; diff -r c58423c20740 -r cbb6c0c1c58a src/HOL/Auth/Shared.ML --- a/src/HOL/Auth/Shared.ML Wed May 07 12:50:26 1997 +0200 +++ b/src/HOL/Auth/Shared.ML Wed May 07 13:01:43 1997 +0200 @@ -56,7 +56,7 @@ goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}"; by (agent.induct_tac "C" 1); -by (auto_tac (!claset addIs [range_eqI], !simpset)); +by (Auto_tac ()); qed "keysFor_parts_initState"; Addsimps [keysFor_parts_initState]; @@ -210,14 +210,14 @@ (** Fresh keys never clash with long-term shared keys **) goal thy "Key (shrK A) : used evs"; -by (Best_tac 1); +by (Blast_tac 1); qed "shrK_in_used"; AddIffs [shrK_in_used]; -(*Used in parts_Fake_tac and analz_Fake_tac to distinguish session keys +(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys from long-term shared keys*) goal thy "!!K. Key K ~: used evs ==> K ~: range shrK"; -by (Best_tac 1); +by (Blast_tac 1); qed "Key_not_used"; (*A session key cannot clash with a long-term shared key*) @@ -237,7 +237,7 @@ by (list.induct_tac "l" 1); by (event.induct_tac "a" 2); by (ALLGOALS Asm_simp_tac); -by (Best_tac 1); +by (Blast_tac 1); qed "used_nil_subset"; goal thy "used l <= used (l@l')"; @@ -245,7 +245,7 @@ by (simp_tac (!simpset addsimps [used_nil_subset]) 1); by (event.induct_tac "a" 1); by (Asm_simp_tac 1); -by (Best_tac 1); +by (Blast_tac 1); qed "used_subset_append"; @@ -372,8 +372,8 @@ goal thy "sees lost A evs <= initState lost A Un sees lost Spy evs"; by (list.induct_tac "evs" 1); by (event.induct_tac "a" 2); -by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] - addss (!simpset)))); +by (ALLGOALS Asm_simp_tac); +by (ALLGOALS (blast_tac (!claset addDs [sees_Says_subset_insert RS subsetD]))); qed "sees_agent_subset_sees_Spy"; (*The Spy can see more than anybody else who's lost their key!*) @@ -381,7 +381,8 @@ by (list.induct_tac "evs" 1); by (event.induct_tac "a" 2); by (agent.induct_tac "A" 1); -by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset))); +by (ALLGOALS Asm_simp_tac); +by (ALLGOALS (blast_tac (!claset addDs [sees_Says_subset_insert RS subsetD]))); qed_spec_mp "sees_lost_agent_subset_sees_Spy"; diff -r c58423c20740 -r cbb6c0c1c58a src/HOL/Auth/WooLam.ML --- a/src/HOL/Auth/WooLam.ML Wed May 07 12:50:26 1997 +0200 +++ b/src/HOL/Auth/WooLam.ML Wed May 07 13:01:43 1997 +0200 @@ -28,8 +28,7 @@ woolam.WL4 RS woolam.WL5) 2); by (ALLGOALS (simp_tac (!simpset setSolver safe_solver))); by (REPEAT_FIRST (resolve_tac [refl, conjI])); -by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE] - addss (!simpset setSolver safe_solver)))); +by (REPEAT_FIRST (blast_tac (!claset addSEs [Nonce_supply RS notE]))); result(); @@ -54,18 +53,12 @@ bind_thm ("WL4_parts_sees_Spy", WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); -val parts_Fake_tac = forward_tac [WL4_parts_sees_Spy] 6; +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) +val parts_induct_tac = + etac woolam.induct 1 THEN + forward_tac [WL4_parts_sees_Spy] 6 THEN + prove_simple_subgoals_tac 1; -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) -fun parts_induct_tac i = SELECT_GOAL - (DETERM (etac woolam.induct 1 THEN parts_Fake_tac THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 2)) THEN - (*Base case*) - fast_tac (!claset addss (!simpset)) 1 THEN - ALLGOALS Asm_simp_tac) i; (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY sends messages containing X! **) @@ -74,8 +67,8 @@ goal thy "!!evs. evs : woolam \ \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; -by (parts_induct_tac 1); -by (Auto_tac()); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -88,7 +81,7 @@ goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ \ evs : woolam |] ==> A:lost"; -by (fast_tac (!claset addDs [Spy_see_shrK]) 1); +by (blast_tac (!claset addDs [Spy_see_shrK]) 1); qed "Spy_see_shrK_D"; bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); @@ -105,8 +98,9 @@ "!!evs. [| A ~: lost; evs : woolam |] \ \ ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) \ \ --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs)"; -by (parts_induct_tac 1); -by (Fast_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed_spec_mp "NB_Crypt_imp_Alice_msg"; (*Guarantee for Server: if it gets a message containing a certificate from @@ -117,7 +111,7 @@ \ Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \ \ : set_of_list evs |] \ \ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs"; -by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg] +by (blast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg] addSEs [MPair_parts] addDs [Says_imp_sees_Spy RS parts.Inj]) 1); qed "Server_trusts_WL4"; @@ -131,8 +125,9 @@ \ Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs \ \ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \ \ : set_of_list evs)"; -by (parts_induct_tac 1); -by (ALLGOALS Fast_tac); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); +by (ALLGOALS Blast_tac); bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp)); @@ -141,7 +136,8 @@ "!!evs. [| B ~: lost; evs : woolam |] \ \ ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs) \ \ --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs"; -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); qed_spec_mp "NB_Crypt_imp_Server_msg"; (*Partial guarantee for B: if it gets a message of correct form then the Server @@ -150,7 +146,7 @@ "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs; \ \ B ~: lost; evs : woolam |] \ \ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs"; -by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] +by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] addDs [Says_imp_sees_Spy RS parts.Inj]) 1); qed "B_got_WL5"; @@ -162,7 +158,7 @@ "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \ \ A ~: lost; B ~: lost; evs : woolam |] \ \ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs"; -by (fast_tac (!claset addIs [Server_trusts_WL4] +by (blast_tac (!claset addIs [Server_trusts_WL4] addSDs [B_got_WL5 RS Server_sent_WL5]) 1); qed "B_trusts_WL5"; @@ -172,8 +168,9 @@ "!!evs. [| B ~= Spy; evs : woolam |] \ \ ==> Says B A (Nonce NB) : set_of_list evs \ \ --> (EX A'. Says A' B (Agent A) : set_of_list evs)"; -by (parts_induct_tac 1); -by (ALLGOALS Fast_tac); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); +by (ALLGOALS Blast_tac); bind_thm ("B_said_WL2", result() RSN (2, rev_mp)); @@ -183,7 +180,8 @@ \ ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) & \ \ Says B A (Nonce NB) : set_of_list evs \ \ --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs"; -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); by (Step_tac 1); -by (best_tac (!claset addSEs partsEs) 1); +by (blast_tac (!claset addSEs partsEs) 1); **) diff -r c58423c20740 -r cbb6c0c1c58a src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Wed May 07 12:50:26 1997 +0200 +++ b/src/HOL/Auth/Yahalom.ML Wed May 07 13:01:43 1997 +0200 @@ -16,7 +16,8 @@ HOL_quantifiers := false; Pretty.setdepth 25; -val op addss = op unsafe_addss; +(*Replacing the variable by a constant improves speed*) +val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy; (*A "possibility property": there are traces that reach the end*) @@ -38,7 +39,7 @@ by (rtac subsetI 1); by (etac yahalom.induct 1); by (REPEAT_FIRST - (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono) + (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono) :: yahalom.intrs)))); qed "yahalom_mono"; @@ -57,7 +58,7 @@ (*Lets us treat YM4 using a similar argument as for the Fake case.*) goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set_of_list evs ==> \ \ X : analz (sees lost Spy evs)"; -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1); qed "YM4_analz_sees_Spy"; bind_thm ("YM4_parts_sees_Spy", @@ -67,26 +68,20 @@ goal thy "!!evs. Says S A {|Crypt (shrK A) {|B, K, NA, NB|}, X|} \ \ : set_of_list evs ==> \ \ K : parts (sees lost Spy evs)"; -by (fast_tac (!claset addSEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); +by (blast_tac (!claset addSEs partsEs + addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1); qed "YM4_Key_parts_sees_Spy"; -(*We instantiate the variable to "lost". Leaving it as a Var makes proofs - harder: the simplifier does less.*) -val parts_Fake_tac = - forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN - forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7; +(*For proving the easier theorems about X ~: parts (sees lost Spy evs). + We instantiate the variable to "lost" since leaving it as a Var would + interfere with simplification.*) +val parts_sees_tac = + forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN + forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN + prove_simple_subgoals_tac 1; -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) -fun parts_induct_tac i = SELECT_GOAL - (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 2)) THEN - (*Base case*) - fast_tac (!claset addss (!simpset)) 1 THEN - ALLGOALS Asm_simp_tac) i; +val parts_induct_tac = + etac yahalom.induct 1 THEN parts_sees_tac; (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY @@ -96,8 +91,9 @@ goal thy "!!evs. evs : yahalom lost \ \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; -by (parts_induct_tac 1); -by (Auto_tac()); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -110,7 +106,7 @@ goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ \ evs : yahalom lost |] ==> A:lost"; -by (fast_tac (!claset addDs [Spy_see_shrK]) 1); +by (blast_tac (!claset addDs [Spy_see_shrK]) 1); qed "Spy_see_shrK_D"; bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); @@ -120,11 +116,11 @@ (*Nobody can have used non-existent keys!*) goal thy "!!evs. evs : yahalom lost ==> \ \ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; -by (parts_induct_tac 1); +by parts_induct_tac; (*YM4: Key K is not fresh!*) -by (fast_tac (!claset addSEs sees_Spy_partsEs) 3); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 3); (*YM3*) -by (fast_tac (!claset addss (!simpset)) 2); +by (Blast_tac 2); (*Fake*) by (best_tac (!claset addIs [impOfSubs analz_subset_parts] @@ -149,12 +145,13 @@ \ ==> K ~: range shrK"; by (etac rev_mp 1); by (etac yahalom.induct 1); -by (ALLGOALS (fast_tac (!claset addss (!simpset)))); +by (ALLGOALS Asm_simp_tac); +by (Blast_tac 1); qed "Says_Server_message_form"; (*For proofs involving analz. We again instantiate the variable to "lost".*) -val analz_Fake_tac = +val analz_sees_tac = forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7); @@ -177,12 +174,12 @@ \ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ \ (K : KK | Key K : analz (sees lost Spy evs))"; by (etac yahalom.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); (*Base*) -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); +by (Blast_tac 1); (*YM4, Fake*) by (REPEAT (spy_analz_tac 1)); qed_spec_mp "analz_image_freshK"; @@ -207,14 +204,13 @@ by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); by (Step_tac 1); by (ex_strip_tac 2); -by (Fast_tac 2); +by (Blast_tac 2); (*Remaining case: YM3*) by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); (*...we assume X is a recent message and handle this case by contradiction*) -by (fast_tac (!claset addSEs sees_Spy_partsEs - delrules [conjI] (*prevent split-up into 4 subgoals*) - addss (!simpset addsimps [parts_insertI])) 1); +by (blast_tac (!claset addSEs sees_Spy_partsEs + delrules [conjI] (*no split-up to 4 subgoals*)) 1); val lemma = result(); goal thy @@ -240,7 +236,8 @@ \ Crypt (shrK B) {|Agent A, Key K|}|} \ \ : set_of_list evs"; by (etac rev_mp 1); -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); qed "A_trusts_YM3"; @@ -255,22 +252,19 @@ \ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs --> \ \ Key K ~: analz (sees lost Spy evs)"; by (etac yahalom.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (ALLGOALS (asm_simp_tac (!simpset addsimps [not_parts_not_analz, analz_insert_freshK] setloop split_tac [expand_if]))); (*YM3*) -by (fast_tac (!claset delrules [impCE] - addSEs sees_Spy_partsEs - addIs [impOfSubs analz_subset_parts] - addss (!simpset addsimps [parts_insert2])) 2); +by (blast_tac (!claset delrules [impCE] + addSEs sees_Spy_partsEs + addIs [impOfSubs analz_subset_parts]) 2); (*OR4, Fake*) by (REPEAT_FIRST spy_analz_tac); (*Oops*) -by (fast_tac (!claset delrules [disjE] - addDs [unique_session_keys] - addss (!simpset)) 1); +by (blast_tac (!claset addDs [unique_session_keys]) 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); @@ -284,7 +278,7 @@ \ A ~: lost; B ~: lost; evs : yahalom lost |] \ \ ==> Key K ~: analz (sees lost Spy evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); -by (fast_tac (!claset addSEs [lemma]) 1); +by (blast_tac (!claset addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; @@ -300,7 +294,7 @@ by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); -by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD]))); +by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD]))); qed "Agent_not_see_encrypted_key"; @@ -317,9 +311,10 @@ \ Crypt (shrK B) {|Agent A, Key K|}|} \ \ : set_of_list evs"; by (etac rev_mp 1); -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); (*YM3*) -by (Fast_tac 1); +by (Blast_tac 1); qed "B_trusts_YM4_shrK"; @@ -330,19 +325,15 @@ \ EX NA' A' B'. ALL NA A B. \ \ Crypt (shrK B) {|Agent A, Nonce NA, NB|} : parts(sees lost Spy evs) \ \ --> B ~: lost --> NA = NA' & A = A' & B = B'"; -by (etac yahalom.induct 1 THEN parts_Fake_tac); -(*Fake: the tactic in parts_induct_tac works, but takes 4 times longer*) -by (REPEAT (etac exE 2) THEN - best_tac (!claset addSIs [exI] - addDs [impOfSubs Fake_parts_insert] - addss (!simpset)) 2); -(*Base case*) -by (fast_tac (!claset addss (!simpset)) 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); +by parts_induct_tac; +(*Fake*) +by (REPEAT (etac (exI RSN (2,exE)) 1) (*stripping EXs makes proof faster*) + THEN Fake_parts_insert_tac 1); +by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); (*YM2: creation of new Nonce. Move assertion into global context*) by (expand_case_tac "NB = ?y" 1); by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1)); -by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); val lemma = result(); goal thy @@ -358,7 +349,7 @@ fun lost_tac s = case_tac ("(" ^ s ^ ") : lost") THEN' SELECT_GOAL - (REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN + (REPEAT_DETERM (dtac (Says_imp_sees_Spy' RS analz.Inj) 1) THEN REPEAT_DETERM (etac MPair_analz 1) THEN THEN_BEST_FIRST (dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1) @@ -376,31 +367,34 @@ \ evs : yahalom lost |] \ \ ==> NA' = NA & A' = A & B' = B"; by (lost_tac "B'" 1); -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj] - addSEs [MPair_parts] - addDs [unique_NB]) 1); +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addSEs [MPair_parts] + addDs [unique_NB]) 1); qed "Says_unique_NB"; +(*Induction for theorems of the form X ~: analz (sees lost Spy evs) --> ... + It simplifies the proof by discarding needless information about + analz (insert X (sees lost Spy evs)) +*) +val analz_mono_parts_induct_tac = + etac yahalom.induct 1 + THEN + REPEAT_FIRST + (rtac impI THEN' + dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN' + mp_tac) + THEN parts_sees_tac; + goal thy "!!evs. [| B ~: lost; evs : yahalom lost |] \ -\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \ -\ Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} : parts (sees lost Spy evs) \ -\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts (sees lost Spy evs)"; -by (etac yahalom.induct 1); -by parts_Fake_tac; -by (REPEAT_FIRST - (rtac impI THEN' - dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN' - mp_tac)); -by (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 2); -by (ALLGOALS Asm_simp_tac); -by (fast_tac (!claset addss (!simpset)) 1); -by (fast_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj] - addSIs [parts_insertI] - addSEs partsEs - addss (!simpset)) 1); +\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \ +\ Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}: parts(sees lost Spy evs)\ +\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts(sees lost Spy evs)"; +by analz_mono_parts_induct_tac; +by (Fake_parts_insert_tac 1); +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj] + addSIs [parts_insertI] + addSEs partsEs) 1); val no_nonce_YM1_YM2 = standard (result() RS mp RSN (2, rev_mp) RS notE); @@ -419,23 +413,15 @@ \ Nonce NA, Nonce NB|}, \ \ Crypt (shrK B) {|Agent A, Key K|}|} \ \ : set_of_list evs)"; -by (etac yahalom.induct 1); -by parts_Fake_tac; -by (fast_tac (!claset addss (!simpset)) 1); -by (REPEAT_FIRST - (rtac impI THEN' - dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD))); -by (ALLGOALS Asm_simp_tac); -(*Fake, YM3, YM4*) -by (Fast_tac 2); -by (fast_tac (!claset addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 1); -(*YM4*) +by analz_mono_parts_induct_tac; +(*YM4 & Fake*) +by (Blast_tac 2); +by (Fake_parts_insert_tac 1); +(*YM3*) by (Step_tac 1); by (lost_tac "A" 1); -by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS - A_trusts_YM3]) 1); +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS + A_trusts_YM3]) 1); val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp); @@ -448,26 +434,19 @@ \ ==> Key K ~: analz (sees lost Spy evs) --> \ \ Crypt K (Nonce NB) : parts (sees lost Spy evs) --> \ \ (EX A B NA. Says Server A \ -\ {|Crypt (shrK A) {|Agent B, Key K, \ -\ Nonce NA, Nonce NB|}, \ +\ {|Crypt (shrK A) {|Agent B, Key K, \ +\ Nonce NA, Nonce NB|}, \ \ Crypt (shrK B) {|Agent A, Key K|}|} \ \ : set_of_list evs)"; -by (etac yahalom.induct 1); -by parts_Fake_tac; -by (fast_tac (!claset addss (!simpset)) 1); -by (TRYALL (rtac impI)); -by (REPEAT_FIRST - (dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD))); -by (ALLGOALS Asm_simp_tac); -(*Fake, YM3, YM4*) -by (fast_tac (!claset addSDs [Crypt_Fake_parts_insert] - addDs [impOfSubs analz_subset_parts]) 1); -by (Fast_tac 1); -(*YM4*) +by analz_mono_parts_induct_tac; +(*YM4 & Fake*) +by (Blast_tac 2); +by (Fake_parts_insert_tac 1); +(*YM3*) by (Step_tac 1); by (lost_tac "A" 1); -by (fast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS - A_trusts_YM3]) 1); +by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS + A_trusts_YM3]) 1); result() RS mp RSN (2, rev_mp); @@ -482,7 +461,7 @@ by (etac rev_mp 1); by (etac yahalom.induct 1); by (ALLGOALS Asm_simp_tac); -by (ALLGOALS Fast_tac); +by (ALLGOALS Blast_tac); qed "Says_Server_imp_YM2"; @@ -491,9 +470,9 @@ val no_nonce_tac = SELECT_GOAL (REPEAT (resolve_tac [impI, notI] 1) THEN REPEAT (hyp_subst_tac 1) THEN - etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS no_nonce_YM1_YM2) 1 + etac (Says_imp_sees_Spy' RS parts.Inj RS parts.Snd RS no_nonce_YM1_YM2) 1 THEN - etac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd) 4 + etac (Says_imp_sees_Spy' RS parts.Inj RS parts.Snd) 4 THEN REPEAT_FIRST assume_tac); @@ -509,30 +488,30 @@ goal thy "!!evs. P --> (X : analz (G Un H)) --> (X : analz H) ==> \ \ P --> (X : analz (G Un H)) = (X : analz H)"; -by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); +by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1); qed "Nonce_secrecy_lemma"; goal thy - "!!evs. evs : yahalom lost ==> \ + "!!evs. evs : yahalom lost ==> \ \ (ALL KK. KK <= Compl (range shrK) --> \ -\ (ALL K: KK. ALL A B na X. \ +\ (ALL K: KK. ALL A B na X. \ \ Says Server A \ \ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \ -\ ~: set_of_list evs) --> \ -\ (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) = \ +\ ~: set_of_list evs) --> \ +\ (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) = \ \ (Nonce NB : analz (sees lost Spy evs)))"; by (etac yahalom.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (REPEAT_FIRST (resolve_tac [impI RS allI])); by (REPEAT_FIRST (rtac Nonce_secrecy_lemma )); by (rtac ccontr 7); -by (subgoal_tac "ALL A B na X. \ +by (subgoal_tac "ALL A B na X. \ \ Says Server A \ \ {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \ \ ~: set_of_list evsa" 7); by (eres_inst_tac [("P","?PP-->?QQ")] notE 7); -by (subgoal_tac "ALL A B na X. \ -\ Says Server A \ +by (subgoal_tac "ALL A B na X. \ +\ Says Server A \ \ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \ \ ~: set_of_list evsa" 5); by (ALLGOALS (*22 seconds*) @@ -542,15 +521,14 @@ not_parts_not_analz, analz_image_freshK] @ pushes @ ball_simps)))); (*Base*) -by (fast_tac (!claset addss (!simpset)) 1); +by (Blast_tac 1); (*Fake*) (** LEVEL 10 **) by (spy_analz_tac 1); (*YM3*) -by (fast_tac (!claset addSEs sees_Spy_partsEs) 1); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); (*Oops*) -(*20 secs*) -by (fast_tac (!claset delrules [ballE] addDs [unique_session_keys] - addss (!simpset)) 2); +by (Asm_full_simp_tac 2); +by (blast_tac (!claset addDs [unique_session_keys]) 2); (*YM4*) (** LEVEL 13 **) by (REPEAT (resolve_tac [impI, allI] 1)); @@ -562,10 +540,10 @@ by (step_tac (!claset addSDs [not_analz_insert]) 1); by (lost_tac "A" 1); (** LEVEL 20 **) -by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1 +by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1 THEN REPEAT (assume_tac 1)); by (thin_tac "All ?PP" 1); -by (Fast_tac 1); +by (Blast_tac 1); qed_spec_mp "Nonce_secrecy"; @@ -581,8 +559,8 @@ \ KAB ~: range shrK; evs : yahalom lost |] \ \ ==> NB = NB'"; by (rtac ccontr 1); -by (subgoal_tac "ALL A B na X. \ -\ Says Server A \ +by (subgoal_tac "ALL A B na X. \ +\ Says Server A \ \ {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB|}, X|} \ \ ~: set_of_list evs" 1); by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1); @@ -592,6 +570,8 @@ qed "single_Nonce_secrecy"; +val Says_unique_NB' = read_instantiate [("lost","lost")] Says_unique_NB; + goal thy "!!evs. [| A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost |] \ \ ==> Says B Server \ @@ -600,55 +580,53 @@ \ (ALL k. Says A Spy {|Nonce NA, Nonce NB, k|} ~: set_of_list evs) --> \ \ Nonce NB ~: analz (sees lost Spy evs)"; by (etac yahalom.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (ALLGOALS (asm_simp_tac (!simpset addsimps ([not_parts_not_analz, analz_insert_freshK] @ pushes) setloop split_tac [expand_if]))); -by (fast_tac (!claset addSIs [parts_insertI] - addSEs sees_Spy_partsEs - addss (!simpset)) 2); +by (blast_tac (!claset addSIs [parts_insertI] + addSEs sees_Spy_partsEs) 2); (*Proof of YM2*) (** LEVEL 4 **) -by (deepen_tac (!claset addDs [Says_imp_sees_Spy RS analz.Inj, - impOfSubs analz_subset_parts] - addSEs partsEs) 3 2); +by (blast_tac (!claset addSEs partsEs + addDs [Says_imp_sees_Spy' RS analz.Inj, + impOfSubs analz_subset_parts]) 2); (*Prove YM3 by showing that no NB can also be an NA*) by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2)); -by (deepen_tac (!claset addDs [Says_unique_NB]) 1 2); +by (blast_tac (!claset addDs [Says_unique_NB']) 2 THEN flexflex_tac); (*Fake*) by (spy_analz_tac 1); (*YM4*) (** LEVEL 8 **) by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1); by (simp_tac (!simpset setloop split_tac [expand_if]) 1); -(*43 secs??*) +(* SLOW: 13s*) by (SELECT_GOAL (REPEAT_FIRST (spy_analz_tac ORELSE' Safe_step_tac)) 1); by (lost_tac "Aa" 1); -by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1); +by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1); by (forward_tac [Says_Server_message_form] 3); by (forward_tac [Says_Server_imp_YM2] 4); -(** LEVEL 15 **) -by (REPEAT_FIRST ((eresolve_tac [asm_rl, bexE, exE, disjE]))); +by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE])); +(** LEVEL 16 **) +(* use unique_NB to identify message components *) by (lost_tac "Ba" 1); -by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Snd RS unique_NB) 1); -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj] - addSEs [MPair_parts]) 1); -by (REPEAT (assume_tac 1 ORELSE Safe_step_tac 1)); +by (subgoal_tac "Aa=A & Ba=B & NAa=NA" 1); +by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addSEs [MPair_parts] addDs [unique_NB]) 2); +by (blast_tac (!claset addDs [Spy_not_see_encrypted_key, + impOfSubs Fake_analz_insert] + addIs [impOfSubs analz_mono]) 1); (** LEVEL 20 **) -by (dtac Spy_not_see_encrypted_key 1); -by (REPEAT (assume_tac 1 ORELSE Fast_tac 1)); -by (spy_analz_tac 1); -(*Oops case*) (** LEVEL 23 **) +(*Oops case*) by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1); by (step_tac (!claset delrules [disjE, conjI]) 1); by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1); by (expand_case_tac "NB = NBa" 1); -by (deepen_tac (!claset addDs [Says_unique_NB]) 1 1); +by (blast_tac (!claset addDs [Says_unique_NB']) 1); by (rtac conjI 1); by (no_nonce_tac 1); (** LEVEL 30 **) -by (thin_tac "?PP|?QQ" 1); (*subsumption!*) -by (fast_tac (!claset addSDs [single_Nonce_secrecy]) 1); +by (blast_tac (!claset addSDs [single_Nonce_secrecy]) 1); val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) |> standard; @@ -671,11 +649,11 @@ \ Crypt (shrK B) {|Agent A, Key K|}|} \ \ : set_of_list evs"; by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); -by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN +by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1 THEN dtac B_trusts_YM4_shrK 1); by (dtac B_trusts_YM4_newK 3); by (REPEAT_FIRST (eresolve_tac [asm_rl, exE])); by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1); by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1)); -by (deepen_tac (!claset addDs [Says_unique_NB] addss (!simpset)) 0 1); +by (blast_tac (!claset addDs [Says_unique_NB']) 1); qed "B_trusts_YM4"; diff -r c58423c20740 -r cbb6c0c1c58a src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Wed May 07 12:50:26 1997 +0200 +++ b/src/HOL/Auth/Yahalom2.ML Wed May 07 13:01:43 1997 +0200 @@ -17,8 +17,6 @@ proof_timing:=true; HOL_quantifiers := false; -val op addss = op unsafe_addss; - (*A "possibility property": there are traces that reach the end*) goal thy "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ @@ -38,7 +36,7 @@ by (rtac subsetI 1); by (etac yahalom.induct 1); by (REPEAT_FIRST - (best_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono) + (blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono) :: yahalom.intrs)))); qed "yahalom_mono"; @@ -57,7 +55,7 @@ (*Lets us treat YM4 using a similar argument as for the Fake case.*) goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set_of_list evs ==> \ \ X : analz (sees lost Spy evs)"; -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); +by (blast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); qed "YM4_analz_sees_Spy"; bind_thm ("YM4_parts_sees_Spy", @@ -67,26 +65,18 @@ goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B, K, NA|}, X|} \ \ : set_of_list evs ==> \ \ K : parts (sees lost Spy evs)"; -by (fast_tac (!claset addSEs partsEs +by (blast_tac (!claset addSEs partsEs addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); qed "YM4_Key_parts_sees_Spy"; -(*We instantiate the variable to "lost". Leaving it as a Var makes proofs - harder: the simplifier does less.*) -val parts_Fake_tac = - forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN - forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7; - -(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) -fun parts_induct_tac i = SELECT_GOAL - (DETERM (etac yahalom.induct 1 THEN parts_Fake_tac THEN - (*Fake message*) - TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert] - addss (!simpset)) 2)) THEN - (*Base case*) - fast_tac (!claset addss (!simpset)) 1 THEN - ALLGOALS Asm_simp_tac) i; +(*For proving the easier theorems about X ~: parts (sees lost Spy evs). + We instantiate the variable to "lost" since leaving it as a Var would + interfere with simplification.*) +val parts_induct_tac = + etac yahalom.induct 1 THEN + forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN + forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN + prove_simple_subgoals_tac 1; (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY @@ -96,8 +86,9 @@ goal thy "!!evs. evs : yahalom lost \ \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; -by (parts_induct_tac 1); -by (Auto_tac()); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -110,7 +101,7 @@ goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ \ evs : yahalom lost |] ==> A:lost"; -by (fast_tac (!claset addDs [Spy_see_shrK]) 1); +by (blast_tac (!claset addDs [Spy_see_shrK]) 1); qed "Spy_see_shrK_D"; bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); @@ -120,11 +111,11 @@ (*Nobody can have used non-existent keys!*) goal thy "!!evs. evs : yahalom lost ==> \ \ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))"; -by (parts_induct_tac 1); +by parts_induct_tac; (*YM4: Key K is not fresh!*) -by (fast_tac (!claset addSEs sees_Spy_partsEs) 3); +by (blast_tac (!claset addSEs sees_Spy_partsEs) 3); (*YM3*) -by (fast_tac (!claset addss (!simpset)) 2); +by (blast_tac (!claset addss (!simpset)) 2); (*Fake*) by (best_tac (!claset addIs [impOfSubs analz_subset_parts] @@ -149,12 +140,12 @@ \ ==> K ~: range shrK & A ~= B"; by (etac rev_mp 1); by (etac yahalom.induct 1); -by (ALLGOALS (fast_tac (!claset addss (!simpset)))); +by (ALLGOALS Asm_simp_tac); qed "Says_Server_message_form"; (*For proofs involving analz. We again instantiate the variable to "lost".*) -val analz_Fake_tac = +val analz_sees_tac = dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN assume_tac 7 THEN @@ -179,12 +170,12 @@ \ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ \ (K : KK | Key K : analz (sees lost Spy evs))"; by (etac yahalom.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); (*Base*) -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); +by (blast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); (*YM4, Fake*) by (REPEAT (spy_analz_tac 1)); qed_spec_mp "analz_image_freshK"; @@ -212,7 +203,7 @@ by (expand_case_tac "K = ?y" 1); by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); (*...we assume X is a recent message and handle this case by contradiction*) -by (fast_tac (!claset addSEs sees_Spy_partsEs +by (blast_tac (!claset addSEs sees_Spy_partsEs delrules [conjI] (*prevent split-up into 4 subgoals*) addss (!simpset addsimps [parts_insertI])) 1); val lemma = result(); @@ -234,30 +225,28 @@ goal thy "!!evs. [| A ~: lost; B ~: lost; A ~= B; \ -\ evs : yahalom lost |] \ +\ evs : yahalom lost |] \ \ ==> Says Server A \ -\ {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, \ -\ Crypt (shrK B) {|NB, Key K, Agent A|}|} \ -\ : set_of_list evs --> \ -\ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs --> \ +\ {|NB, Crypt (shrK A) {|Agent B, Key K, NA|}, \ +\ Crypt (shrK B) {|NB, Key K, Agent A|}|} \ +\ : set_of_list evs --> \ +\ Says A Spy {|NA, NB, Key K|} ~: set_of_list evs --> \ \ Key K ~: analz (sees lost Spy evs)"; by (etac yahalom.induct 1); -by analz_Fake_tac; +by analz_sees_tac; by (ALLGOALS (asm_simp_tac (!simpset addsimps [not_parts_not_analz, analz_insert_freshK] setloop split_tac [expand_if]))); (*YM3*) -by (fast_tac (!claset delrules [impCE] +by (blast_tac (!claset delrules [impCE] addSEs sees_Spy_partsEs addIs [impOfSubs analz_subset_parts] addss (!simpset addsimps [parts_insert2])) 2); (*OR4, Fake*) by (REPEAT_FIRST spy_analz_tac); (*Oops*) -by (fast_tac (!claset delrules [disjE] - addDs [unique_session_keys] - addss (!simpset)) 1); +by (blast_tac (!claset addDs [unique_session_keys]) 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); @@ -271,7 +260,7 @@ \ A ~: lost; B ~: lost; evs : yahalom lost |] \ \ ==> Key K ~: analz (sees lost Spy evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); -by (fast_tac (!claset addSEs [lemma]) 1); +by (blast_tac (!claset addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; @@ -287,7 +276,7 @@ by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); -by (REPEAT_FIRST (fast_tac (!claset addIs [yahalom_mono RS subsetD]))); +by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD]))); qed "Agent_not_see_encrypted_key"; @@ -303,9 +292,9 @@ \ Crypt (shrK B) {|NB, Key K, Agent A|}|} \ \ : set_of_list evs"; by (etac rev_mp 1); -by (parts_induct_tac 1); -(*The nested conjunctions are entirely useless*) -by (REPEAT_FIRST (rtac conjI ORELSE' fast_tac (!claset delrules [conjI]))); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed "A_trusts_YM3"; @@ -321,9 +310,10 @@ \ Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \ \ : set_of_list evs"; by (etac rev_mp 1); -by (parts_induct_tac 1); +by parts_induct_tac; +by (Fake_parts_insert_tac 1); (*YM3*) -by (Fast_tac 1); +by (Blast_tac 1); qed "B_trusts_YM4_shrK"; (*With this variant we don't bother to use the 2nd part of YM4 at all, since @@ -342,5 +332,5 @@ \ Crypt (shrK B) {|Nonce NB, Key K, Agent A|}|} \ \ : set_of_list evs"; by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1); -by (fast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1); +by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1); qed "B_trusts_YM4";