// Andrew Secure RPC 
  
 A, B :          principal      
 Kab, K'ab :     symkey         
 Na, Nb, N'b :   nonce          
 succ :          nonce -> nonce 
  
  
 1.   A -> B  :   A, {Na}Kab      
 2.   B -> A  :   {succNa, Nb}Kab 
 3.   A -> B  :   {succNb}Kab     
 4.   B -> A  :   {K'ab, N'b}Kab  
   
 // Security Protocols Open Repository 
 // http://www.lsv.ens-cachan.fr/spore 
   
-----------------------------------------------------------------------
  
   
              This document was translated from LaTeX by HeVeA
              (http://pauillac.inria.fr/~maranget/hevea/index.html).