Abstract
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.
This work has been supported bythe Information SocietyT echnologies Programme, FET Open Assessment Project “AVISS” (Automated Verification of Infinite State Systems), IST-2000-26410.
The idea of regarding securityproto col analysis as a planning problem is not new. To our knowledge it is also been proposed in [1].
Chapter PDF
Similar content being viewed by others
Keywords
References
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.
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.
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.
D. Bolignano. Towards the formal verification of electronic commerce protocols. In Proceedings of the IEEE Computer Security Foundations Workshop, pages 133–146. 1997.
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.
John Clark and Jeremy Jacob. A Surveyof Authentication Protocol Literature: Version 1.0, 17. Nov. 1997. URL http://www.cs.york.ac.uk/~jac/papers/drareview.ps.gz.
Ernie Cohen. TAPS: A first-order verifier for cryptographic protocols. In Proceedings of The 13th Computer Security Foundations Workshop. IEEE Computer SocietyPress, 2000.
Sebastian Moedersheim David Basin and Luca Viganò. An on-the-fly model checker for security protocol analysis. forthcoming, 2002.
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 http://www.csl.sri.com/~millen/capsl/.
Danny Dolev and Andrew Yao. On the securityof public-key protocols. IEEE Transactions on Information Theory, 2(29), 1983.
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.
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.
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.
Mei Lin Hui and Gavin Lowe. Fault-preserving simplifying transformations for security protocols. Journal of Computer Security, 9(1/2):3–46, 2001.
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.
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.
Gawin Lowe. Casper: a compiler for the analysis of security protocols. Journal of Computer Security, 6(1):53–84, 1998. See also http://www.mcs.le.ac.uk/~gl7/Security/Casper/.
Catherine Meadows. The NRL protocol analyzer: An overview. Journal of Logic Programming, 26(2):113–131, 1996. See also http://chacs.nrl.navy.mil/projects/crypto.html.
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.
L.C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6(1):85–128, 1998.
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.
H. Zhang. SATO: An efficient propositional prover. In William McCune, editor, Proceedings of CADE 14, LNAI 1249, pages 272–275. Springer-Verlag, Heidelberg, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Armando, A., Compagna, L. (2002). Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning. In: Peled, D.A., Vardi, M.Y. (eds) Formal Techniques for Networked and Distributed Sytems — FORTE 2002. FORTE 2002. Lecture Notes in Computer Science, vol 2529. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36135-9_14
Download citation
DOI: https://doi.org/10.1007/3-540-36135-9_14
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00141-6
Online ISBN: 978-3-540-36135-0
eBook Packages: Springer Book Archive