Restored the ciphertext in OR4 in order to make the spec closer to that in
OtwayRees.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 |]