# HG changeset patch # User paulson # Date 882873828 -3600 # Node ID af3239def3d4241a2ca3c1e37f5841e34f1f3feb # Parent 399868bf8444451d83f9ddd68273e5de7d98c449 Tidied using more default rules diff -r 399868bf8444 -r af3239def3d4 src/HOL/Auth/NS_Public.ML --- a/src/HOL/Auth/NS_Public.ML Tue Dec 23 11:41:12 1997 +0100 +++ b/src/HOL/Auth/NS_Public.ML Tue Dec 23 11:43:48 1997 +0100 @@ -5,6 +5,9 @@ Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. Version incorporating Lowe's fix (inclusion of B's identify in round 2). + +This version is experimental. It adds many more rules to the claset and even +replaces Fake_parts_insert_tac by Blast_tac. *) open NS_Public; @@ -12,6 +15,10 @@ set proof_timing; HOL_quantifiers := false; +AddEs spies_partsEs; +AddDs [impOfSubs analz_subset_parts]; +AddDs [impOfSubs Fake_parts_insert]; + AddIffs [Spy_in_bad]; (*A "possibility property": there are traces that reach the end*) @@ -53,27 +60,18 @@ goal thy "!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed "Spy_see_priK"; Addsimps [Spy_see_priK]; -AddDs [impOfSubs analz_subset_parts]; -AddDs [Says_imp_spies RS parts.Inj]; -AddDs [impOfSubs Fake_parts_insert]; - goal thy "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; by (Auto_tac()); qed "Spy_analz_priK"; Addsimps [Spy_analz_priK]; -goal thy "!!A. [| Key (priK A) : parts (spies evs); \ -\ evs : ns_public |] ==> A:bad"; -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); -AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; +AddSDs [Spy_see_priK RSN (2, rev_iffD1), + Spy_analz_priK RSN (2, rev_iffD1)]; (**** Authenticity properties obtained from NS2 ****) @@ -88,13 +86,12 @@ by (etac rev_mp 1); by (etac rev_mp 1); by (parts_induct_tac 1); -(*NS3*) -by (blast_tac (claset() addSEs partsEs) 3); -(*NS2*) -by (blast_tac (claset() addSEs partsEs) 2); -by (Fake_parts_insert_tac 1); +by (ALLGOALS Blast_tac); qed "no_nonce_NS1_NS2"; +(*Adding it to the claset slows down proofs...*) +val nonce_NS1_NS2_E = no_nonce_NS1_NS2 RSN (2, rev_notE); + (*Unicity for NS1: nonce NA identifies agents A and B*) goal thy @@ -105,13 +102,14 @@ by (etac rev_mp 1); by (parts_induct_tac 1); by (ALLGOALS - (asm_simp_tac (simpset() addsimps [all_conj_distrib, parts_insert_spies]))); + (asm_simp_tac (simpset() addsimps [all_conj_distrib, + parts_insert_spies]))); (*NS1*) -by (expand_case_tac "NA = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2); +by (expand_case_tac "NA = ?y" 2 THEN Blast_tac 2); (*Fake*) by (Clarify_tac 1); by (ex_strip_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); val lemma = result(); goal thy @@ -127,8 +125,7 @@ (*Tactic for proving secrecy theorems*) fun analz_induct_tac i = etac ns_public.induct i THEN - ALLGOALS (asm_simp_tac - (simpset() addsplits [expand_if])); + ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])); (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) @@ -139,12 +136,11 @@ by (etac rev_mp 1); by (analz_induct_tac 1); (*NS3*) -by (blast_tac (claset() addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); +by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 4); (*NS2*) -by (blast_tac (claset() addSEs [MPair_parts] - addDs [parts.Body, unique_NA]) 3); +by (blast_tac (claset() addDs [unique_NA]) 3); (*NS1*) -by (blast_tac (claset() addSEs spies_partsEs) 2); +by (Blast_tac 2); (*Fake*) by (spy_analz_tac 1); qed "Spy_not_see_NA"; @@ -165,7 +161,7 @@ by (etac ns_public.induct 1); by (ALLGOALS Asm_simp_tac); (*NS1*) -by (blast_tac (claset() addSEs spies_partsEs) 2); +by (Blast_tac 2); (*Fake*) by (blast_tac (claset() addDs [Spy_not_see_NA]) 1); qed "A_trusts_NS2"; @@ -179,7 +175,7 @@ by (etac rev_mp 1); by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed "B_trusts_NS1"; @@ -200,11 +196,11 @@ (asm_simp_tac (simpset() addsimps [all_conj_distrib, parts_insert_spies]))); (*NS2*) -by (expand_case_tac "NB = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2); +by (expand_case_tac "NB = ?y" 2 THEN Blast_tac 2); (*Fake*) by (Clarify_tac 1); by (ex_strip_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); val lemma = result(); goal thy @@ -218,6 +214,8 @@ by (prove_unique_tac lemma 1); qed "unique_NB"; +AddDs [unique_NB]; + (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*) goal thy @@ -228,12 +226,11 @@ by (etac rev_mp 1); by (analz_induct_tac 1); (*NS3*) -by (blast_tac (claset() addDs [unique_NB]) 4); +by (Blast_tac 4); (*NS2: by freshness and unicity of NB*) -by (blast_tac (claset() addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)] - addEs partsEs) 3); +by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3); (*NS1*) -by (blast_tac (claset() addSEs spies_partsEs) 2); +by (Blast_tac 2); (*Fake*) by (spy_analz_tac 1); qed "Spy_not_see_NB"; @@ -254,12 +251,7 @@ by (etac (Says_imp_spies RS parts.Inj RS rev_mp) 1); by (parts_induct_tac 1); by (ALLGOALS Clarify_tac); -(*NS3: because NB determines A*) -by (blast_tac (claset() addDs [unique_NB]) 3); -(*NS1: by freshness*) -by (blast_tac (claset() addSEs spies_partsEs) 2); -(*Fake*) -by (Blast_tac 1); +by (ALLGOALS Blast_tac); qed "B_trusts_NS3"; @@ -284,11 +276,7 @@ by (etac ns_public.induct 1); by (ALLGOALS Asm_simp_tac); by (ALLGOALS Clarify_tac); -(*NS3: because NB determines A and NA*) -by (blast_tac (claset() addDs [unique_NB]) 3); -(*NS1*) -by (blast_tac (claset() addSEs spies_partsEs) 2); -(*Fake*) -by (Blast_tac 1); +(*NS3 holds because NB determines A and NA*) +by (ALLGOALS Blast_tac); qed "B_trusts_protocol"; diff -r 399868bf8444 -r af3239def3d4 src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Tue Dec 23 11:41:12 1997 +0100 +++ b/src/HOL/Auth/NS_Shared.ML Tue Dec 23 11:43:48 1997 +0100 @@ -15,6 +15,10 @@ set proof_timing; HOL_quantifiers := false; +AddEs spies_partsEs; +AddDs [impOfSubs analz_subset_parts]; +AddDs [impOfSubs Fake_parts_insert]; + (*A "possibility property": there are traces that reach the end*) goal thy @@ -49,13 +53,13 @@ (*For reasoning about the encrypted portion of message NS3*) goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \ \ ==> X : parts (spies evs)"; -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); qed "NS3_msg_in_parts_spies"; goal thy "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \ \ ==> K : parts (spies evs)"; -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); qed "Oops_parts_spies"; (*For proving the easier theorems about X ~: parts (spies evs).*) @@ -74,24 +78,18 @@ goal thy "!!evs. evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; goal thy "!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; -by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); +by (Auto_tac()); qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; -goal thy "!!A. [| Key (shrK A) : parts (spies evs); \ -\ evs : ns_shared |] ==> A:bad"; -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); -AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; +AddSDs [Spy_see_shrK RSN (2, rev_iffD1), + Spy_analz_shrK RSN (2, rev_iffD1)]; (*Nobody can have used non-existent keys!*) @@ -105,7 +103,7 @@ addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] addss (simpset())) 1); (*NS2, NS4, NS5*) -by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs))); +by (ALLGOALS (Blast_tac)); qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", @@ -138,7 +136,7 @@ \ : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed "A_trusts_NS2"; @@ -162,7 +160,7 @@ by (case_tac "A : bad" 1); by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj] addss (simpset())) 1); -by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, cert_A_form]) 1); +by (blast_tac (claset() addSDs [cert_A_form]) 1); qed "Says_S_message_form"; @@ -191,7 +189,7 @@ \ (Crypt KAB X) : parts (spies evs) & \ \ Key K : parts {X} --> Key K : parts (spies evs)"; by (parts_induct_tac 1); -(*Deals with Faked messages*) +(*Fake*) by (blast_tac (claset() addSEs partsEs addDs [impOfSubs parts_insert_subset_Un]) 1); (*Base, NS4 and NS5*) @@ -242,8 +240,7 @@ (*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 (blast_tac (claset() delrules [conjI] (*prevent splitup into 4 subgoals*) - addSEs spies_partsEs) 1); +by (Blast_tac 1); val lemma = result(); (*In messages of this form, the session key uniquely identifies the rest*) @@ -278,9 +275,7 @@ (*NS3, replay sub-case*) by (Blast_tac 4); (*NS2*) -by (blast_tac (claset() addSEs spies_partsEs - addIs [parts_insertI, - impOfSubs analz_subset_parts]) 2); +by (Blast_tac 2); (*Fake*) by (spy_analz_tac 1); (*NS3, Server sub-case*) (**LEVEL 6 **) @@ -288,7 +283,7 @@ by (forward_tac [Says_imp_spies RS parts.Inj RS A_trusts_NS2] 1); by (assume_tac 2); by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS - Crypt_Spy_analz_bad]) 1); + Crypt_Spy_analz_bad]) 1); by (blast_tac (claset() addDs [unique_session_keys]) 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); @@ -320,8 +315,6 @@ \ : set evs"; by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -(*Fake case*) by (ALLGOALS Blast_tac); qed "B_trusts_NS3"; @@ -339,7 +332,7 @@ by (parts_induct_tac 1); (*NS3*) by (Blast_tac 3); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); (*NS2: contradiction from the assumptions Key K ~: used evs2 and Crypt K (Nonce NB) : parts (spies evs2) *) by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)] @@ -348,8 +341,7 @@ (*NS4*) by (Clarify_tac 1); by (not_bad_tac "Ba" 1); -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS B_trusts_NS3, - unique_session_keys]) 1); +by (blast_tac (claset() addDs [B_trusts_NS3, unique_session_keys]) 1); qed "A_trusts_NS4_lemma"; @@ -381,7 +373,7 @@ by (parts_induct_tac 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); by (ALLGOALS Clarify_tac); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); (**LEVEL 7**) (*NS2*) by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)] @@ -407,19 +399,18 @@ \ Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs"; by (parts_induct_tac 1); (*NS4*) -by (blast_tac (claset() addSEs spies_partsEs) 4); +by (Blast_tac 4); (*NS3*) -by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, cert_A_form]) 3); +by (blast_tac (claset() addSDs [cert_A_form]) 3); (*NS2*) by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)] addSDs [Crypt_imp_keysFor]) 2); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); (**LEVEL 5**) (*NS5*) by (Clarify_tac 1); by (not_bad_tac "Aa" 1); -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS A_trusts_NS2, - unique_session_keys]) 1); +by (blast_tac (claset() addDs [A_trusts_NS2, unique_session_keys]) 1); val lemma = result(); diff -r 399868bf8444 -r af3239def3d4 src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Tue Dec 23 11:41:12 1997 +0100 +++ b/src/HOL/Auth/OtwayRees.ML Tue Dec 23 11:43:48 1997 +0100 @@ -17,6 +17,10 @@ set proof_timing; HOL_quantifiers := false; +AddEs spies_partsEs; +AddDs [impOfSubs analz_subset_parts]; +AddDs [impOfSubs Fake_parts_insert]; + (*A "possibility property": there are traces that reach the end*) goal thy @@ -45,17 +49,19 @@ goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \ \ ==> X : analz (spies evs)"; -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); +bd (Says_imp_spies RS analz.Inj) 1; +by (Blast_tac 1); qed "OR2_analz_spies"; goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \ \ ==> X : analz (spies evs)"; -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); +bd (Says_imp_spies RS analz.Inj) 1; +by (Blast_tac 1); qed "OR4_analz_spies"; goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \ \ ==> K : parts (spies evs)"; -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); qed "Oops_parts_spies"; (*OR2_analz... and OR4_analz... let us treat those cases using the same @@ -85,7 +91,6 @@ goal thy "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -96,12 +101,8 @@ qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; -goal thy "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad"; -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); -AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; +AddSDs [Spy_see_shrK RSN (2, rev_iffD1), + Spy_analz_shrK RSN (2, rev_iffD1)]; (*Nobody can have used non-existent keys!*) @@ -111,9 +112,9 @@ (*Fake*) by (best_tac (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] - addIs [impOfSubs analz_subset_parts] - addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] - addss (simpset())) 1); + addIs [impOfSubs analz_subset_parts] + addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] + addss (simpset())) 1); by (ALLGOALS Blast_tac); qed_spec_mp "new_keys_not_used"; @@ -201,8 +202,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 (blast_tac (claset() addSEs spies_partsEs - delrules [conjI] (*no split-up into 4 subgoals*)) 1); +by (Blast_tac 1); val lemma = result(); goal thy @@ -224,7 +224,7 @@ \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ \ : set evs"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed_spec_mp "Crypt_imp_OR1"; @@ -236,11 +236,11 @@ \ Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \ \ --> B = B'"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_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); -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); val lemma = result(); goal thy @@ -261,11 +261,10 @@ \ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ \ ~: parts (spies evs)"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -by (REPEAT (blast_tac (claset() addSEs spies_partsEs - addSDs [impOfSubs parts_insert_subset_Un]) 1)); +by (ALLGOALS Blast_tac); qed_spec_mp"no_nonce_OR1_OR2"; +val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE); (*Crucial property: If the encrypted message appears, and A has used NA to start a run, then it originated with the Server!*) @@ -281,24 +280,19 @@ \ Crypt (shrK B) {|NB, Key K|}|} \ \ : set evs)"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); (*OR1: it cannot be a new Nonce, contradiction.*) -by (blast_tac (claset() addSIs [parts_insertI] addSEs spies_partsEs) 1); +by (Blast_tac 1); (*OR3 and OR4*) by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); by (rtac conjI 1); by (ALLGOALS Clarify_tac); (*OR4*) -by (blast_tac (claset() addSIs [Crypt_imp_OR1] - addEs spies_partsEs) 3); -(*OR3, two cases*) (** LEVEL 5 **) -by (blast_tac (claset() addSEs [MPair_parts] - addSDs [Says_imp_spies RS parts.Inj] - addEs [no_nonce_OR1_OR2 RSN (2, rev_notE)] - delrules [conjI] (*stop split-up into 4 subgoals*)) 2); -by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj] - addSEs [MPair_parts] - addIs [unique_NA]) 1); +by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 3); +(*OR3, two cases*) (** LEVEL 7 **) +by (blast_tac (claset() addSEs [nonce_OR1_OR2_E] + delrules [conjI] (*stop split-up into 4 subgoals*)) 2); +by (blast_tac (claset() addIs [unique_NA]) 1); qed_spec_mp "NA_Crypt_imp_Server_msg"; @@ -316,8 +310,7 @@ \ Crypt (shrK A) {|NA, Key K|}, \ \ Crypt (shrK B) {|NB, Key K|}|} \ \ : set evs"; -by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg] - addEs spies_partsEs) 1); +by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); qed "A_trusts_OR4"; @@ -343,8 +336,7 @@ (*OR4*) by (Blast_tac 3); (*OR3*) -by (blast_tac (claset() addSEs spies_partsEs - addIs [impOfSubs analz_subset_parts]) 2); +by (Blast_tac 2); (*Fake*) by (spy_analz_tac 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); @@ -374,7 +366,6 @@ \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ \ : set evs)"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); by (ALLGOALS Blast_tac); bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE); @@ -387,11 +378,11 @@ \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \ \ --> NA = NA' & A = A'"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_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); -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); val lemma = result(); goal thy @@ -417,20 +408,20 @@ \ Crypt (shrK B) {|NB, Key K|}|} \ \ : set evs)"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); (*OR1: it cannot be a new Nonce, contradiction.*) -by (blast_tac (claset() addSIs [parts_insertI] addSEs spies_partsEs) 1); +by (Blast_tac 1); (*OR4*) -by (blast_tac (claset() addSEs [MPair_parts, Crypt_imp_OR2]) 2); +by (blast_tac (claset() addSEs [Crypt_imp_OR2]) 2); (*OR3*) +(*Provable in 38s by the single command + by (blast_tac (claset() addDs [unique_NB] addEs[nonce_OR1_OR2_E]) 1); +*) by (safe_tac (claset() delrules [disjCI, impCE])); -by (blast_tac (claset() delrules [conjI] (*stop split-up*)) 3); -by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj] - addSEs [MPair_parts] - addDs [unique_NB]) 2); -by (blast_tac (claset() addSEs [MPair_parts, no_nonce_OR1_OR2 RSN (2, rev_notE)] - addSDs [Says_imp_spies RS parts.Inj] - delrules [conjI, impCE] (*stop split-up*)) 1); +by (Blast_tac 3); +by (blast_tac (claset() addDs [unique_NB]) 2); +by (blast_tac (claset() addSEs [nonce_OR1_OR2_E] + delrules [conjI] (*stop split-up*)) 1); qed_spec_mp "NB_Crypt_imp_Server_msg"; @@ -447,8 +438,7 @@ \ Crypt (shrK A) {|NA, Key K|}, \ \ Crypt (shrK B) {|NB, Key K|}|} \ \ : set evs"; -by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg] - addSEs spies_partsEs) 1); +by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); qed "B_trusts_OR3"; @@ -465,8 +455,7 @@ \ : set evs)"; by (etac otway.induct 1); by (ALLGOALS Asm_simp_tac); -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj] - addSEs [MPair_parts, Crypt_imp_OR2]) 3); +by (blast_tac (claset() addSEs [Crypt_imp_OR2]) 3); by (ALLGOALS Blast_tac); bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE); @@ -482,6 +471,6 @@ \ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \ \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\ \ : set evs"; -by (blast_tac (claset() addSDs [A_trusts_OR4] - addSEs [OR3_imp_OR2]) 1); +by (blast_tac (claset() addSDs [A_trusts_OR4] + addSEs [OR3_imp_OR2]) 1); qed "A_auths_B"; diff -r 399868bf8444 -r af3239def3d4 src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Tue Dec 23 11:41:12 1997 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.ML Tue Dec 23 11:43:48 1997 +0100 @@ -17,6 +17,10 @@ set proof_timing; HOL_quantifiers := false; +AddEs spies_partsEs; +AddDs [impOfSubs analz_subset_parts]; +AddDs [impOfSubs Fake_parts_insert]; + (*A "possibility property": there are traces that reach the end*) goal thy @@ -45,12 +49,13 @@ goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \ \ X : analz (spies evs)"; -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); +bd (Says_imp_spies RS analz.Inj) 1; +by (Blast_tac 1); qed "OR4_analz_spies"; goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \ \ : set evs ==> K : parts (spies evs)"; -by (blast_tac (claset() addSEs spies_partsEs) 1); +by (Blast_tac 1); qed "Oops_parts_spies"; (*OR4_analz_spies lets us treat those cases using the same @@ -75,7 +80,6 @@ goal thy "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -86,12 +90,8 @@ qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; -goal thy "!!A. [| Key (shrK A) : parts (spies evs); evs : otway |] ==> A:bad"; -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); -AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; +AddSDs [Spy_see_shrK RSN (2, rev_iffD1), + Spy_analz_shrK RSN (2, rev_iffD1)]; (*Nobody can have used non-existent keys!*) @@ -101,9 +101,9 @@ (*Fake*) by (best_tac (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)] - addIs [impOfSubs analz_subset_parts] - addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] - addss (simpset())) 1); + addIs [impOfSubs analz_subset_parts] + addDs [impOfSubs (analz_subset_parts RS keysFor_mono)] + addss (simpset())) 1); (*OR3*) by (Blast_tac 1); qed_spec_mp "new_keys_not_used"; @@ -195,8 +195,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 (blast_tac (claset() addSEs spies_partsEs - delrules[conjI] (*prevent splitup into 4 subgoals*)) 1); +by (Blast_tac 1); val lemma = result(); @@ -227,7 +226,7 @@ \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ \ : set evs)"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); (*OR3*) by (Blast_tac 1); @@ -244,8 +243,7 @@ \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ \ : set evs"; -by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg] - addEs spies_partsEs) 1); +by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); qed "A_trusts_OR4"; @@ -272,8 +270,7 @@ (*OR4*) by (Blast_tac 3); (*OR3*) -by (blast_tac (claset() addSEs spies_partsEs - addIs [impOfSubs analz_subset_parts]) 2); +by (Blast_tac 2); (*Fake*) by (spy_analz_tac 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); @@ -302,7 +299,7 @@ \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ \ : set evs)"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); (*OR3*) by (Blast_tac 1); @@ -319,6 +316,5 @@ \ {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}, \ \ Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \ \ : set evs"; -by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg] - addEs spies_partsEs) 1); +by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); qed "B_trusts_OR3"; diff -r 399868bf8444 -r af3239def3d4 src/HOL/Auth/WooLam.ML --- a/src/HOL/Auth/WooLam.ML Tue Dec 23 11:41:12 1997 +0100 +++ b/src/HOL/Auth/WooLam.ML Tue Dec 23 11:43:48 1997 +0100 @@ -15,6 +15,10 @@ set proof_timing; HOL_quantifiers := false; +AddEs spies_partsEs; +AddDs [impOfSubs analz_subset_parts]; +AddDs [impOfSubs Fake_parts_insert]; + (*A "possibility property": there are traces that reach the end*) goal thy @@ -62,23 +66,18 @@ goal thy "!!evs. evs : woolam ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; goal thy "!!evs. evs : woolam ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; -by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); +by (Auto_tac()); qed "Spy_analz_shrK"; Addsimps [Spy_analz_shrK]; -goal thy "!!A. [| Key (shrK A) : parts (spies evs); \ -\ evs : woolam |] ==> A:bad"; -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); -AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; +AddSDs [Spy_see_shrK RSN (2, rev_iffD1), + Spy_analz_shrK RSN (2, rev_iffD1)]; (**** Autheticity properties for Woo-Lam ****) @@ -88,61 +87,53 @@ (*If the encrypted message appears then it originated with Alice*) goal thy - "!!evs. [| A ~: bad; evs : woolam |] \ -\ ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) \ -\ --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs)"; + "!!evs. [| Crypt (shrK A) (Nonce NB) : parts (spies evs); \ +\ A ~: bad; evs : woolam |] \ +\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; +by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); -by (Blast_tac 1); -qed_spec_mp "NB_Crypt_imp_Alice_msg"; +by (ALLGOALS Blast_tac); +qed "NB_Crypt_imp_Alice_msg"; (*Guarantee for Server: if it gets a message containing a certificate from Alice, then she originated that certificate. But we DO NOT know that B ever saw it: the Spy may have rerouted the message to the Server.*) goal thy - "!!evs. [| A ~: bad; evs : woolam; \ -\ Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \ -\ : set evs |] \ + "!!evs. [| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \ +\ : set evs; \ +\ A ~: bad; evs : woolam |] \ \ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; -by (blast_tac (claset() addSIs [NB_Crypt_imp_Alice_msg] - addSEs [MPair_parts] - addDs [Says_imp_spies RS parts.Inj]) 1); +by (blast_tac (claset() addSIs [NB_Crypt_imp_Alice_msg]) 1); qed "Server_trusts_WL4"; +AddDs [Server_trusts_WL4]; + (*** WL5 ***) (*Server sent WL5 only if it received the right sort of message*) goal thy - "!!evs. evs : woolam ==> \ -\ Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs \ -\ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \ -\ : set evs)"; + "!!evs. [| Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs; \ +\ evs : woolam |] \ +\ ==> EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \ +\ : set evs"; +by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); by (ALLGOALS Blast_tac); -bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp)); +qed "Server_sent_WL5"; +AddDs [Server_sent_WL5]; (*If the encrypted message appears then it originated with the Server!*) goal thy - "!!evs. [| B ~: bad; evs : woolam |] \ -\ ==> Crypt (shrK B) {|Agent A, NB|} : parts (spies evs) \ -\ --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs"; + "!!evs. [| Crypt (shrK B) {|Agent A, NB|} : parts (spies evs); \ +\ B ~: bad; evs : woolam |] \ +\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs"; +by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_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 - sent the same message.*) -goal thy - "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set evs; \ -\ B ~: bad; evs : woolam |] \ -\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs"; -by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg] - addDs [Says_imp_spies RS parts.Inj]) 1); -qed "B_got_WL5"; - (*Guarantee for B. If B gets the Server's certificate then A has encrypted the nonce using her key. This event can be no older than the nonce itself. But A may have sent the nonce to some other agent and it could have reached @@ -151,20 +142,18 @@ "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \ \ A ~: bad; B ~: bad; evs : woolam |] \ \ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; -by (blast_tac (claset() addIs [Server_trusts_WL4] - addSDs [B_got_WL5 RS Server_sent_WL5]) 1); +by (blast_tac (claset() addSDs [NB_Crypt_imp_Server_msg]) 1); qed "B_trusts_WL5"; -(*B only issues challenges in response to WL1. Useful??*) +(*B only issues challenges in response to WL1. Not used.*) goal thy - "!!evs. [| B ~= Spy; evs : woolam |] \ -\ ==> Says B A (Nonce NB) : set evs \ -\ --> (EX A'. Says A' B (Agent A) : set evs)"; + "!!evs. [| Says B A (Nonce NB) : set evs; B ~= Spy; evs : woolam |] \ +\ ==> EX A'. Says A' B (Agent A) : set evs"; +by (etac rev_mp 1); by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); by (ALLGOALS Blast_tac); -bind_thm ("B_said_WL2", result() RSN (2, rev_mp)); +qed "B_said_WL2"; (**CANNOT be proved because A doesn't know where challenges come from... @@ -174,7 +163,6 @@ \ Says B A (Nonce NB) : set evs \ \ --> Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; by (parts_induct_tac 1); -by (Fake_parts_insert_tac 1); +by (Blast_tac 1); by Safe_tac; -by (blast_tac (claset() addSEs partsEs) 1); **)