# HG changeset patch # User paulson # Date 884620599 -3600 # Node ID e7a4683c0026c586bc264a146ee0fc9d6190836d # Parent 1d7f8faaaea38dc3872866c614deb38d8971f69e Tidying, mostly to do with handling a more specific version of Fake_parts_insert diff -r 1d7f8faaaea3 -r e7a4683c0026 src/HOL/Auth/Message.ML --- a/src/HOL/Auth/Message.ML Mon Jan 12 15:47:43 1998 +0100 +++ b/src/HOL/Auth/Message.ML Mon Jan 12 16:56:39 1998 +0100 @@ -240,8 +240,8 @@ goal thy "!!H. X: parts H ==> parts (insert X H) = parts H"; by (fast_tac (claset() addSDs [parts_cut] - addIs [parts_insertI] - addss (simpset())) 1); + addIs [parts_insertI] + addss (simpset())) 1); qed "parts_cut_eq"; Addsimps [parts_cut_eq]; @@ -472,7 +472,7 @@ \ else insert (Crypt K X) (analz H))"; by (case_tac "Key (invKey K) : analz H " 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [analz_insert_Crypt, - analz_insert_Decrypt]))); + analz_insert_Decrypt]))); qed "analz_Crypt_if"; Addsimps [analz_insert_Agent, analz_insert_Nonce, @@ -551,7 +551,7 @@ goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; by (asm_simp_tac (simpset() addsimps [insert_def] delsimps [singleton_conv] - setloop (rtac analz_cong)) 1); + setloop (rtac analz_cong)) 1); qed "analz_insert_cong"; (*If there are no pairs or encryptions then analz does nothing*) @@ -675,7 +675,7 @@ by (etac parts.induct 1); by (ALLGOALS (blast_tac (claset() addIs ((synth_increasing RS parts_mono RS subsetD) - ::parts.intrs)))); + ::parts.intrs)))); qed "parts_synth"; Addsimps [parts_synth]; @@ -706,29 +706,22 @@ by (Blast_tac 1); qed "parts_insert_subset_Un"; -(*More specifically for Fake*) -goal thy "!!H. X: synth (analz G) ==> \ -\ parts (insert X H) <= synth (analz G) Un parts G Un parts H"; +(*More specifically for Fake. Very occasionally we could do with a version + of the form parts{X} <= synth (analz H) Un parts H *) +goal thy "!!H. X: synth (analz H) ==> \ +\ parts (insert X H) <= synth (analz H) Un parts H"; by (dtac parts_insert_subset_Un 1); by (Full_simp_tac 1); by (Blast_tac 1); qed "Fake_parts_insert"; -goal thy - "!!H. [| Crypt K Y : parts (insert X H); X: synth (analz G); \ -\ Key K ~: analz G |] \ -\ ==> Crypt K Y : parts G Un parts H"; -by (dtac (impOfSubs Fake_parts_insert) 1); -by (assume_tac 1); -by (blast_tac (claset() addDs [impOfSubs analz_subset_parts]) 1); -qed "Crypt_Fake_parts_insert"; - +(*H is sometimes (Key `` KK Un spies evs), so can't put G=H*) goal thy "!!H. X: synth (analz G) ==> \ \ analz (insert X H) <= synth (analz G) Un analz (G Un H)"; by (rtac subsetI 1); by (subgoal_tac "x : analz (synth (analz G) Un H)" 1); by (blast_tac (claset() addIs [impOfSubs analz_mono, - impOfSubs (analz_mono RS synth_mono)]) 2); + impOfSubs (analz_mono RS synth_mono)]) 2); by (Full_simp_tac 1); by (Blast_tac 1); qed "Fake_analz_insert"; @@ -875,8 +868,9 @@ ALLGOALS Asm_simp_tac; fun Fake_parts_insert_tac i = - blast_tac (claset() addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert]) i; + blast_tac (claset() addIs [parts_insertI] + 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) @@ -909,7 +903,7 @@ THEN IF_UNSOLVED (Blast.depth_tac (claset() addIs [analz_insertI, - impOfSubs analz_subset_parts]) 4 1)) + impOfSubs analz_subset_parts]) 4 1)) ]) i); (** Useful in many uniqueness proofs **) diff -r 1d7f8faaaea3 -r e7a4683c0026 src/HOL/Auth/NS_Public.ML --- a/src/HOL/Auth/NS_Public.ML Mon Jan 12 15:47:43 1998 +0100 +++ b/src/HOL/Auth/NS_Public.ML Mon Jan 12 16:56:39 1998 +0100 @@ -5,9 +5,6 @@ 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; @@ -80,8 +77,7 @@ is secret. (Honest users generate fresh nonces.)*) goal thy "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ -\ Nonce NA ~: analz (spies evs); \ -\ evs : ns_public |] \ +\ Nonce NA ~: analz (spies evs); evs : ns_public |] \ \ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (spies evs)"; by (etac rev_mp 1); by (etac rev_mp 1); @@ -101,14 +97,11 @@ \ A=A' & B=B'"; by (etac rev_mp 1); by (parts_induct_tac 1); -by (ALLGOALS - (asm_simp_tac (simpset() addsimps [all_conj_distrib, - parts_insert_spies]))); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); (*NS1*) by (expand_case_tac "NA = ?y" 2 THEN Blast_tac 2); (*Fake*) by (Clarify_tac 1); -by (ex_strip_tac 1); by (Blast_tac 1); val lemma = result(); @@ -130,8 +123,8 @@ (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) goal thy - "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ -\ A ~: bad; B ~: bad; evs : ns_public |] \ + "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ +\ A ~: bad; B ~: bad; evs : ns_public |] \ \ ==> Nonce NA ~: analz (spies evs)"; by (etac rev_mp 1); by (analz_induct_tac 1); @@ -149,10 +142,10 @@ (*Authentication for A: if she receives message 2 and has used NA to start a run, then B has sent message 2.*) goal thy - "!!evs. [| Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs; \ + "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs; \ \ Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ \ : set evs; \ -\ A ~: bad; B ~: bad; evs : ns_public |] \ +\ A ~: bad; B ~: bad; evs : ns_public |] \ \ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ \ : set evs"; by (etac rev_mp 1); @@ -166,11 +159,12 @@ by (blast_tac (claset() addDs [Spy_not_see_NA]) 1); qed "A_trusts_NS2"; + (*If the encrypted message appears then it originated with Alice in NS1*) goal thy "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ -\ Nonce NA ~: analz (spies evs); \ -\ evs : ns_public |] \ +\ Nonce NA ~: analz (spies evs); \ +\ evs : ns_public |] \ \ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set evs"; by (etac rev_mp 1); by (etac rev_mp 1); @@ -192,14 +186,11 @@ \ --> A=A' & NA=NA' & B=B'"; by (etac rev_mp 1); by (parts_induct_tac 1); -by (ALLGOALS - (asm_simp_tac (simpset() addsimps [all_conj_distrib, - parts_insert_spies]))); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); (*NS2*) by (expand_case_tac "NB = ?y" 2 THEN Blast_tac 2); (*Fake*) by (Clarify_tac 1); -by (ex_strip_tac 1); by (Blast_tac 1); val lemma = result(); diff -r 1d7f8faaaea3 -r e7a4683c0026 src/HOL/Auth/NS_Public_Bad.ML --- a/src/HOL/Auth/NS_Public_Bad.ML Mon Jan 12 15:47:43 1998 +0100 +++ b/src/HOL/Auth/NS_Public_Bad.ML Mon Jan 12 16:56:39 1998 +0100 @@ -16,6 +16,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*) @@ -57,13 +61,13 @@ 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]; goal thy "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)"; -by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); +by Auto_tac; qed "Spy_analz_priK"; Addsimps [Spy_analz_priK]; @@ -82,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 @@ -98,15 +101,12 @@ \ A=A' & B=B'"; by (etac rev_mp 1); by (parts_induct_tac 1); -by (ALLGOALS - (asm_simp_tac (simpset() addsimps [all_conj_distrib, - parts_insert_spies]))); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); (*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 @@ -133,15 +133,11 @@ by (etac rev_mp 1); by (analz_induct_tac 1); (*NS3*) -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj] - 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 [Says_imp_spies RS parts.Inj, - parts.Body, unique_NA]) 3); +by (blast_tac (claset() addDs [unique_NA]) 3); (*NS1*) -by (blast_tac (claset() addSEs spies_partsEs - addIs [impOfSubs analz_subset_parts]) 2); +by (Blast_tac 2); (*Fake*) by (spy_analz_tac 1); qed "Spy_not_see_NA"; @@ -161,16 +157,14 @@ by (ALLGOALS Asm_simp_tac); by (ALLGOALS Clarify_tac); (*NS2*) -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, - Spy_not_see_NA, unique_NA]) 3); +by (blast_tac (claset() addDs [Spy_not_see_NA, unique_NA]) 3); (*NS1*) -by (blast_tac (claset() addSEs spies_partsEs) 2); +by (Blast_tac 2); (*Fake*) -by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert] - addDs [Spy_not_see_NA, - impOfSubs analz_subset_parts]) 1); +by (blast_tac (claset() addDs [Spy_not_see_NA]) 1); qed "A_trusts_NS2"; + (*If the encrypted message appears then it originated with Alice in NS1*) goal thy "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \ @@ -180,30 +174,27 @@ 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"; (**** Authenticity properties obtained from NS2 ****) -(*Unicity for NS2: nonce NB identifies agent A and nonce NA +(*Unicity for NS2: nonce NB identifies nonce NA and agent A [proof closely follows that for unique_NA] *) goal thy - "!!evs. [| Nonce NB ~: analz (spies evs); evs : ns_public |] \ -\ ==> EX A' NA'. ALL A NA. \ -\ Crypt (pubK A) {|Nonce NA, Nonce NB|} \ -\ : parts (spies evs) --> A=A' & NA=NA'"; + "!!evs. [| Nonce NB ~: analz (spies evs); evs : ns_public |] \ +\ ==> EX A' NA'. ALL A NA. \ +\ Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (spies evs) \ +\ --> A=A' & NA=NA'"; by (etac rev_mp 1); by (parts_induct_tac 1); -by (ALLGOALS - (asm_simp_tac (simpset() addsimps [all_conj_distrib, parts_insert_spies]))); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); (*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 @@ -228,14 +219,11 @@ by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); by (ALLGOALS Clarify_tac); (*NS3: because NB determines A*) -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, unique_NB]) 4); +by (blast_tac (claset() addDs [unique_NB]) 4); (*NS2: by freshness and unicity of NB*) -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj] - addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)] - addEs partsEs - addIs [impOfSubs analz_subset_parts]) 3); +by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3); (*NS1: by freshness*) -by (blast_tac (claset() addSEs spies_partsEs) 2); +by (Blast_tac 2); (*Fake*) by (spy_analz_tac 1); qed "Spy_not_see_NB"; @@ -256,14 +244,12 @@ by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); by (ALLGOALS Clarify_tac); (*NS3: because NB determines A (this use of unique_NB is more robust) *) -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Spy_not_see_NB] +by (blast_tac (claset() addDs [Spy_not_see_NB] addIs [unique_NB RS conjunct1]) 3); (*NS1: by freshness*) -by (blast_tac (claset() addSEs spies_partsEs) 2); +by (Blast_tac 2); (*Fake*) -by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert] - addDs [Spy_not_see_NB, - impOfSubs analz_subset_parts]) 1); +by (blast_tac (claset() addDs [Spy_not_see_NB]) 1); qed "B_trusts_NS3"; @@ -275,12 +261,9 @@ by (analz_induct_tac 1); by (ALLGOALS Clarify_tac); (*NS2: by freshness and unicity of NB*) -by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj] - addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)] - addEs partsEs - addIs [impOfSubs analz_subset_parts]) 3); +by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3); (*NS1: by freshness*) -by (blast_tac (claset() addSEs spies_partsEs) 2); +by (Blast_tac 2); (*Fake*) by (spy_analz_tac 1); (*NS3: unicity of NB identifies A and NA, but not B*) diff -r 1d7f8faaaea3 -r e7a4683c0026 src/HOL/Auth/Recur.ML --- a/src/HOL/Auth/Recur.ML Mon Jan 12 15:47:43 1998 +0100 +++ b/src/HOL/Auth/Recur.ML Mon Jan 12 16:56:39 1998 +0100 @@ -268,7 +268,6 @@ by (etac responses.induct 2); by (ALLGOALS Asm_simp_tac); (*Fake*) -by (simp_tac (simpset() addsimps [parts_insert_spies]) 1); by (Fake_parts_insert_tac 1); qed "Hash_imp_body"; @@ -440,8 +439,7 @@ by (ALLGOALS (asm_simp_tac (simpset() addsimps (expand_ifs @ - [analz_insert_eq, parts_insert_spies, - analz_insert_freshK])))); + [analz_insert_eq, analz_insert_freshK])))); (*RA4*) by (spy_analz_tac 5); (*RA2*) @@ -451,17 +449,17 @@ (*Base*) by (Blast_tac 1); (*RA3 remains*) +by (simp_tac (simpset() addsimps [parts_insert_spies]) 1); by (safe_tac (claset() delrules [impCE])); (*RA3, case 2: K is an old key*) by (blast_tac (claset() addSDs [resp_analz_insert] - addSEs partsEs - addDs [Key_in_parts_respond]) 2); + addSEs partsEs + addDs [Key_in_parts_respond]) 2); (*RA3, case 1: use lemma previously proved by induction*) by (blast_tac (claset() addSEs [respond_Spy_not_see_session_key RSN (2,rev_notE)]) 1); qed "Spy_not_see_session_key"; - (**** Authenticity properties for Agents ****) (*The response never contains Hashes*) diff -r 1d7f8faaaea3 -r e7a4683c0026 src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Mon Jan 12 15:47:43 1998 +0100 +++ b/src/HOL/Auth/TLS.ML Mon Jan 12 16:56:39 1998 +0100 @@ -299,7 +299,6 @@ \ ==> Nonce PMS : parts (spies evs)"; by (etac rev_mp 1); by (parts_induct_tac 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [parts_insert_spies]))); by (Fake_parts_insert_tac 1); (*Six others, all trivial or by freshness*) by (REPEAT (blast_tac (claset() addSDs [Notes_Crypt_parts_spies] @@ -446,7 +445,6 @@ (*SpyKeys*) by (blast_tac (claset() addSEs spies_partsEs) 3); (*Fake*) -by (simp_tac (simpset() addsimps [parts_insert_spies]) 2); by (Fake_parts_insert_tac 2); (** LEVEL 6 **) (*Oops*)