--- a/src/HOL/Auth/Message.ML Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/Message.ML Tue Dec 16 15:17:26 1997 +0100
@@ -18,11 +18,19 @@
AddIffs atomic.inject;
AddIffs msg.inject;
-(*Holds because Friend is injective: thus cannot prove for all f*)
+(*Equations hold because constructors are injective; cannot prove for all f*)
goal thy "(Friend x : Friend``A) = (x:A)";
by (Auto_tac());
qed "Friend_image_eq";
-Addsimps [Friend_image_eq];
+
+goal thy "(Key x : Key``A) = (x:A)";
+by (Auto_tac());
+qed "Key_image_eq";
+
+goal thy "(Nonce x ~: Key``A)";
+by (Auto_tac());
+qed "Nonce_Key_image_eq";
+Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
(** Inverse of keys **)
--- a/src/HOL/Auth/NS_Public.ML Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/NS_Public.ML Tue Dec 16 15:17:26 1997 +0100
@@ -57,9 +57,13 @@
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(claset() addDs [impOfSubs analz_subset_parts], simpset()));
+by (Auto_tac());
qed "Spy_analz_priK";
Addsimps [Spy_analz_priK];
@@ -135,15 +139,12 @@
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 [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
(*NS2*)
by (blast_tac (claset() addSEs [MPair_parts]
- addDs [Says_imp_spies RS parts.Inj,
- parts.Body, unique_NA]) 3);
+ addDs [parts.Body, unique_NA]) 3);
(*NS1*)
-by (blast_tac (claset() addSEs spies_partsEs
- addIs [impOfSubs analz_subset_parts]) 2);
+by (blast_tac (claset() addSEs spies_partsEs) 2);
(*Fake*)
by (spy_analz_tac 1);
qed "Spy_not_see_NA";
@@ -166,9 +167,7 @@
(*NS1*)
by (blast_tac (claset() addSEs spies_partsEs) 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*)
@@ -198,7 +197,8 @@
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])));
(*NS2*)
by (expand_case_tac "NB = ?y" 2 THEN blast_tac (claset() addSEs partsEs) 2);
(*Fake*)
@@ -228,18 +228,18 @@
by (etac rev_mp 1);
by (analz_induct_tac 1);
(*NS3*)
-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 [no_nonce_NS1_NS2 RSN (2, rev_notE)]
+ addEs partsEs) 3);
(*NS1*)
by (blast_tac (claset() addSEs spies_partsEs) 2);
(*Fake*)
by (spy_analz_tac 1);
qed "Spy_not_see_NB";
+AddDs [Spy_not_see_NB];
+
(*Authentication for B: if he receives message 3 and has used NB
in message 2, then A has sent message 3.*)
@@ -254,15 +254,12 @@
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 (this use of unique_NB is more robust) *)
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Spy_not_see_NB]
- addIs [unique_NB RS conjunct1]) 3);
+(*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 (claset() addSDs [impOfSubs Fake_parts_insert]
- addDs [Spy_not_see_NB,
- impOfSubs analz_subset_parts]) 1);
+by (Blast_tac 1);
qed "B_trusts_NS3";
@@ -288,13 +285,10 @@
by (ALLGOALS Asm_simp_tac);
by (ALLGOALS Clarify_tac);
(*NS3: because NB determines A and NA*)
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj,
- Spy_not_see_NB, unique_NB]) 3);
+by (blast_tac (claset() addDs [unique_NB]) 3);
(*NS1*)
by (blast_tac (claset() addSEs spies_partsEs) 2);
(*Fake*)
-by (blast_tac (claset() addSDs [impOfSubs Fake_parts_insert]
- addDs [Spy_not_see_NB,
- impOfSubs analz_subset_parts]) 1);
+by (Blast_tac 1);
qed "B_trusts_protocol";
--- a/src/HOL/Auth/NS_Shared.ML Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/NS_Shared.ML Tue Dec 16 15:17:26 1997 +0100
@@ -214,9 +214,7 @@
(*Takes 9 secs*)
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
(*Fake*)
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
qed_spec_mp "analz_image_freshK";
--- a/src/HOL/Auth/OtwayRees.ML Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Tue Dec 16 15:17:26 1997 +0100
@@ -173,9 +173,7 @@
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
(*Fake*)
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
qed_spec_mp "analz_image_freshK";
--- a/src/HOL/Auth/OtwayRees_AN.ML Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Tue Dec 16 15:17:26 1997 +0100
@@ -165,9 +165,7 @@
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
(*Fake*)
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
qed_spec_mp "analz_image_freshK";
--- a/src/HOL/Auth/OtwayRees_Bad.ML Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Tue Dec 16 15:17:26 1997 +0100
@@ -176,9 +176,7 @@
by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
(*Fake*)
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
qed_spec_mp "analz_image_freshK";
--- a/src/HOL/Auth/Public.ML Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/Public.ML Tue Dec 16 15:17:26 1997 +0100
@@ -34,6 +34,24 @@
AddIffs [not_isSymKey_pubK, not_isSymKey_priK];
+
+(** "Image" equations that hold for injective functions **)
+
+goal thy "(invKey x : invKey``A) = (x:A)";
+by (Auto_tac());
+qed "invKey_image_eq";
+
+(*holds because invKey is injective*)
+goal thy "(pubK x : pubK``A) = (x:A)";
+by (Auto_tac());
+qed "pubK_image_eq";
+
+goal thy "(priK x ~: pubK``A)";
+by (Auto_tac());
+qed "priK_pubK_image_eq";
+Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq];
+
+
(** Rewrites should not refer to initState(Friend i)
-- not in normal form! **)
--- a/src/HOL/Auth/Recur.ML Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/Recur.ML Tue Dec 16 15:17:26 1997 +0100
@@ -247,8 +247,6 @@
by (ALLGOALS
(asm_simp_tac
(analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
-(*Base*)
-by (Blast_tac 1);
(*Fake*)
by (spy_analz_tac 1);
val raw_analz_image_freshK = result();
--- a/src/HOL/Auth/TLS.ML Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/TLS.ML Tue Dec 16 15:17:26 1997 +0100
@@ -197,14 +197,14 @@
ClientKeyExch_tac (i+6) THEN (*ClientKeyExch*)
ALLGOALS (asm_simp_tac
(simpset() addcongs [if_weak_cong]
- addsimps (expand_ifs@pushes)
- addsplits [expand_if])) THEN
+ 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.*)
ALLGOALS (asm_simp_tac
(simpset() addcongs [if_weak_cong]
- addsimps [insert_absorb]
- addsplits [expand_if]));
+ addsimps [insert_absorb]
+ addsplits [expand_if]));
(*** Properties of items found in Notes ***)
@@ -228,7 +228,7 @@
by (blast_tac (claset() addIs [parts_insertI]) 1);
(*Client, Server Accept*)
by (REPEAT (blast_tac (claset() addSEs spies_partsEs
- addSDs [Notes_Crypt_parts_spies]) 1));
+ addSDs [Notes_Crypt_parts_spies]) 1));
qed "Notes_master_imp_Crypt_PMS";
(*Compared with the theorem above, both premise and conclusion are stronger*)
@@ -380,9 +380,7 @@
(asm_simp_tac (analz_image_keys_ss
addsimps (certificate_def::keys_distinct))));
(*Fake*)
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
qed_spec_mp "analz_image_priK";
@@ -412,16 +410,14 @@
by (ClientKeyExch_tac 7);
by (REPEAT_FIRST (resolve_tac [allI, impI]));
by (REPEAT_FIRST (rtac analz_image_keys_lemma));
-by (ALLGOALS (*15 seconds*)
+by (ALLGOALS (*18 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])));
(*Fake*)
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
qed_spec_mp "analz_image_keys";
(*Knowing some session keys is no help in getting new nonces*)
@@ -542,7 +538,7 @@
by (Blast_tac 3);
(*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)
by (blast_tac (claset() addSDs [Spy_not_see_PMS,
- Says_imp_spies RS analz.Inj]) 2);
+ Says_imp_spies RS analz.Inj]) 2);
(*Fake*)
by (spy_analz_tac 1);
(*ServerHello and ClientKeyExch: mostly freshness reasoning*)
@@ -659,7 +655,7 @@
\ Notes A {|Agent B, Nonce PMS|} : set evs --> \
\ X : parts (spies evs) --> Says B A X : set evs";
by (hyp_subst_tac 1);
-by (analz_induct_tac 1); (*22 seconds*)
+by (analz_induct_tac 1); (*26 seconds*)
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
(*proves ServerResume*)
by (ALLGOALS Clarify_tac);
@@ -668,7 +664,7 @@
(*Fake: the Spy doesn't have the critical session key!*)
by (subgoal_tac "Key (serverK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS,
- not_parts_not_analz]) 2);
+ not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
val lemma = normalize_thm [RSmp] (result());
@@ -731,7 +727,7 @@
\ evs : tls; A ~: bad; B ~: bad |] \
\ ==> EX A'. Says B A' (Crypt (serverK(Na,Nb,M)) Y) : set evs";
by (blast_tac (claset() addIs [lemma]
- addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
+ addEs [serverK_Oops_ALL RSN(2, rev_notE)]) 1);
qed_spec_mp "TrustServerMsg";
@@ -760,7 +756,7 @@
(*Fake: the Spy doesn't have the critical session key!*)
by (subgoal_tac "Key (clientK(Na,Nb,PRF(PMS,NA,NB))) ~: analz(spies evsa)" 1);
by (asm_simp_tac (simpset() addsimps [Spy_not_see_MS,
- not_parts_not_analz]) 2);
+ not_parts_not_analz]) 2);
by (Fake_parts_insert_tac 1);
val lemma = normalize_thm [RSmp] (result());
--- a/src/HOL/Auth/Yahalom.ML Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/Yahalom.ML Tue Dec 16 15:17:26 1997 +0100
@@ -165,9 +165,7 @@
by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
(*Fake*)
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
qed_spec_mp "analz_image_freshK";
goal thy
@@ -386,11 +384,9 @@
KeyWithNonce_Says, fresh_not_KeyWithNonce,
imp_disj_not1, (*Moves NBa~=NB to the front*)
Says_Server_KeyWithNonce])));
-(*Base*)
-by (Blast_tac 1);
(*Fake*)
by (spy_analz_tac 1);
-(*YM4*) (** LEVEL 7 **)
+(*YM4*) (** LEVEL 6 **)
by (not_bad_tac "A" 1);
by (dtac (Says_imp_spies RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1
THEN REPEAT (assume_tac 1));
--- a/src/HOL/Auth/Yahalom2.ML Tue Dec 16 15:15:38 1997 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Tue Dec 16 15:17:26 1997 +0100
@@ -167,9 +167,7 @@
by (REPEAT_FIRST (rtac analz_image_freshK_lemma));
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
(*Fake*)
-by (spy_analz_tac 2);
-(*Base*)
-by (Blast_tac 1);
+by (spy_analz_tac 1);
qed_spec_mp "analz_image_freshK";
goal thy