Search papers, labs, and topics across Lattice.
This paper investigates the verification of parameterised secrecy in cryptographic protocols within the Dolev-Yao model, focusing on the implications of unbounded protocol sessions treated as a parameter. Unlike classical Dolev-Yao secrecy, which assesses whether a protocol leaks information regardless of execution count, this study establishes conditions under which parameterised secrecy becomes decidable, specifically through global bounded freshness and well-typed substitutions for intruders. The key finding is a cut-off theorem indicating that secrecy violations in systems with infinite sessions can be detected in systems of bounded size, linking symbolic protocol analysis to parameterised verification techniques.
Parameterised secrecy can be decisively verified under specific structural restrictions, revealing a surprising connection between symbolic analysis and finite witness existence.
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.
