1.3.1 按攻击模型分类（Dolev-Yao vs. 计算模型）

文档摘要

1.3.1 按攻击模型分类（Dolev-Yao vs. 计算模型） 1.3.1 按攻击模型分类（Dolev-Yao vs. 计算模型）在密码协议的形式化分析中，攻击模型的选择直接决定了验证的粒度、安全性的边界以及实现的复杂度。当前主流的两种攻击模型——Dolev-Yao 模型与计算模型（Computational Model）——分别代表了符号化抽象与概率性精确的两个极端。它们并非互斥，而是互补：前者用于快速验证协议逻辑结构的合理性，后者用于评估其在现实世界中的实际安全性。然而，许多工程师在工程实践中往往混淆二者适用场景，或仅停留在“知道有这两种模型”的层面，却未能深入理解其背后的实现机制、验证工具链、参数配置逻辑，更遑论在真实项目中灵活切换与组合使用。