diff -r 0c723635b9e6 -r 8d8344bcf98a src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Thu Jan 23 18:13:07 1997 +0100
+++ b/src/HOL/Auth/Recur.thy	Thu Jan 23 18:14:20 1997 +0100
@@ -27,8 +27,8 @@
              PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|};
              B ~= Server |]
           ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, 
-               {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
-                 Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
+               {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
+                 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
                  RA|},
                KBC)
               : respond evs"
@@ -80,8 +80,7 @@
           ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
               # evs : recur lost"
 
-         (*The Server receives and decodes Bob's message.  Then he generates
-           a new session key and a response.*)
+         (*The Server receives Bob's message and prepares a response.*)
     RA3  "[| evs: recur lost;  B ~= Server;
              Says B' Server PB : set_of_list evs;
              (PB,RB,K) : respond evs |]
@@ -90,11 +89,12 @@
          (*Bob receives the returned message and compares the Nonces with
            those in the message he previously sent the Server.*)
     RA4  "[| evs: recur lost;  A ~= B;  
-             Says C' B {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
-                         Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, RA|}
-               : set_of_list evs;
              Says B  C {|XH, Agent B, Agent C, Nonce NB, 
                          XA, Agent A, Agent B, Nonce NA, P|} 
+               : set_of_list evs;
+             Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
+                         Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
+                         RA|}
                : set_of_list evs |]
           ==> Says B A RA # evs : recur lost"