--- a/src/HOL/Auth/NS_Public.thy Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/NS_Public.thy Thu Dec 19 11:58:39 1996 +0100
@@ -25,15 +25,16 @@
(*Alice initiates a protocol run, sending a nonce to Bob*)
NS1 "[| evs: ns_public; A ~= B |]
- ==> Says A B (Crypt (pubK B) {|Nonce (newN evs), Agent A|}) # evs
- : ns_public"
+ ==> Says A B (Crypt (pubK B) {|Nonce (newN(length evs)), Agent A|})
+ # evs : ns_public"
(*Bob responds to Alice's message with a further nonce*)
NS2 "[| evs: ns_public; A ~= B;
Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
: set_of_list evs |]
- ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN evs), Agent B|})
- # evs : ns_public"
+ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN(length evs)),
+ Agent B|})
+ # evs : ns_public"
(*Alice proves her existence by sending NB back to Bob.*)
NS3 "[| evs: ns_public; A ~= B;