// Bull's Authentication Protocol 
  
 A, B, C, S :      principal                  
 Kab, Kbc :        fresh symkey               
 Na, Nb, Nc :      fresh number               
 Kas, Kbs, Kcs :   symkey                     
 h :               message, symkey -> message 
  
  A computes Xa = h((A,B,Na),Kas), (A,B,Na) 
 1.   A -> B  :   Xa 
  
  B computes Xb = h((B,C,Nb,Xa),Kbs), (B,C,Nb,Xa)
  
 2.   B -> C  :   Xb 
  
  C computes Xc = h((C,S,Nc,Xb),Kcs), (C,S,Nc,Xb)
  
 3.   C -> S  :   Xc 
  
  
 4.   S -> C  :   A, B, Kab xor h(Na,Kas), {A,B,Na}Kab, 
                  B, A, Kab xor h(Nb,Kbs), {B,A,Nb}Kab, 
                  B, C, Kbc xor h(Nb,Kbs), {B,C,Nb}Kbc, 
                  C, B, Kbc xor h(Nc,Kcs), {C,B,Nc}Kbc  
 5.   C -> B  :   A, B, Kab xor h(Na,Kas), {A,B,Na}Kab, 
                  B, A, Kab xor h(Nb,Kbs), {B,A,Nb}Kab, 
                  B, C, Kbc xor h(Nb,Kbs), {B,C,Nb}Kbc  
 6.   B -> A  :   A, B, Kab xor h(Na,Kas), {A,B,Na}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).