网络安全协议的形式化分析与验证 作者 李建华 第一章 绪论.pptVIP

1.1 安全协议概述 安全协议的基本概念 安全协议的缺陷分析 安全协议的攻击手段 形式化分析方法的重要性 Needham－Schroeder公钥协议工作过程： （1）Alice→Bob: {A, NA}PK_Bob （2）Bob→Alice: {NA, NB}PK_Alice （3）Alice→Bob: {NB}PK_Bob G.Lowe于1996年证明该协议很容易遭到一种巧妙的攻击。 （1）Alice→Eve: {A, NA}PK_Eve （1′）Eve(Alice)→Bob: {A, NA} PK_Bob （2′）Bob→Eve(Alice): {NA, NB} PK_Alice （2）Eve→Alice: {NA, NB}PK_Alice （3）Alice→Eve: {NB}PK_Eve （3′）Eve(Alice)→Bob: {NB} PK_Bob 消息重放攻击是数据源认证和认证密钥建立协议的典型攻击。 防止重放攻击的常用机制是在消息中增加随机的新鲜值nonce、运行标识符或时戳等时间标记，但有一些设计巧妙的攻击会使得这些措施失效。比如，本攻击中旧密钥的泄露使得NA、NB毫无用处。 总结：上述内容通过对安全协议的攻击举例，使大家对各种协议攻击的类型、原理和主要做法等方面有了一个初步的概念。 随着技术的进步，还会产生更多类型的攻击，而且更多的是多种攻击方法的组合使用。 1.2 形式化技术基础 模态逻辑技术 模型检测技术 定理证明技术 1.3 形式化方法在安全协议验证中的应用 自20世纪80年代以来，安全协议的形式化分析逐渐成为信息安全研究领域中的主要方向和热点问题。 它通过创建严密的理论模型，对安全协议进行严格的数学和逻辑推导论证，以证明协议的安全属性。 从分析结论的严谨性、理论基础的完备性、推导过程的合理性、描述和分析方法的规范性、自动分析的可能性来看，安全协议的形式化分析方法都具有无可比拟的优势，也是安全协议分析研究走向成熟和规范的必经阶段。 1.3 形式化方法在安全协议验证中的应用 安全协议形式化理论发展现状 安全协议形式化方法发展趋势 1.网络安全协议的形式化分析技术 （1）攻击构造方法：按照所采用的理论基础可分为3类： 基于广义确认语言（General Purpose Validation Language）的方法， 代数简化理论模型（Algebraic Simplification Theoretic Model）的方法 设计特定专家系统（Special Purpose Expert System）的方法。 （2）推理构造方法 采用推理构造方法的最著名的形式化逻辑模型是BAN逻辑及其类BAN逻辑族。同时，人们提出了许多扩展的类BAN逻辑，如GNY逻辑、SVO逻辑和Kailar逻辑等 （3）证据构造方法 Bolignano首先提出了产生可读证据的途径 Paulson 集中推理构造方法中的协议消息确认思想和攻击构造方法中事件的概念，提出类似的解决途径 Schneider使用CSP语言提出了对认证属性进行分析和验证的一般途径，并得到了成功的应用。近年来，Schneider还提出了束空间（Strand Space）的概念  1.3.1 安全协议形式化理论发展现状 目前，形式化理论在安全协议验证中的应用主要集中在形式化分析、形式化设计及自动化工具开发3个方面。 1．网络安全协议的形式化分析技术，大体上有两种分类方法： 一种是按照所采用的形式化理论基础进行分类综述， 另一种是按照分析的过程进行分类，S.Gritzalis、D.Spinellis及P.Georgiadis等人据此进行了详细、全面的综述。 具体地说，形式化的分析方法主要采取攻击构造、推理构造和证据构造3种方法。 2．网络安全协议的形式化设计技术 目前进行形式化协议设计的思路主要有两种： 一种是研究用于协议设计的方法学，采用这种特定的方法学设计完成后的安全协议可以方便地进行形式化分析，如模块化方法和Fail-Stop协议概念等。 另一种应用更为广泛的设计思路是层次化设计方法，它相当于一个由多种抽象模型形成的堆栈，栈顶是协议设计者根据协议安全性能提出的协议抽象模型，协议设计的过程就是将该抽象模型逐层细化，直到最后得到协议的精确描述或者确切代码。 在层次化设计思想的基础上，产生了一些新的协议设计的方法，如Rudolph利用Asynchronous Product Automata设计新的安全协议，Buttyan等使用管道的概念进行安全协议设计等。另外，Guttman等人使用认证测试方法，以串空间模型为基础提出了一种用于协议设计的方法。 形式化的方法还没有形成完整、有效的理论模型。 3．网络安全协议的自动化分析与设计工具开发 开发自动化的协议分析和