AI 中文总结
该研究在Dolev-Yao模型下，针对无界会话的密码协议，确定使参数化保密性可判定的结构限制，得出截止定理，将其归约为WSTS的覆盖性问题，为符号协议分析提供结构解释并关联两类验证技术。
AI 中文摘要
我们在Dolev-Yao模型中研究密码协议的参数化保密性验证，其中协议会话的数量是无界的，被视为一个参数。这与经典的Dolev-Yao保密性有着根本区别，经典Dolev-Yao保密性关注协议是否会泄露秘密，而不考虑执行次数；我们的问题是，在所有系统规模下，保密性是否都能一致成立，其中该规模是一个参数。这种参数化视角捕捉了攻击如何随参与者数量扩展的情况，并为小实例分析的经验有效性提供了形式化基础。保密性（无论是参数化的还是非参数化的）在一般情况下是不可判定的，即使在新鲜度有界或消息大小有界的情况下也是如此。我们确定了两种使参数化保密性可判定的结构限制：(i) 每个角色的全局有界新鲜度，以及(ii) 受限于良类型替换的Dolev-Yao入侵者。在这些假设下，协议执行可以通过代理和项上的折叠映射获得有限表示。我们的主要结果是，在该设定下参数化保密性是可判定的。我们得到一个截止定理：具有任意多会话的系统中的保密性违反，总能在有界规模的系统中被发现。该截止是自包含的；更重要的是，诱导的转换系统在基于界限的序下形成良结构转换系统（WSTS），因此保密性也可归约为WSTS中的覆盖性问题。这为符号协议分析中有限见证的存在提供了结构解释，并将Dolev-Yao验证与参数化验证技术联系起来。
英文摘要
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.
