--- a/src/HOL/Auth/OtwayRees_AN.thy Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy Tue Mar 09 11:01:39 1999 +0100
@@ -28,9 +28,14 @@
(*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; X: synth (analz (spies evs)) |]
+ Fake "[| evs: otway; X: synth (analz (knows Spy evs)) |]
==> Says Spy B X # evs : otway"
+ (*A message that has been sent can be received by the
+ intended recipient.*)
+ Reception "[| evsr: otway; Says A B X : set evsr |]
+ ==> Gets B X # evsr : otway"
+
(*Alice initiates a protocol run*)
OR1 "[| evs1: otway |]
==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 : otway"
@@ -38,14 +43,14 @@
(*Bob's response to Alice's message. Bob doesn't know who
the sender is, hence the A' in the sender field.*)
OR2 "[| evs2: otway;
- Says A' B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
+ Gets B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
# evs2 : otway"
(*The Server receives Bob's message. Then he sends a new
session key to Bob with a packet for forwarding to Alice.*)
OR3 "[| evs3: otway; Key KAB ~: used evs3;
- Says B' Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
+ Gets Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
: set evs3 |]
==> Says Server B
{|Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key KAB|},
@@ -57,7 +62,7 @@
Need B ~= Server because we allow messages to self.*)
OR4 "[| evs4: otway; B ~= Server;
Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|} : set evs4;
- Says S' B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
+ Gets B {|X, Crypt(shrK B){|Nonce NB,Agent A,Agent B,Key K|}|}
: set evs4 |]
==> Says B A X # evs4 : otway"