Skip to main content
SpringerLink
Log in

SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis

  • Conference paper
  • First Online:
FME 2003: Formal Methods (FME 2003)

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

Included in the following conference series:

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.

This work was partially funded by the IHP-RTN EC project CALCULEMUS (HPRN-CT-2000-00102), by the FET Open EC Project AVISPA (IST-2001-39252), and by the project "Convenzione per lo svolgimento di tesi di dottorato in una Network di istituzioni europee e mutuo riconoscimento del titolo di dottore di ricerca. (Dottorato in Ingegneria Elettronica e Informatica)" of MIUR.

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 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

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); Also presented at the FCS & Verify Workshops, Copenhagen, Denmark (July 2002)

    Google Scholar 

  4. Armando, A., Compagna, L.: Abstraction-driven SAT-based Analysis of Security Protocols. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 257–271. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

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

    Google Scholar 

  6. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  7. Blum, A., Furst, M.: Fast planning through planning graph analysis. In: Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI 1995), pp. 1636–1642 (1995)

    Google Scholar 

  8. Cervesato, I., Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: CSFW, pp. 55–69 (1999)

    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), France). IEEE Computer Society Press, Los Alamitos (2001); Long version available as Technical Report A01- R-140, LORIA, Nancy (France)

    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. Do, M.B., Srivastava, B., Kambhampati, S.: Investigating the effect of relevance and reachability constraints on SAT encodings of planning. Artificial Intelligence Planning Systems, 308–314 (2000)

    Google Scholar 

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

    Google Scholar 

  13. 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 

  14. Ernst, M.D., Millstein, T.D., Weld, D.S.: Automatic SATcompilation 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 

  15. 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 

  16. Heather, J., Lowe, G., Schneider, S.: 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 

  17. 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 

  18. 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 

  19. Kautz, H.A., Selman, B.: Unifying SAT-based and graph-based planning. In: Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI 1999), Stockholm, Sweden, July 31-August 6, pp. 318–325. Morgan Kaufmann, San Francisco (1999)

    Google Scholar 

  20. 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)

    Chapter  Google Scholar 

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

    Google Scholar 

  22. 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 

  23. 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 

  24. 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)

    Chapter  Google Scholar 

  25. Weld, D.S.: Recent advances in AI planning. AI Magazine 20(2), 93–123 (1999)

    Google Scholar 

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

    Chapter  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 & Pierre Ganty

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

  3. Pierre Ganty
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Communication Engineering, Graduate School of Information Science and Electrical Engineering, Kyushu University, 6-10-1-Hakozaki, Higashi-ku, 812-8581, Fukuoka, Japan

    Keijiro Araki

  2. Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo”, ISTI - CNR, Pisa, Italy

    Stefania Gnesi

  3. Dipartimento di Elettronica e Informazione, Politecnico di Milano, Italy

    Dino Mandrioli

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Armando, A., Compagna, L., Ganty, P. (2003). SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. FME 2003. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45236-2_47

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45236-2_47

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40828-4

  • Online ISBN: 978-3-540-45236-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation