--- a/src/HOL/Auth/NS_Public_Bad.thy Mon Jul 14 12:44:09 1997 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy Mon Jul 14 12:47:21 1997 +0200
@@ -13,8 +13,7 @@
NS_Public_Bad = Public +
-consts lost :: agent set (*No need for it to be a variable*)
- ns_public :: event list set
+consts ns_public :: event list set
inductive ns_public
intrs
@@ -25,7 +24,7 @@
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
Fake "[| evs: ns_public; B ~= Spy;
- X: synth (analz (sees lost Spy evs)) |]
+ X: synth (analz (sees Spy evs)) |]
==> Says Spy B X # evs : ns_public"
(*Alice initiates a protocol run, sending a nonce to Bob*)
@@ -47,8 +46,4 @@
(**Oops message??**)
-rules
- (*Spy has access to his own key for spoof messages*)
- Spy_in_lost "Spy: lost"
-
end