Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning

  • Alessandro Armando
  • Luca Compagna
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2529)


We provide a fullyautomatic translation from security protocol specifications into propositional logic which can be effectively used to find attacks to protocols. Our approach results from the combination of a reduction of protocol insecurity problems to planning problems and well-known SAT-reduction techniques developed for planning. We also propose and discuss a set of transformations on protocol insecurity problems whose application has a dramatic effect on the size of the propositional encoding obtained with our SAT-compilation technique. We describe a model-checker for security protocols based on our ideas and show that attacks to a set of well-known authentication protocols are quickly found bystate-of-the-art SAT solvers.


Network security Verification. 


  1. 1.
    Luigia Carlucci Aiello and Fabio Massacci. Verifying security protocols as planning in logic programming. ACM Transactions on Computational Logic, 2(4):542–580, October 2001.CrossRefMathSciNetGoogle Scholar
  2. 2.
    A. Armando, D. Basin, M. Bouallagui, Y. Chevalier, L. Compagna, S. Moedersheim, M. Rusinowitch, M. Turuani, L. Viganò, and L. Vigneron. The AVISS Security Proto cols Analysis Tool. In 14th International Conference on Computer-Aided Verification (CAV’02). 2002.Google Scholar
  3. 3.
    David Basin and Grit Denker. Maude versus haskell: an experimental comparison in security protocol analysis. In Kokichi Futatsugi, editor, Electronic Notes in Theoretical Computer Science, volume 36. Elsevier Science Publishers, 2001.Google Scholar
  4. 4.
    D. Bolignano. Towards the formal verification of electronic commerce protocols. In Proceedings of the IEEE Computer Security Foundations Workshop, pages 133–146. 1997.Google Scholar
  5. 6.
    Cervesato, Durgin, Mitchell, Lincoln, and Scedrov. Relating strands and multiset rewriting for security protocol analysis. In PCSFW: Proceedings of The 13th Computer Security Foundations Workshop. IEEE Computer SocietyPress, 2000.Google Scholar
  6. 7.
    John Clark and Jeremy Jacob. A Surveyof Authentication Protocol Literature: Version 1.0, 17. Nov. 1997. URL
  7. 8.
    Ernie Cohen. TAPS: A first-order verifier for cryptographic protocols. In Proceedings of The 13th Computer Security Foundations Workshop. IEEE Computer SocietyPress, 2000.Google Scholar
  8. 9.
    Sebastian Moedersheim David Basin and Luca Viganò. An on-the-fly model checker for security protocol analysis. forthcoming, 2002.Google Scholar
  9. 10.
    Grit Denker, Jonathan Millen, and Harald Rueβ. The CAPSL Integrated Protocol Environment. Technical Report SRI-CSL-2000-02, SRI International, Menlo Park, CA, October 2000. Available at Scholar
  10. 11.
    Danny Dolev and Andrew Yao. On the securityof public-key protocols. IEEE Transactions on Information Theory, 2(29), 1983.Google Scholar
  11. 12.
    B. Donovan, P. Norris, and G. Lowe. Analyzing a libraryof security protocols using Casper and FDR. In Proceedings of the Workshop on Formal Methods and Security Protocols. 1999.Google Scholar
  12. 13.
    Michael D. Ernst, Todd D. Millstein, and Daniel S. Weld. Automatic SATcompilation of planning problems. In Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97), pages 1169–1177. Morgan Kaufmann Publishers, San Francisco, 1997.Google Scholar
  13. 14.
    Enrico Giunchiglia, Marco Maratea, Armando Tacchella, and Davide Zambonin. Evaluating search heuristics and optimization techniques in propositional satisfiability. In Rajeev Goré, Aleander Leitsch, and Tobias Nipkow, editors, Proceedings of IJCAR’2001, pages 347–363. Springer-Verlag, 2001.Google Scholar
  14. 15.
    Mei Lin Hui and Gavin Lowe. Fault-preserving simplifying transformations for security protocols. Journal of Computer Security, 9(1/2):3–46, 2001.Google Scholar
  15. 16.
    Florent Jacquemard, Michael Rusinowitch, and Laurent Vigneron. Compiling and Verifying Security Protocols. In M. Parigot and A. Voronkov, editors, Proceedings of LPAR 2000, LNCS 1955, pages 131–160. Springer-Verlag, Heidelberg, 2000.Google Scholar
  16. 17.
    Henry Kautz, David McAllester, and Bart Selman. Encoding plans in propositional logic. In Luigia Carlucci Aiello, Jon Doyle, and Stuart Shapiro, editors, KR’96: Principles of Knowledge Representation and Reasoning, pages 374–384. Morgan Kaufmann, San Francisco, California, 1996.Google Scholar
  17. 18.
    Gawin Lowe. Casper: a compiler for the analysis of security protocols. Journal of Computer Security, 6(1):53–84, 1998. See also Scholar
  18. 19.
    Catherine Meadows. The NRL protocol analyzer: An overview. Journal of Logic Programming, 26(2):113–131, 1996. See also Scholar
  19. 20.
    Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Cha.: Engineering an Efficient SAT Solver. In Proceedings of the 38th Design Automation Conference (DAC’01). 2001.Google Scholar
  20. 21.
    L.C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6(1):85–128, 1998.Google Scholar
  21. 22.
    D. Song. Athena: A new efficient automatic checker for securityproto col analysis. In Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW’ 99), pages 192–202. IEEE Computer SocietyPress, 1999.Google Scholar
  22. 23.
    H. Zhang. SATO: An efficient propositional prover. In William McCune, editor, Proceedings of CADE 14, LNAI 1249, pages 272–275. Springer-Verlag, Heidelberg, 1997.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Alessandro Armando
    • 1
  • Luca Compagna
    • 1
  1. 1.DIST - Università degli Studi di GenovaGenovaItaly

Personalised recommendations