--- a/src/HOL/Auth/OtwayRees_Bad.thy Tue Oct 01 17:44:54 1996 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Tue Oct 01 18:10:33 1996 +0200
@@ -12,7 +12,9 @@
OtwayRees_Bad = Shared +
-consts otway :: "event list set"
+consts lost :: agent set (*No need for it to be a variable*)
+ otway :: event list set
+
inductive otway
intrs
(*Initial trace is empty*)
@@ -21,7 +23,7 @@
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake "[| evs: otway; B ~= Spy; X: synth (analz (sees Spy evs)) |]
+ Fake "[| evs: otway; B ~= Spy; X: synth (analz (sees lost Spy evs)) |]
==> Says Spy B X # evs : otway"
(*Alice initiates a protocol run*)