// Paulson's strengthened version of Yahalom 
  
 A, B, S :         principal    
 Na, Nb :          number fresh 
 Kas, Kbs, Kab :   key          
  
 A knows :   A, B, S, Kas      
 B knows :   B, S, Kbs         
 S knows :   S, A, B, Kas, Kbs 
  
  
 1.   A -> B  :    A, Na                                   
 2.   B -> S  :    B, Nb, {A, Na}Kbs                       
 3.   S -> A  :    Nb, {B, Kab, Na}Kas, {A, B, Kab, Nb}Kbs 
 4.   A -> B  :    {A, B, Kab, Nb}Kbs, {Nb}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).