Abstract
A limit to algorithmic verification of security protocols is posed by the fact that checking whether a security property such as secrecy is satisfied is undecidable in general. In this paper we introduce the class of well-founded protocols. It is designed to exclude what seems to be common to all protocols used in undecidability proofs: the protocol syntax ensures that honest information cannot be propagated unboundedly without the intruder manipulating it. We show that the secrecy property of leakiness is decidable for well-founded protocols.
This work is partially supported by the Niedersächsisches Vorab of the Volkswagen Foundation and the Ministry of Science and Culture of Lower Saxony as part of the Interdisciplinary Research Center on Critical Systems Engineering for Socio-Technical Systems.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Needham, R.: Prudent engineering practice for cryptographic protocols. IEEE Trans. Softw. Eng. 22(1), 6–15 (1996)
Arapinis, M., Duflot, M.: Bounding messages for free in security protocols. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 376–387. Springer, Heidelberg (2007)
Blanchet, B., Podelski, A.: Verification of Cryptographic Protocols: Tagging Enforces Termination. Theoretical Computer Science 333(1-2), 67–90 (2005), Special issue FoSSaCS 2003
Boyd, C., Mathuria, A.: Protocols for Authentication and Key Establishment. Springer (2003)
Chrétien, R., Cortier, V., Delaune, S.: Typing messages for free in security protocols: The case of equivalence properties. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 372–386. Springer, Heidelberg (2014)
Clark, J., Jacob, J.: A survey of authentication protocol literature: Version 1.0 (1997)
Comon-Lundh, H., Cortier, V., Zălinescu, E.: Deciding security properties for cryptographic protocols. application to key cycles. ACM Trans. Comput. Logic 11(9), 9:1–9:42 (2010)
Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security 14(1), 1–43 (2006)
Dolev, D., Yao, A.C.-C.: On the security of public key protocols (extended abstract). In: FOCS, pp. 350–357 (1981)
Dolev, S., Even, S., Karp, R.M.: On the security of ping-pong protocols. Inform. and Control 55(1-3), 57–68 (1982)
Dougherty, D., Guttman, J.: Decidability for lightweight diffie-hellman protocols. In: CSF 2014, pp. 217–231. IEEE Computer Society (2014)
Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Multiset rewriting and the complexity of bounded security protocols. J. of Computer Security 12(2), 247–311 (2004)
Even, S., Goldreich, O.: On the security of multi-party ping-pong protocols. In: Symposium on the Foundations of Computer Science, pp. 4–39. IEEE Computer Society (1983)
Fröschle, S.: From Security Protocols to Security APIS: Foundations and Verification. To appear in the Information Security and Cryptography series of Springer
Fröschle, S.: On well-founded security protocols. In: Joint Workshop on Foundations of Computer Security and Formal and Computational Cryptography (FCS-FCC 2014) (2014)
Guttman, J.D., Thayer, F.J.: Authentication tests and the structure of bundles. Theor. Comput. Sci. 283(2), 333–380 (2002)
Heintze, N., Tygar, J.D.: A model for secure protocols and their compositions. IEEE Transactions on Software Engineering 22, 2–13 (1996)
Lowe, G.: Towards a completeness result for model checking of security protocols. Journal of Computer Security 7(1), 89–146 (1999)
Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)
Ramanujam, R., Suresh, S.P.: A decidable subclass of unbounded security protocols. In: WITS 2003, pp. 11–20 (2003)
Sarukkai, S., Suresh, S.P.: Tagging makes secrecy decidable with unbounded nonces as well. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 363–374. Springer, Heidelberg (2003)
Ramanujam, R., Suresh, S.P.: Decidability of context-explicit security protocols. Journal of Computer Security 13(1), 135–165 (2005)
Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is NP-complete. In: CSFW 2001, pp. 174–187. IEEE Computer Society (2001)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fröschle, S. (2015). Leakiness is Decidable for Well-Founded Protocols. In: Focardi, R., Myers, A. (eds) Principles of Security and Trust. POST 2015. Lecture Notes in Computer Science(), vol 9036. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46666-7_10
Download citation
DOI: https://doi.org/10.1007/978-3-662-46666-7_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46665-0
Online ISBN: 978-3-662-46666-7
eBook Packages: Computer ScienceComputer Science (R0)