Abstract
We study the control reachability problem in the Dolev-Yao model of cryptographic protocols when principals are represented by tail recursive processes with generated names. We propose a conservative approximation of the problem by reduction to a non-standard collapsed operational semantics and we introduce checkable syntactic conditions entailing the equivalence of the standard and the collapsed semantics. Then we introduce a conservative and decidable set-based analysis of the collapsed operational semantics and we characterize a situation where the analysis is exact.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
R. Amadio, D. Lugiez, and V. Vanackere. On the symbolic reduction of processes with cryptographic functions. Theoretical Computer Science (to appear). Also RR 4147, INRIA.
R. Amadio, W. Charatonik. On name generation and set-based analysis in the Dolev-Yao model. RR-INRIA 4379, January 2002.
R. Amadio, C. Meyssonnier. On the decidability of fragments of the asynchronous π-calculus. Journal of Nordic Computing (to appear). Also RRINRIA 4241.
W. Charatonik and A. Podelski. Set constraints with intersection. In Proc. 12th IEEE LICS, 1997.
W. Charatonik, A. Podelski, and J.-M. Talbot. Paths vs. trees in set-based program analysis. In Proc. 27th Annual ACM POPL, 2000.
H. Comon, V. Cortier, and J. Mitchell. Tree automata with one memory, set constraints, and ping-pong protocols. In Proc. ICALP, Springer Lecture Notes in Comp. Sci. 2076, 2001.
J. Clark and J. Jacob. A survey of authentication protocol literature: Version 1.0. Available at http://www-users.cs.york.ac.uk/~jac/ papers/drareview.ps.gz, 1997.
D. Dolev, S. Even, and R. Karp. On the security of ping-pong protocols. Information and Control, 55:57–68, 1982.
N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In Proc. Formal methods and security protocols, FLOC Workshop, Trento, 1999.
D. Dolev and A. Yao. On the security of public key protocols. IEEE Trans. on Information Theory, 29(2):198–208, 1983.
T. Genet and F. Klay. Rewriting for cryptographic protocol verification. In Proc. CADE, Springer Lecture Notes in Comp. Sci. 1831, 2000.
J. Goubault. A method for automatic cryptographic protocol verification. In Proc. FMPPTA, Springer-Verlag, 2000.
N. Heintze and J. Jaffar. A decision procedure for a class of set constraints (extended abstract). In Proc. 5th IEEE LICS, 1990.
N. Heintze and J. Jaffar. Set constraints and set-based analysis. In Proc. Workshop on Principles and Practice of Constraint Programming, Springer Lecture Notes in Comp. Sci. 874, 1994.
D. Monniaux. Abstracting cryptographic protocols with tree automata. In Proc. Static Analysis Symposium, Springer Lect. Notes in Comp. Sci., 1999.
M. Rusinowitch and M. Turuani Protocol insecurity with finite number of sessions is NP-complete. RR INRIA 4134, March 2001.
S. Stoller. A bound on attacks on authentication protocols. TR 526, Indiana University, CS Dept., july 1999.
J.-M. Talbot, Ph. Devienne, and S. Tison. Generalized definite set constraints. Constraints: An International Journal, 5(1–2):161–202, January 2000.
C. Weidenbach. Towards an automatic analysis of security protocols in first-order logic. In Proc. CADE 99.Springer Lect. Notes in Comp. Sci. (LNAI) 1632, 1999.
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
Amadio, R.M., Charatonik, W. (2002). On Name Generation and Set-Based Analysis in the Dolev-Yao Model. In: Brim, L., Křetínský, M., Kučera, A., Jančar, P. (eds) CONCUR 2002 — Concurrency Theory. CONCUR 2002. Lecture Notes in Computer Science, vol 2421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45694-5_33
Download citation
DOI: https://doi.org/10.1007/3-540-45694-5_33
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44043-7
Online ISBN: 978-3-540-45694-0
eBook Packages: Springer Book Archive