// GJM 
  
 A,B,T :              principal                               
 C :                  msg                                     
 PCS :                (principal,msg,principal,principal):msg 
 S-SIG :              (principal,msg):msg                     
 TP-SIG :             (principal,msg):msg                     
 resolved,aborted :   bool                                    
 abort :              msg                                     
  
  
 Exchange-1.    A -> B  :   PCS(A,C,B,T)                                
                                                    
 Exchange-2.    B -> A  :   PCS(B,C,A,T)                                
                                                    
 Exchange-3.    A -> B  :   S-SIG(A,C)                                  
                                                    
 Exchange-4.    B -> A  :   S-SIG(B,C)                                  
                                                    
 Abort-1.       A -> T  :   S-SIG(A,[C,A,B,abort])                      
                                                    
 Abort-2.       T -> A  :   if (resolved) then S-SIG(B,C) else
S-SIG(T,S-SIG(A,[C,A,B,abort]))                               
 Resolve-A-1.   A -> T  :   [PCS(B,C,A,T),S-SIG(A,C)]                   
                                                    
 Resolve-A-2.   T -> A  :   if (aborted) then
S-SIG(T,S-SIG(A,[C,A,B,abort])) else if (resolved) S-SIG(B,C) else
TP-SIG(B,C) 
 Resolve-B-1.   B -> T  :   [PCS(A,C,B,T),S-SIG(B,C)]                   
                                                    
 Resolve-B-2.   T -> B  :   if (aborted) then
S-SIG(T,S-SIG(A,[C,A,B,abort])) else if (resolved) S-SIG(A,C) else
TP-SIG(A,C) 
   
 // 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).