Abstract
The design and verification of cryptographic protocols is a notoriously difficult task, even in abstract Dolev-Yao models. This is mainly due to several sources of unboundedness (size of messages, number of sessions, ...). In this paper, we characterize a class of protocols for which secrecy for an unbounded number of sessions is decidable. More precisely, we present a simple transformation which maps a protocol that is secure for a single protocol session (a decidable problem) to a protocol that is secure for an unbounded number of sessions.
Our result provides an effective strategy to design secure protocols: (i) design a protocol intended to be secure for one protocol session (this can be verified with existing automated tools); (ii) apply our transformation and obtain a protocol which is secure for an unbounded number of sessions. The proof of our result is closely tied to a particular constraint solving procedure by Comon-Lundh et al.
Work partly supported by ARA SSIA Formacrypt and CNRS/JST ICT “Cryptography and logic: Computer-checked security proofs”.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Arapinis, M., Delaune, S., Kremer, S.: From one session to many: Dynamic tags for security protocols. Research Report LSV-08-20, ENS Cachan, France, 30 pages (June 2008)
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)
Armando, A., et al.: The Avispa tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)
Beauquier, D., Gauche, F.: How to guarantee secrecy for cryptographic protocols. CoRR, abs/cs/0703140 (2007)
Bellare, M., Canetti, R., Krawczyk, H.: A modular approach to the design and analysis of authentication and key exchange protocols (extended abstract). In: Proc. 30th Annual ACM Symposium on the Theory of Computing (STOC 1998), pp. 419–428. ACM Press, New York (1998)
Blanchet, B., Podelski, A.: Verification of cryptographic protocols: Tagging enforces termination. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 136–152. Springer, Heidelberg (2003)
Clark, J., Jacob, J.: A survey of authentication protocol literature (1997)
Comon, H.: Résolution de contraintes et recherche d’attaques pour un nombre borné de sessions, http://www.lsv.ens-cachan.fr/~comon/CRYPTO/bounded.ps
Comon-Lundh, H., Cortier, V.: Security properties: two agents are sufficient. Science of Computer Programming 50(1-3), 51–71 (2004)
Cortier, V., Delaitre, J., Delaune, S.: Safely composing security protocols. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 352–363. Springer, Heidelberg (2007)
Cortier, V., Delaune, S.: Safely composing security protocols. Research Report LSV-08-06, ENS Cachan, France, 39 pages (March 2008)
Cortier, V., Warinschi, B., Zălinescu, E.: Synthesizing secure protocols. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 406–421. Springer, Heidelberg (2007)
Cortier, V., Zălinescu, E.: Deciding key cycles for security protocols. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS, vol. 4246, pp. 317–331. Springer, Heidelberg (2006)
Delaune, S.: Note: Constraint solving procedure, http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDD-fsttcs07-addendum.pdf
Dolev, D., Even, S., Karp, R.M.: On the security of ping-pong protocols. In: Proc. Advances in Cryptology (CRYPTO 1982), pp. 177–186 (1982)
Dolev, D., Yao, A.C.: On the security of public key protocols. In: Proc. of the 22nd Symposium on Foundations of Computer Science (FOCS 1981). IEEE Comp. Soc. Press, Los Alamitos (1981)
Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of bounded security protocols. In: Proc. Workshop on Formal Methods and Security Protocols (1999)
Heather, J., Lowe, G., Schneider, S.: How to prevent type flaw attacks on security protocols. In: Proc. 13th Computer Security Foundations Workshop (CSFW 2001), pp. 255–268. IEEE Comp. Soc. Press, Los Alamitos (2000)
Katz, J., Yung, M.: Scalable protocols for authenticated group key exchange. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 110–125. Springer, Heidelberg (2003)
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Lowe, G.: Towards a completeness result for model checking of security protocols. Journal of Computer Security 7(1) (1999)
Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proc. 8th ACM Conference on Computer and Communications Security (CCS 2001). ACM Press, New York (2001)
Ramanujam, R., Suresh, S.P.: Tagging makes secrecy decidable for 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 and composed keys is NP-complete. Theoretical Computer Science 299(1-3), 451–475 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arapinis, M., Delaune, S., Kremer, S. (2008). From One Session to Many: Dynamic Tags for Security Protocols. In: Cervesato, I., Veith, H., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2008. Lecture Notes in Computer Science(), vol 5330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89439-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-89439-1_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89438-4
Online ISBN: 978-3-540-89439-1
eBook Packages: Computer ScienceComputer Science (R0)