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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Carlucci Aiello, L., Massacci, F.: Verifying security protocols as planning in logic programming. ACM Trans. on Computational Logic 2(4), 542–580 (2001)
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)
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)
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)
Basin, D., Moedersheim, S., Viganò, L.: An On-the-Fly Model- Checker for security protocol analysis (2003) (forthcoming)
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)
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)
Cervesato, I., Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: CSFW, pp. 55–69 (1999)
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)
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
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)
Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Transactions on Information Theory 2(29) (1983)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
Weld, D.S.: Recent advances in AI planning. AI Magazine 20(2), 93–123 (1999)
Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol. 1249, pp. 272–275. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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