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")
--- 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*)
--- 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*)
--- 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*)
--- 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*)
--- 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*)
--- 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 ***)
--- 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])));
--- 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]
--- 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;
--- 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);