--- 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 **)
--- 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();
--- 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*)
--- 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*)
--- 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*)