--- a/src/HOL/Auth/OtwayRees.thy Tue Mar 09 12:20:22 1999 +0100
+++ b/src/HOL/Auth/OtwayRees.thy Wed Mar 10 10:42:11 1999 +0100
@@ -34,9 +34,7 @@
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
# evs1 : otway"
- (*Bob's response to Alice's message. Bob doesn't know who
- the sender is, hence the A' in the sender field.
- Note that NB is encrypted.*)
+ (*Bob's response to Alice's message. Note that NB is encrypted.*)
OR2 "[| evs2: otway; Nonce NB ~: used evs2;
Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
==> Says B Server
--- a/src/HOL/Auth/OtwayRees_AN.thy Tue Mar 09 12:20:22 1999 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.thy Wed Mar 10 10:42:11 1999 +0100
@@ -40,8 +40,7 @@
OR1 "[| evs1: otway |]
==> Says A B {|Agent A, Agent B, Nonce NA|} # evs1 : otway"
- (*Bob's response to Alice's message. Bob doesn't know who
- the sender is, hence the A' in the sender field.*)
+ (*Bob's response to Alice's message.*)
OR2 "[| evs2: otway;
Gets B {|Agent A, Agent B, Nonce NA|} : set evs2 |]
==> Says B Server {|Agent A, Agent B, Nonce NA, Nonce NB|}
--- a/src/HOL/Auth/OtwayRees_Bad.thy Tue Mar 09 12:20:22 1999 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Wed Mar 10 10:42:11 1999 +0100
@@ -36,9 +36,8 @@
Crypt (shrK A) {|Nonce NA, Agent A, Agent B|} |}
# evs1 : otway"
- (*Bob's response to Alice's message. Bob doesn't know who
- the sender is, hence the A' in the sender field.
- We modify the published protocol by NOT encrypting NB.*)
+ (*Bob's response to Alice's message.
+ This variant of the protocol does NOT encrypt NB.*)
OR2 "[| evs2: otway; Nonce NB ~: used evs2;
Gets B {|Nonce NA, Agent A, Agent B, X|} : set evs2 |]
==> Says B Server