# HG changeset patch
# User paulson
# Date 921058931 -3600
# Node ID b1dec44d001845e4bb990ddb6023a2dc6286fc89
# Parent  7cee353c7f2a8ddc0f3a480ec70aa2b9e9d442c9
deleted obsolete comments

diff -r 7cee353c7f2a -r b1dec44d0018 src/HOL/Auth/OtwayRees.thy
--- 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 
diff -r 7cee353c7f2a -r b1dec44d0018 src/HOL/Auth/OtwayRees_AN.thy
--- 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|}
diff -r 7cee353c7f2a -r b1dec44d0018 src/HOL/Auth/OtwayRees_Bad.thy
--- 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