# HG changeset patch
# User paulson
# Date 884254998 -3600
# Node ID 0218c486cf078c2721784ab544000a62bb2d9cb6
# Parent  c7f56322a84bf4e3ccabe54ff9f2d4ed02fc4299
Restored the ciphertext in OR4 in order to make the spec closer to that in
OtwayRees.thy

diff -r c7f56322a84b -r 0218c486cf07 src/HOL/Auth/OtwayRees_Bad.thy
--- a/src/HOL/Auth/OtwayRees_Bad.thy	Thu Jan 08 11:21:45 1998 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy	Thu Jan 08 11:23:18 1998 +0100
@@ -60,7 +60,8 @@
          (*Bob receives the Server's (?) message and compares the Nonces with
 	   those in the message he previously sent the Server.*)
     OR4  "[| evs4: otway;  A ~= B;
-             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
+             Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB,
+                             Crypt (shrK B) {|Nonce NA, Agent A, Agent B|}|}
                : set evs4;
              Says S' B {|Nonce NA, X, Crypt (shrK B) {|Nonce NB, Key K|}|}
                : set evs4 |]