--- 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";