src/HOL/Auth/Recur.thy

--- a/src/HOL/Auth/Recur.thy	Thu Dec 19 11:54:19 1996 +0100
+++ b/src/HOL/Auth/Recur.thy	Thu Dec 19 11:58:39 1996 +0100
@@ -77,7 +77,7 @@
 
          (*Alice initiates a protocol run.
            "Agent Server" is just a placeholder, to terminate the nesting.*)
-    NA1  "[| evs: recur lost;  A ~= B;  A ~= Server;
+    RA1  "[| evs: recur lost;  A ~= B;  A ~= Server;
              MA = {|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|}|]
           ==> Says A B {|Hash{|Key(shrK A),MA|}, MA|} # evs : recur lost"
 
@@ -85,7 +85,7 @@
            XA should be the Hash of the remaining components with KA, but
 		Bob cannot check that.
            P is the previous recur message from Alice's caller.*)
-    NA2  "[| evs: recur lost;  B ~= C;  B ~= Server;
+    RA2  "[| evs: recur lost;  B ~= C;  B ~= Server;
              Says A' B PA : set_of_list evs;  
              PA = {|XA, Agent A, Agent B, Nonce NA, P|};
              MB = {|Agent B, Agent C, Nonce (newN(length evs)), PA|} |]
@@ -93,14 +93,14 @@
 
          (*The Server receives and decodes Bob's message.  Then he generates
            a new session key and a response.*)
-    NA3  "[| evs: recur lost;  B ~= Server;
+    RA3  "[| evs: recur lost;  B ~= Server;
              Says B' Server PB : set_of_list evs;
              (0,PB,RB) : respond (length evs) |]
           ==> Says Server B RB # evs : recur lost"
 
          (*Bob receives the returned message and compares the Nonces with
 	   those in the message he previously sent the Server.*)
-    NA4  "[| evs: recur lost;  A ~= B;  
+    RA4  "[| evs: recur lost;  A ~= B;  
              Says C' B {|Agent B, 
                          Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
                          Agent B,