// Gong 
  
 A, B, S :      principal                                
 Na, Nb, Ns :   number                                   
 Pa, Pb :       number                                   
 K, Ha, Hb :    number                                   
 f1 :           number, number, number, number -> number 
 f2 :           number, number, number, number -> number 
 f3 :           number, number, number, number -> number 
 g :            number, number, number, number -> number 
 xor :          number,number -> number                  
                                                         
 alias K = f1(Ns,Na,B,Pa)                                
 alias Ha = f2(Ns,Na,B,Pa)                               
 alias Hb = f3(Ns,Na,B,Pa)                               
  
  
 1.   A -> B  :   A, B, Na                       
 2.   B -> S  :   A, B, Na, Nb                   
 3.   S -> B  :   Ns, xor(f1(Ns, Nb, A, Pb), K), 
                  xor(f2(Ns, Nb, A, Pb), Ha),    
                  xor(f3(Ns, Nb, A, Pb), Hb),    
                  g(K, Ha, Hb, Pb)               
 4.   B -> A  :   Ns, Hb                         
 5.   A -> B  :   Ha                             
   
 // 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).