# HG changeset patch
# User paulson
# Date 879243351 -3600
# Node ID 1547bc6daa5aeaade2eb0d8d576dcb615ef9d48b
# Parent  9953c0995b79c818e40518e9563b6aa70b09c13c
Made some proofs more robust

diff -r 9953c0995b79 -r 1547bc6daa5a src/HOL/Auth/NS_Public.ML
--- a/src/HOL/Auth/NS_Public.ML	Tue Nov 11 11:12:37 1997 +0100
+++ b/src/HOL/Auth/NS_Public.ML	Tue Nov 11 11:15:51 1997 +0100
@@ -247,22 +247,22 @@
  "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
 \             : set evs;                                               \
 \           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
-\           A ~: bad;  B ~: bad;  evs : ns_public |]                 \
+\           A ~: bad;  B ~: bad;  evs : ns_public |]                   \
 \        ==> Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
 by (etac rev_mp 1);
 (*prepare induction over Crypt (pubK B) NB : parts H*)
 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*)
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
-			      Spy_not_see_NB, unique_NB]) 3);
+(*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);
 (*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);
+                        addDs  [Spy_not_see_NB, 
+			        impOfSubs analz_subset_parts]) 1);
 qed "B_trusts_NS3";
 
 
@@ -287,14 +287,14 @@
 by (etac ns_public.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (ALLGOALS Clarify_tac);
-(*NS3: because NB determines A*)
+(*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);
+                               Spy_not_see_NB, 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);
+                        addDs  [Spy_not_see_NB, 
+			        impOfSubs analz_subset_parts]) 1);
 qed "B_trusts_protocol";
 
diff -r 9953c0995b79 -r 1547bc6daa5a src/HOL/Auth/NS_Public_Bad.ML
--- a/src/HOL/Auth/NS_Public_Bad.ML	Tue Nov 11 11:12:37 1997 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML	Tue Nov 11 11:15:51 1997 +0100
@@ -259,9 +259,9 @@
 by (parts_induct_tac 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
 by (ALLGOALS Clarify_tac);
-(*NS3: because NB determines A*)
-by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, 
-			      Spy_not_see_NB, unique_NB]) 3);
+(*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);
 (*NS1: by freshness*)
 by (blast_tac (claset() addSEs spies_partsEs) 2);
 (*Fake*)