Skip to main content
SpringerLink
Log in

Abstraction-Driven SAT-based Analysis of Security Protocols

  • Conference paper
Theory and Applications of Satisfiability Testing (SAT 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2919))

Abstract

In previous work we proposed an approach to the automatic translation of protocol insecurity problems into propositional logic with the ultimate goal of building an automatic model-checker for security protocols based on state-of-the-art SAT solvers. In this paper we present an improved procedure based on an abstraction/refinement strategy which, by interleaving the encoding and solving phases, leads to a significant improvement of the overall performance of our model-checker.

We wish to thank Enrico Giuchiglia, Marco Maratea, Massimo Narizzano, and Armando Tacchella for many useful and stimulating discussions and their support in the use of the SIM solver. This work was partially funded by the FET Open EC Project AVISPA (IST-2001-39252), and by MIUR. Moreover, the second author was partially supported by the IHP-RTN EC project CALCULEMUS (HPRN-CT-2000-00102).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Carlucci Aiello, L., Massacci, F.: Verifying security protocols as planning in logic programming. ACM Trans. on Computational Logic 2(4), 542–580 (2001)

    Article  MathSciNet  Google Scholar 

  2. Armando, A., Basin, D., Bouallagui, M., Chevalier, Y., Compagna, L., Moedersheim, S., Rusinowitch, M., Turuani, M., Viganò, L., Vigneron, L.: The AVISS Security Protocols Analysis Tool. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 349. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  3. Armando, A., Compagna, L.: Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Armando, A., Compagna, L., Ganty, P.: Sat-based model-checking of security protocols. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  5. Basin, D., Denker, G.: Maude versus haskell: an experimental comparison in security protocol analysis. In: Futatsugi, K. (ed.). Electronic Notes in Theoretical Computer Science, vol. 36, Elsevier Science Publishers, Amsterdam (2001)

    Google Scholar 

  6. Basin, D., Moedersheim, S., Viganò, L.: An On-the-Fly Model-Checker for security protocol analysis (2003) (forthcoming)

    Google Scholar 

  7. Bolignano, D.: Towards the formal verification of electronic commerce protocols. In: Proc.of the IEEE Computer Security Foundations Workshop, pp. 133–146 (1997)

    Google Scholar 

  8. Cervesato, Durgin, Mitchell, Lincoln, Scedrov: Relating strands and multiset rewriting for security protocol analysis. In: PCSFW: Proceedings of The 13th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2000)

    Google Scholar 

  9. Chevalier, Y., Vigneron, L.: A Tool for Lazy Verification of Security Protocols. In: Proceedings of the Automated Software Engineering Conference (ASE 2001). IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

  10. Clark, J., Jacob, J.: A Survey of Authentication Protocol Literature: Version 1.0 (November 17, 1997), http://www.cs.york.ac.uk/~jac/papers/drareview.ps.gz

  11. Clarke, E., Gupta, A., Kukula, J., Strichman, O.: SAT based abstraction refinement using ILP and machine learning techniques. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 265. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  12. Cohen, E.: TAPS: A first-order verifier for cryptographic protocols. In: Proc. of The 13th Computer Security Foundations Workshop (2000)

    Google Scholar 

  13. Crawford, J.M., Anton, L.D.: Experimental results on the crossover point in satisfiability problems. In: Fikes, R., Lehnert, W. (eds.) Proceedings of the 11th AAAI Conference, California, pp. 21–27. AAAI Press, Menlo Park (1993)

    Google Scholar 

  14. Denker, G., Millen, J., Rueß, H.: The CAPSL Integrated Protocol Environment. Technical Report SRI-CSL-2000-02, SRI International, Menlo Park, CA (October 2000), Available at http://www.csl.sri.com/~millen/capsl/

  15. Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Transactions on Information Theory 2(29) (1983)

    Google Scholar 

  16. Donovan, B., Norris, P., Lowe, G.: Analyzing a library of security protocols using Casper and FDR. In: Proceedings of the Workshop on Formal Methods and Security Protocols (1999)

    Google Scholar 

  17. Ernst, M.D., Millstein, T.D., Weld, D.S.: Automatic SAT compilation of planning problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), pp. 1169–1177. Morgan Kaufmann Publishers, San Francisco (1997)

    Google Scholar 

  18. Giunchiglia, E., Maratea, M., Tacchella, A., Zambonin, D.: Evaluating search heuristics and optimization techniques in propositional satisfiability. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 347–363. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  19. Heather, Lowe, Schneider: How to prevent type flaw attacks on security protocols. In: PCSFW: Proceedings of The 13th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2000)

    Google Scholar 

  20. Jacquemard, F., Rusinowitch, M., Vigneron, L.: Compiling and Verifying Security Protocols. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol. 1955, pp. 131–160. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  21. Kautz, H., McAllester, D., Selman, B.: Encoding plans in propositional logic. In: KR 1996: Principles of Knowledge Representation and Reasoning, pp. 374–384. Morgan Kaufmann, San Francisco (1996)

    Google Scholar 

  22. Lowe, G.: Breaking and fixing the Needham-Shroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)

    Google Scholar 

  23. Lowe, G.: Casper: a compiler for the analysis of security protocols. Journal of Computer Security 6(1), 53–84 (1998)

    Google Scholar 

  24. Marrero, W., Clarke, E., Jha, S.: Model checking for security protocols (1997)

    Google Scholar 

  25. Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming 26(2), 113–131 (1996)

    Article  MATH  Google Scholar 

  26. Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using murphi. In: Proc. of IEEE Symposium on Security and Privacy, pp. 141–153 (1997)

    Google Scholar 

  27. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001 (2001)

    Google Scholar 

  28. Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Technical Report CSL-78-4, Xerox Palo Alto Research Center, Palo Alto, CA, USA (1978) (Reprinted June 1982)

    Google Scholar 

  29. Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1), 85–128 (1998)

    Google Scholar 

  30. Song, D.: Athena: A new efficient automatic checker for security protocol analysis. In: Proceedings of the 12th IEEE Computer Security Foundations Workshop (CSFW 1999), pp. 192–202. IEEE Computer Society Press, Los Alamitos (1999)

    Google Scholar 

  31. Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 272–275. Springer, Heidelberg (1997)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. DIST – Università degli Studi di Genova, Viale Causa 13, 16145, Genova, Italy

    Alessandro Armando & Luca Compagna

Authors
  1. Alessandro Armando
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Luca Compagna
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. DIST, Università di Genova, Viale Causa, 13, 16145, Genova, Italy

    Enrico Giunchiglia  & Armando Tacchella  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Armando, A., Compagna, L. (2004). Abstraction-Driven SAT-based Analysis of Security Protocols. In: Giunchiglia, E., Tacchella, A. (eds) Theory and Applications of Satisfiability Testing. SAT 2003. Lecture Notes in Computer Science, vol 2919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24605-3_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24605-3_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-20851-8

  • Online ISBN: 978-3-540-24605-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation