本文研究Dolev-Yao模型中密码协议的参数化保密性验证问题。经典Dolev-Yao保密性问题询问协议是否无论执行多少次都不会泄露秘密，而参数化保密性则要求保密性在所有可能的系统规模（即参与者数量）上一致成立，其中规模被视为参数。这一视角能够刻画攻击如何随参与者数量扩展，并为小型实例分析在实践中的有效性提供了形式化基础。文章指出，即使在有界新鲜性或有界消息大小的限制下，一般意义上的参数化保密性也是不可判定的。然而，作者识别出两种使问题可判定的结构性限制：(i) 每个角色的全局有界新鲜性；(ii) Dolev-Yao入侵者被限制为良类型替换。在这些假设下，协议执行可通过一个对代理和项的折叠映射获得有限表示。主要成果是证明了在该设定下参数化保密性是可判定的，并得到了一个cut-off定理：即使系统允许任意多的会话，任何保密性违反都必定在某个有界大小的系统中被观察到。该cut-off是自包含的；更严格地，诱导的转移系统在基于界限的偏序下构成良结构转移系统（WSTS），因此保密性问题还可归约为WSTS中的覆盖性问题。这一结果为符号协议分析中有限见证的存在性提供了结构性解释，并将Dolev-Yao验证与参数化验证技术联系起来。本文属于理论计算机科学范畴，主要贡献在于可判定性结论和新的验证方法，对密码协议的形式化分析与验证具有重要理论意义。