Decidability of Parameterised Dolev-Yao Secrecy

Computer Science > Cryptography and Security [Submitted on 3 Aug 2026] Decidability of Parameterised Dolev-Yao Secrecy Ioana Boureanu, R. Ramanujam, Srinibas Swain We study the verification of parameterised secrecy for cryptographic protocols in the Dolev-Yao model, where the number of protocol sessions is unbounded and treated as a parameter. This differs fundamentally from classical Dolev-Yao secrecy, which asks whether a protocol leaks a secret irrespective of the number of executions; our question is whether secrecy holds uniformly across all system sizes, where such a size is a parameter. This parameterised perspective captures how attacks scale with the number of participants and provides a formal basis for the empirical effectiveness of small-instance analysis. Secrecy (parameterised or not) is undecidable in general, even under bounded freshness or bounded message size. We identify two structural restrictions that make parameterised secrecy decidable: (i) global bounded freshness per role, and (ii) a Dolev-Yao intruder restricted to well-typed substitutions. Under these assumptions, protocol executions admit a finite representation up to a collapsing map on agents and terms. Our main result is that parameterised secrecy is decidable in this setting. We obtain a cut-off theorem: secrecy violations in systems with arbitrarily many sessions are always witnessed in systems of bounded size. The cut-off is self-contained; more strongly, the induced transition system forms a well-structured transition system (WSTS) under a bound-based ordering, so secrecy also reduces to a coverability problem in WSTS. This provides a structural explanation for the existence of finite witnesses in symbolic protocol analysis and connects Dolev-Yao verification with parameterised verification techniques. Subjects: Cryptography and Security (cs.CR); Computational Complexity (cs.CC) Cite as: arXiv:2608.02838 [cs.CR]   (or arXiv:2608.02838v1 [cs.CR] for this version)   https://doi.org/10.48550/arXiv.2608.02838 Focus to learn more Submission history From: Ioana Boureanu [view email] [v1] Mon, 3 Aug 2026 19:51:46 UTC (263 KB) Access Paper: view license Current browse context: cs.CR < prev   |   next > new | recent | 2026-08 Change to browse by: cs cs.CC References & Citations NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)