第七章密码协议:72认证协议概述 722 Daley-Yao威胁模型与常见攻击 协议的安全性分析方法 逻辑分析法:基于信仰和知识对协议进行安全性研究,使用最广 泛,如BAN逻辑等 模型检测法:一种验证有限状态系统的自动化分析工具,采用非 专门的说明语言和验证工具来对协议建立模型并加以验证,如 cSP等 定理证明和专家系统方法:类似证明程序的正确性一样,将协议 的证明规约到证明一些循环不变式,基于计算复杂度理论 通用形式化分析方法:试图用一些通用的形式化方法来说明和分 析安全协议。如最弱前置谓词等方法,Petr网,代数方法等。 可证明安全的协议设计 基本思想类似于可证明安全的公钥密码算法 历忠毛孑技*字7.2.2 Daolev-Yao威胁模型与常见攻击 ⚫ 协议的安全性分析方法 ⚫ 逻辑分析法：基于信仰和知识对协议进行安全性研究，使用最广 泛，如BAN逻辑等 ⚫ 模型检测法：一种验证有限状态系统的自动化分析工具，采用非 专门的说明语言和验证工具来对协议建立模型并加以验证，如 CSP等 ⚫ 定理证明和专家系统方法：类似证明程序的正确性一样，将协议 的证明规约到证明一些循环不变式，基于计算复杂度理论 ⚫ 通用形式化分析方法：试图用一些通用的形式化方法来说明和分 析安全协议。如最弱前置谓词等方法，Petri网，代数方法等。 ⚫ 可证明安全的协议设计 ⚫ 基本思想类似于可证明安全的公钥密码算法 9/ 第七章 密码协议：7.2 认证协议概述