--- a/src/HOL/Auth/NS_Public_Bad.thy Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.thy Fri Jan 17 12:49:31 1997 +0100
@@ -41,9 +41,9 @@
(*Alice proves her existence by sending NB back to Bob.*)
NS3 "[| evs: ns_public; A ~= B;
- Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
+ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
: set_of_list evs;
- Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
+ Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
: set_of_list evs |]
==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public"