src/HOL/Auth/OtwayRees.thy
changeset 2135 80477862ab33
parent 2105 782772e744dc
child 2284 80ebd1a213fd
--- a/src/HOL/Auth/OtwayRees.thy	Mon Oct 28 15:36:18 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.thy	Mon Oct 28 15:59:39 1996 +0100
@@ -62,7 +62,7 @@
 
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.*)
-    OR4  "[| evs: otway lost;  A ~= B;  B ~= Server;
+    OR4  "[| evs: otway lost;  A ~= B;  
              Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
                : set_of_list evs;
              Says B Server {|Nonce NA, Agent A, Agent B, X', 
@@ -71,14 +71,11 @@
                : set_of_list evs |]
           ==> Says B A {|Nonce NA, X|} # evs : otway lost"
 
-         (*This message models possible leaks of session keys.  Alice's Nonce
-           identifies the protocol run.*)
-    Revl "[| evs: otway lost;  A ~= Spy;
-             Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
-               : set_of_list evs;
-             Says A  B {|Nonce NA, Agent A, Agent B, 
-                         Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
+         (*This message models possible leaks of session keys.  The nonces
+           identify the protocol run.*)
+    Oops "[| evs: otway lost;  B ~= Spy;
+             Says Server B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
                : set_of_list evs |]
-          ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost"
+          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
 
 end