src/HOL/Auth/NS_Public.ML
changeset 4422 21238c9d363e
parent 4197 1547bc6daa5a
child 4449 df30e75f670f
--- 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";