# HG changeset patch # User paulson # Date 877423167 -7200 # Node ID 6a8996fb7d999e9391647448bf1da4757ed98d3f # Parent 7a38fae985f932332b997eedb5a5372b324a2f7e Many minor speedups: 1. Some use of rewriting with expand_ifs instead of addsplits[expand_if] 2. Faster proof of new_keys_not_used 3. New version of shrK_neq (no longer refers to "range") diff -r 7a38fae985f9 -r 6a8996fb7d99 src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Tue Oct 21 10:36:23 1997 +0200 +++ b/src/HOL/Auth/NS_Shared.ML Tue Oct 21 10:39:27 1997 +0200 @@ -74,7 +74,7 @@ "!!evs. evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); -by (Blast_tac 1); +by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -99,10 +99,10 @@ by (parts_induct_tac 1); (*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)] - addss (!simpset)) 1); + (!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); (*NS2, NS4, NS5*) by (ALLGOALS (blast_tac (!claset addSEs spies_partsEs))); qed_spec_mp "new_keys_not_used"; @@ -203,8 +203,8 @@ by (etac ns_shared.induct 1); by analz_spies_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); -by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); -(*Takes 24 secs*) +by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); +(*Takes 9 secs*) by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); (*Fake*) by (spy_analz_tac 2); @@ -255,7 +255,7 @@ (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **) goal thy - "!!evs. [| A ~: bad; B ~: bad; evs : ns_shared |] \ + "!!evs. [| A ~: bad; B ~: bad; evs : ns_shared |] \ \ ==> Says Server A \ \ (Crypt (shrK A) {|NA, Agent B, Key K, \ \ Crypt (shrK B) {|Key K, Agent A|}|}) \ @@ -266,8 +266,8 @@ by analz_spies_tac; by (ALLGOALS (asm_simp_tac - (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes) - addsplits [expand_if]))); + (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ + pushes @ expand_ifs)))); (*Oops*) by (blast_tac (!claset addDs [unique_session_keys]) 5); (*NS3, replay sub-case*) diff -r 7a38fae985f9 -r 6a8996fb7d99 src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Tue Oct 21 10:36:23 1997 +0200 +++ b/src/HOL/Auth/OtwayRees.ML Tue Oct 21 10:39:27 1997 +0200 @@ -86,7 +86,7 @@ "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); -by (Blast_tac 1); +by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -110,10 +110,10 @@ by (parts_induct_tac 1); (*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)] - addss (!simpset)) 1); + (!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); by (ALLGOALS Blast_tac); qed_spec_mp "new_keys_not_used"; @@ -339,7 +339,7 @@ by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong] addsimps [analz_insert_eq, analz_insert_freshK] - addsplits [expand_if]))); + addsimps (pushes@expand_ifs)))); (*Oops*) by (blast_tac (!claset addSDs [unique_session_keys]) 4); (*OR4*) diff -r 7a38fae985f9 -r 6a8996fb7d99 src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Tue Oct 21 10:36:23 1997 +0200 +++ b/src/HOL/Auth/OtwayRees_AN.ML Tue Oct 21 10:39:27 1997 +0200 @@ -76,7 +76,7 @@ "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); -by (Blast_tac 1); +by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -100,10 +100,10 @@ by (parts_induct_tac 1); (*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)] - addss (!simpset)) 1); + (!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); (*OR3*) by (Blast_tac 1); qed_spec_mp "new_keys_not_used"; @@ -268,7 +268,7 @@ by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong] addsimps [analz_insert_eq, analz_insert_freshK] - addsplits [expand_if]))); + addsimps (pushes@expand_ifs)))); (*Oops*) by (blast_tac (!claset addSDs [unique_session_keys]) 4); (*OR4*) diff -r 7a38fae985f9 -r 6a8996fb7d99 src/HOL/Auth/OtwayRees_Bad.ML --- a/src/HOL/Auth/OtwayRees_Bad.ML Tue Oct 21 10:36:23 1997 +0200 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Tue Oct 21 10:39:27 1997 +0200 @@ -88,7 +88,7 @@ "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); -by (Blast_tac 1); +by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -112,10 +112,10 @@ by (parts_induct_tac 1); (*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)] - addss (!simpset)) 1); + (!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); (*OR1-3*) by (ALLGOALS Blast_tac); qed_spec_mp "new_keys_not_used"; @@ -231,7 +231,7 @@ by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong] addsimps [analz_insert_eq, analz_insert_freshK] - addsplits [expand_if]))); + addsimps (pushes@expand_ifs)))); (*Oops*) by (blast_tac (!claset addSDs [unique_session_keys]) 4); (*OR4*) diff -r 7a38fae985f9 -r 6a8996fb7d99 src/HOL/Auth/Recur.ML --- a/src/HOL/Auth/Recur.ML Tue Oct 21 10:36:23 1997 +0200 +++ b/src/HOL/Auth/Recur.ML Tue Oct 21 10:39:27 1997 +0200 @@ -192,10 +192,10 @@ addss (!simpset addsimps [parts_insert_spies])) 2); (*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)] - addss (!simpset)) 1); + (!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); qed_spec_mp "new_keys_not_used"; @@ -263,7 +263,7 @@ *) bind_thm ("resp_analz_image_freshK", raw_analz_image_freshK RSN - (2, resp_analz_image_freshK_lemma) RS spec RS spec); + (2, resp_analz_image_freshK_lemma) RS spec RS spec RS mp); goal thy "!!evs. [| evs : recur; KAB ~: range shrK |] ==> \ @@ -422,25 +422,26 @@ by (etac respond.induct 1); by (forward_tac [respond_imp_responses] 2); by (forward_tac [respond_imp_not_used] 2); -by (ALLGOALS (*12 seconds*) +by (ALLGOALS (*6 seconds*) (asm_simp_tac - (analz_image_freshK_ss addsimps - [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2]))); + (analz_image_freshK_ss + addsimps expand_ifs + addsimps + [shrK_in_analz_respond, resp_analz_image_freshK, parts_insert2]))); by (ALLGOALS (simp_tac (!simpset addsimps [ex_disj_distrib]))); (** LEVEL 5 **) by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1); -by (safe_tac (!claset addSEs [MPair_parts])); -by (REPEAT (blast_tac (!claset addSDs [respond_certificate] - addDs [resp_analz_insert] - addIs [impOfSubs analz_subset_parts]) 4)); -by (Blast_tac 3); -by (blast_tac (!claset addSEs partsEs - addDs [Key_in_parts_respond]) 2); -(*by unicity, either B=Aa or B=A', a contradiction since B: bad*) -by (dtac unique_session_keys 1); -by (etac respond_certificate 1); -by (assume_tac 1); -by (Blast_tac 1); +by (REPEAT_FIRST (resolve_tac [allI, conjI, impI])); +by (ALLGOALS Clarify_tac); +by (blast_tac (!claset addSDs [resp_analz_insert] + addIs [impOfSubs analz_subset_parts]) 2); +by (blast_tac (!claset addSDs [respond_certificate]) 1); +by (Asm_full_simp_tac 1); +(*by unicity, either B=Aa or B=A', a contradiction if B: bad*) +by (blast_tac + (!claset addSEs [MPair_parts] + addDs [parts.Body, + respond_certificate RSN (2, unique_session_keys)]) 1); qed_spec_mp "respond_Spy_not_see_session_key"; @@ -453,9 +454,9 @@ by analz_spies_tac; by (ALLGOALS (asm_simp_tac - (!simpset addsimps [analz_insert_eq, parts_insert_spies, - analz_insert_freshK] - addsplits [expand_if]))); + (!simpset addsimps (expand_ifs @ + [analz_insert_eq, parts_insert_spies, + analz_insert_freshK])))); (*RA4*) by (spy_analz_tac 5); (*RA2*) diff -r 7a38fae985f9 -r 6a8996fb7d99 src/HOL/Auth/Shared.ML --- a/src/HOL/Auth/Shared.ML Tue Oct 21 10:36:23 1997 +0200 +++ b/src/HOL/Auth/Shared.ML Tue Oct 21 10:39:27 1997 +0200 @@ -81,13 +81,12 @@ by (Blast_tac 1); qed "Key_not_used"; -(*A session key cannot clash with a long-term shared key*) -goal thy "!!K. K ~: range shrK ==> shrK B ~= K"; +goal thy "!!K. Key K ~: used evs ==> shrK B ~= K"; by (Blast_tac 1); qed "shrK_neq"; Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym]; -Delsimps [image_eqI]; (* loops together with shrK_neq *) + (*** Fresh nonces ***) diff -r 7a38fae985f9 -r 6a8996fb7d99 src/HOL/Auth/TLS.ML --- a/src/HOL/Auth/TLS.ML Tue Oct 21 10:36:23 1997 +0200 +++ b/src/HOL/Auth/TLS.ML Tue Oct 21 10:39:27 1997 +0200 @@ -17,8 +17,13 @@ rollback attacks). *) +open TLS; -open TLS; +val if_distrib_parts = + read_instantiate_sg (sign_of Message.thy) [("f", "parts")] if_distrib; + +val if_distrib_analz = + read_instantiate_sg (sign_of Message.thy) [("f", "analz")] if_distrib; proof_timing:=true; HOL_quantifiers := false; @@ -198,6 +203,7 @@ ClientKeyExch_tac (i+6) THEN (*ClientKeyExch*) ALLGOALS (asm_simp_tac (!simpset addcongs [if_weak_cong] + addsimps (expand_ifs@pushes) addsplits [expand_if])) THEN (*Remove instances of pubK B: the Spy already knows all public keys. Combining the two simplifier calls makes them run extremely slowly.*) @@ -396,7 +402,7 @@ "!!evs. (X : analz (G Un H)) --> (X : analz H) ==> \ \ (X : analz (G Un H)) = (X : analz H)"; by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1); -val lemma = result(); +val analz_image_keys_lemma = result(); (** Strangely, the following version doesn't work: \ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \ @@ -411,9 +417,10 @@ by (etac tls.induct 1); by (ClientKeyExch_tac 7); by (REPEAT_FIRST (resolve_tac [allI, impI])); -by (REPEAT_FIRST (rtac lemma)); -by (ALLGOALS (*24 seconds*) +by (REPEAT_FIRST (rtac analz_image_keys_lemma)); +by (ALLGOALS (*15 seconds*) (asm_simp_tac (analz_image_keys_ss + addsimps (expand_ifs@pushes) addsimps [range_sessionkeys_not_priK, analz_image_priK, certificate_def]))); by (ALLGOALS (asm_simp_tac (!simpset addsimps [insert_absorb]))); diff -r 7a38fae985f9 -r 6a8996fb7d99 src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Tue Oct 21 10:36:23 1997 +0200 +++ b/src/HOL/Auth/Yahalom.ML Tue Oct 21 10:39:27 1997 +0200 @@ -82,7 +82,7 @@ "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; by (parts_induct_tac 1); by (Fake_parts_insert_tac 1); -by (Blast_tac 1); +by (ALLGOALS Blast_tac); qed "Spy_see_shrK"; Addsimps [Spy_see_shrK]; @@ -105,16 +105,14 @@ goal thy "!!evs. evs : yahalom ==> \ \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; by (parts_induct_tac 1); -(*YM4: Key K is not fresh!*) -by (blast_tac (!claset addSEs spies_partsEs) 3); -(*YM3*) -by (Blast_tac 2); (*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)] - addss (!simpset)) 1); + (!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); +(*YM2-4: Because Key K is not fresh, etc.*) +by (REPEAT (blast_tac (!claset addSEs spies_partsEs) 1)); qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", @@ -226,8 +224,8 @@ by analz_spies_tac; by (ALLGOALS (asm_simp_tac - (!simpset addsimps [analz_insert_eq, analz_insert_freshK] - addsplits [expand_if]))); + (!simpset addsimps (expand_ifs@pushes) + addsimps [analz_insert_eq, analz_insert_freshK]))); (*Oops*) by (blast_tac (!claset addDs [unique_session_keys]) 3); (*YM3*) @@ -365,7 +363,7 @@ "!!evs. P --> (X : analz (G Un H)) --> (X : analz H) ==> \ \ P --> (X : analz (G Un H)) = (X : analz H)"; by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1); -val lemma = result(); +val Nonce_secrecy_lemma = result(); goal thy "!!evs. evs : yahalom ==> \ @@ -376,17 +374,18 @@ by (etac yahalom.induct 1); by analz_spies_tac; by (REPEAT_FIRST (resolve_tac [impI RS allI])); -by (REPEAT_FIRST (rtac lemma)); +by (REPEAT_FIRST (rtac Nonce_secrecy_lemma)); (*For Oops, simplification proves NBa~=NB. By Says_Server_KeyWithNonce, we get (~ KeyWithNonce K NB evsa); then simplification can apply the induction hypothesis with KK = {K}.*) -by (ALLGOALS (*17 seconds*) +by (ALLGOALS (*12 seconds*) (asm_simp_tac - (analz_image_freshK_ss addsimps - [all_conj_distrib, analz_image_freshK, - KeyWithNonce_Says, fresh_not_KeyWithNonce, - imp_disj_not1, (*Moves NBa~=NB to the front*) - Says_Server_KeyWithNonce]))); + (analz_image_freshK_ss + addsimps expand_ifs + addsimps [all_conj_distrib, analz_image_freshK, + KeyWithNonce_Says, fresh_not_KeyWithNonce, + imp_disj_not1, (*Moves NBa~=NB to the front*) + Says_Server_KeyWithNonce]))); (*Base*) by (Blast_tac 1); (*Fake*) @@ -498,8 +497,8 @@ by analz_spies_tac; by (ALLGOALS (asm_simp_tac - (!simpset addsimps [analz_insert_eq, analz_insert_freshK] - addsplits [expand_if]))); + (!simpset addsimps (expand_ifs@pushes) + addsimps [analz_insert_eq, analz_insert_freshK]))); (*Prove YM3 by showing that no NB can also be an NA*) by (blast_tac (!claset addDs [Says_imp_spies RS parts.Inj] addSEs [MPair_parts] diff -r 7a38fae985f9 -r 6a8996fb7d99 src/HOL/Auth/Yahalom.thy --- a/src/HOL/Auth/Yahalom.thy Tue Oct 21 10:36:23 1997 +0200 +++ b/src/HOL/Auth/Yahalom.thy Tue Oct 21 10:39:27 1997 +0200 @@ -49,7 +49,8 @@ # evs3 : yahalom" (*Alice receives the Server's (?) message, checks her Nonce, and - uses the new session key to send Bob his Nonce.*) + uses the new session key to send Bob his Nonce. The premise + A ~= Server is needed to prove Says_Server_message_form.*) YM4 "[| evs4: yahalom; A ~= Server; Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, Nonce NB|}, X|} : set evs4; diff -r 7a38fae985f9 -r 6a8996fb7d99 src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Tue Oct 21 10:36:23 1997 +0200 +++ b/src/HOL/Auth/Yahalom2.ML Tue Oct 21 10:39:27 1997 +0200 @@ -111,10 +111,10 @@ by (blast_tac (!claset addss (!simpset)) 2); (*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)] - addss (!simpset)) 1); + (!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); qed_spec_mp "new_keys_not_used"; bind_thm ("new_keys_not_analzd", @@ -164,7 +164,7 @@ by (etac yahalom.induct 1); by analz_spies_tac; by (REPEAT_FIRST (resolve_tac [allI, impI])); -by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); +by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); (*Fake*) by (spy_analz_tac 2); @@ -226,7 +226,8 @@ by analz_spies_tac; by (ALLGOALS (asm_simp_tac - (!simpset addsimps [analz_insert_eq, analz_insert_freshK] + (!simpset addsimps expand_ifs + addsimps [analz_insert_eq, analz_insert_freshK] addsplits [expand_if]))); (*Oops*) by (blast_tac (!claset addDs [unique_session_keys]) 3);