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