src/HOL/Auth/Recur.thy

              X: synth (analz (sees lost Spy evs)) |]
           ==> Says Spy B X  # evs : recur lost"
 
          (*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"
 
          (*Bob's response to Alice's message.  C might be the Server.
            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|} |]
           ==> Says B C {|Hash{|Key(shrK B),MB|}, MB|} # evs : recur lost"
 
          (*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, 
                          Crypt (shrK B) {|Key KAC, Agent C, Nonce NB|}, RA|}
                : set_of_list evs;