@InCollection{ArmandoCompagnaGanty03-long,
  author    = {A.~Armando and L.~Compagna and P.~Ganty},
  title     = "{SAT-based Model-Checking of Security Protocols using
                Planning Graph Analysis}", 
  booktitle = {Proceedings of the 12th International Symposium of Formal Methods Europe (FME)}, 
  publisher = {Springer-Verlag},
  series    = {LNCS 2805},
  editor    = {Araki, K. and Gnesi, S. and Mandrioli, D.},
  pages     = "875--893",
  year      = 2003,
  url       = "http://www.mrg.dist.unige.it/~compa/papers/FME-2003/paper.ps",
  abstract  = "In previous work we showed that automatic SAT-based model-checking    
	       techniques based on a reduction of protocol insecurity problems to    
	       satisfiability problems in propositional logic (SAT) can be used      
	       effectively to find attacks on security protocols.  The approach      
	       results from the combination of a reduction of protocol insecurity    
	       problems to planning problems and well-known SAT-reduction            
	       techniques, called linear encodings, developed for planning.          
	       Experimental results confirmed the effectiveness of the approach but  
	       also showed that the time spent to generate the SAT formula largely   
	       dominates the time spent by the SAT solver to check its               
	       satisfiability.  Moreover, the SAT instances generated by the tool    
	       get of unmanageable size on the most complex protocols.  In this      
	       paper we explore the application of the Graphplan-based encoding      
	       technique to the analysis of security protocols and present           
	       experimental data showing that Graphplan-based encodings are          
	       considerably (i.e.up to 2 orders of magnitude) smaller than        
	       linear encodings.  These results confirm the effectiveness of the     
	       SAT-based approach to the analysis of security protocols and pave     
	       the way to its application to large protocols arising in practical    
	       applications.",
}