// KSL 
  
 A, B, S :              principal            
 Na, Nb, Nc, Ma, Mb :   number               
 Kas, Kbs, Kab, Kbb :   key                  
 Tb :                   generalizedTimestamp 
  
  
 1.   A -> B  :   Na, A                                         
 2.   B -> S  :   Na, A, Nb, B                                  
 3.   S -> B  :   {Nb, A, Kab}Kbs, {Na, B, Kab}Kas              
 4.   B -> A  :   {Na, B, Kab}Kas, {Tb, A, Kab}Kbb, Nc, {Na}Kab 
 5.   A -> B  :   {Nc}Kab                                       
                                                                
 6.   A -> B  :   Ma, {Tb, A, Kab}Kbb                           
 7.   B -> A  :   Mb, {Ma}Kab                                   
 8.   A -> B  :   {Mb}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).