diff -r a0bdee64194c -r 649bf14debe7 src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Thu Feb 05 10:26:59 1998 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Thu Feb 05 10:38:34 1998 +0100
@@ -259,7 +259,7 @@
 (*Crucial property: If the encrypted message appears, and A has used NA
   to start a run, then it originated with the Server!*)
 goal thy 
- "!!evs. [| A ~: bad;  A ~= Spy;  evs : otway |]                      \
+ "!!evs. [| A ~: bad;  evs : otway |]                                  \
 \    ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs)              \
 \        --> Says A B {|NA, Agent A, Agent B,                          \
 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}      \
@@ -291,10 +291,10 @@
   bad form of this protocol, even though we can prove
   Spy_not_see_encrypted_key*)
 goal thy 
- "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
-\           Says A  B {|NA, Agent A, Agent B,                       \
+ "!!evs. [| Says A  B {|NA, Agent A, Agent B,                       \
 \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
-\           A ~: bad;  A ~= Spy;  evs : otway |]                  \
+\           Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
+\           A ~: bad;  evs : otway |]                              \
 \        ==> EX NB. Says Server B                                  \
 \                     {|NA,                                        \
 \                       Crypt (shrK A) {|NA, Key K|},              \
@@ -343,6 +343,19 @@
 qed "Spy_not_see_encrypted_key";
 
 
+(*A's guarantee.  The Oops premise quantifies over NB because A cannot know
+  what it is.*)
+goal thy 
+ "!!evs. [| Says A  B {|NA, Agent A, Agent B,                       \
+\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
+\           Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
+\           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;         \
+\           A ~: bad;  B ~: bad;  evs : otway |]                    \
+\        ==> Key K ~: analz (spies evs)";
+by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1);
+qed "A_gets_good_key";
+
+
 (**** Authenticity properties relating to NB ****)
 
 (*Only OR2 can have caused such a part of a message to appear.  We do not
@@ -363,8 +376,8 @@
 (** The Nonce NB uniquely identifies B's  message. **)
 
 goal thy 
- "!!evs. [| evs : otway; B ~: bad |]                    \
-\ ==> EX NA' A'. ALL NA A.                               \
+ "!!evs. [| evs : otway; B ~: bad |]  \
+\ ==> EX NA' A'. ALL NA A.            \
 \      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
 \      --> NA = NA' & A = A'";
 by (parts_induct_tac 1);
@@ -387,8 +400,8 @@
 (*If the encrypted message appears, and B has used Nonce NB,
   then it originated with the Server!*)
 goal thy 
- "!!evs. [| B ~: bad;  B ~= Spy;  evs : otway |]                        \
-\    ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs)             \
+ "!!evs. [| B ~: bad;  evs : otway |]                                    \
+\    ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs)                \
 \        --> (ALL X'. Says B Server                                      \
 \                       {|NA, Agent A, Agent B, X',                      \
 \                         Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|}  \
@@ -418,11 +431,11 @@
 (*Guarantee for B: if it gets a message with matching NB then the Server
   has sent the correct message.*)
 goal thy 
- "!!evs. [| B ~: bad;  B ~= Spy;  evs : otway;                    \
-\           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
-\           Says B Server {|NA, Agent A, Agent B, X',              \
+ "!!evs. [| Says B Server {|NA, Agent A, Agent B, X',              \
 \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
-\            : set evs |]                                          \
+\            : set evs;                                            \
+\           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
+\           B ~: bad;  evs : otway |]                              \
 \        ==> Says Server B                                         \
 \                 {|NA,                                            \
 \                   Crypt (shrK A) {|NA, Key K|},                  \
@@ -432,11 +445,21 @@
 qed "B_trusts_OR3";
 
 
-B_trusts_OR3 RS Spy_not_see_encrypted_key;
+(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
+goal thy 
+ "!!evs. [| Says B Server {|NA, Agent A, Agent B, X',              \
+\                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
+\             : set evs;                                           \
+\           Says S' B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;   \
+\           Notes Spy {|NA, NB, Key K|} ~: set evs;                \
+\           A ~: bad;  B ~: bad;  evs : otway |]                   \
+\        ==> Key K ~: analz (spies evs)";
+by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1);
+qed "B_gets_good_key";
 
 
 goal thy 
- "!!evs. [| B ~: bad;  evs : otway |]                           \
+ "!!evs. [| B ~: bad;  evs : otway |]                            \
 \        ==> Says Server B                                       \
 \              {|NA, Crypt (shrK A) {|NA, Key K|},               \
 \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->    \
@@ -454,11 +477,11 @@
   We could probably prove that X has the expected form, but that is not
   strictly necessary for authentication.*)
 goal thy 
- "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;       \
-\           Says A B {|NA, Agent A, Agent B,                                \
-\                      Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
-\           A ~: bad;  A ~= Spy;  B ~: bad;  evs : otway |]               \
-\        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,              \
+ "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;        \
+\           Says A  B {|NA, Agent A, Agent B,                                \
+\                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
+\           A ~: bad;  B ~: bad;  evs : otway |]                             \
+\        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,               \
 \                              Crypt (shrK B)  {|NA, NB, Agent A, Agent B|} |}\
 \            : set evs";
 by (blast_tac (claset() addSDs [A_trusts_OR4]