Decidability of Parameterised Dolev-Yao Secrecy
TL;DR
A cut-off theorem is obtained: secrecy violations in systems with arbitrarily many sessions are always witnessed in systems of bounded size, so secrecy also reduces to a coverability problem in WSTS.
Abstract
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.