《《通信网安全理论与技术》课程第7讲《安全协议形式化分析与设计》》由会员分享，可在线阅读，更多相关《《通信网安全理论与技术》课程第7讲《安全协议形式化分析与设计》（46页珍藏版）》请在金锄头文库上搜索。
1、 第七讲 :安全协议形式化分析与设计 主讲人： 2017年 2月 19日星期日 通信网安全理论与技术 课程 实践性 通信安全保障 协议安全设计 理论和技术基础 前导性 8. 课程体系及主要内容 讲解内容 通信网安全现状、趋势与策略 第 1讲 通信网技术基础与安全体系 第 2讲 通信网安全基础理论与技术 (密码学、攻击与防御技术 ) 第 3讲 网络安全协议理论设计与分析 认证协议以及密钥建立协议 第 4讲 数字签名与阈下信道设计 第 5讲 零知识证明及其安全协议构造 第 6讲 安全协议形式化分析与设计 第 7讲 典型的网络安全协议 ( 第 8 10讲 通信网安全保障技术 第 11讲 无线网络安全
2、性增强技术 ( 第 12讲 网络防火墙与入侵防御技术 第 13讲 网络安全实现方案设计与分析 第 14讲 内容提要 1. 安全协议存在安全缺陷 2. 安全协议形式化分析 3. 类 4. 例子：对 安全协议存在安全缺陷 原因 目前安全协议因如下原因，都存在一些安全缺陷 ： 对于其目的、需求和概念没有明确认识和准确描述 运行环境复杂，攻击者无处不在，其攻击能力强、手段多 协议设计者误解或者采用了不恰当的技术 很多安全缺陷并不显而易见，必须采用一定的分析手段才能发现和弥补 安全协议存在安全缺陷 常见缺陷 根据其产生的原因和相应的攻击方法，安全缺陷主要有： 基本协议缺陷： 指在设计中没有或者很少防范攻
3、击者的攻击而引发的协议缺陷 例如：使用公钥密码系统加密交换消息时，不能预防中间人攻击 口令 /密钥猜测缺陷： 指用户选择一些常用词作为其口令，而导致攻击者能进行口令猜测攻击；或者选取了不安全的伪随机数生成算法构造密钥，使攻击者能够恢复该密钥 安全协议存在安全缺陷 常见缺陷 陈旧消息缺陷： 指设计中对消息的新鲜性没有充分考虑，从而使攻击者能够进行消息重放攻击，包括消息源的攻击、消息目的的攻击等 并行会话缺陷： 指协议对并行会话攻击缺乏防范，从而导致攻击者通过交换适当的协议消息能够获得所需要的信息。包括并行会话单角色缺陷、并行会话多角色缺陷等 内部协议缺陷： 指协议的可达性存在问题，协议的参与者中
4、至少有一方不能够完成所有必需的动作而导致的缺陷 密码系统缺陷： 指协议中使用的密码算法和安全协议导致协议不能完全满足所要求的机密性、完整性等需求而产生的缺陷 内容提要 1. 安全协议存在安全缺陷 2. 安全协议形式化分析 3. 类 4. 例子：对 安全协议形式化分析 需求 从前面的认证协议、密钥建立协议来看，几乎所有协议都有安全漏洞 迫切需要一套协议的安全分析方法，以指导协议设计 安全协议形式化分析就是一种正规的、标准的方法，可有效检查协议是否满足其安全目标 形式化分析被视作分析协议安全的有效工具 安全协议形式化分析 主要技术 现有的安全协议形式化分析技术主要有四种： 逻辑方法： 采用基于信仰
5、和知识逻辑的形式分析方法，比如以 通用形式化分析方法： 采用一些通用的形式分析方法来分析安全协议，例如应用 模型检测方法： 基于代数方法构造一个运行协议的有限状态系统模型，再利用状态检测工具来分析安全协议 定理证明方法： 将密码协议的安全行作为定理来证明，这是一个新的研究热点 内容提要 1. 安全协议存在安全缺陷 2. 安全协议形式化分析 3. 类 4. 例子：对 类 在众多协议形式化分析方法中，其中最具有影响的是 1989年由 成功地对 到了其中已知的和未知的漏洞 由此，激发了密码研究者对密码协议形式分析的兴趣并导致许多密码协议形式分析方法的产生 象层次 上讨论认证协议的安全行，而不考虑其具
6、体实现的安全缺陷和因加密体制而引发的协议缺陷 类 它是一种基于主体信念以及用于从已知信念推出新的信念的推理规则的逻辑 基本原理： 它可形式化定义协议的目标，并确定协议初始时刻各参与者的知识和信任，通过协议里消息的发送和接收步骤产生新知识，运用推导规则来得到目标信任和知识 如果得到最终的关于知识和信任的语句集里不包含所要得到的信任和知识的语句时，就表明协议存在安全缺陷 即：通过相互发送和接收消息，协议双方能否从最初的信念逐渐发展到协议运行最终要达到的目的 类 对 人们发现 能还不够完善，对协议中某些性能的推理能力有限，因此各国学者又提出了许多修改和扩充意见，其中较为著名的有： 它们统称为 类 对
7、 通过新增加的逻辑构件与规则，推广了 增加了“拥有密钥”的表达式，增加了 在 分一个主体收到的消息和一个主体可用的消息 在 一步区分一个主体自己生成的消息和其它消息 在 理想化协议中保留明文；而在 文在认证过程中不起作用 类 对 对 弃其中语义和实现细节的混合部分： 对某些逻辑构件引入更直接的定义，免除对诚实性进行隐含假设 简化了推理规则，所有的概念都独立定义，不与其它概念相混淆 整个逻辑只有两条基本推理规则： 则 ( 在 15 P c o n tr o P sa y s 类 对 其贡献在于：拓展了 而可以分析 它细化了认证协议的认证目标 类 对 虽形式化分析已获得了较大发展，但它还需在以下几
8、方面提高： 扩展现有的形式化分析工具的能力，使之不仅能 分析证明一个安全协议的不安全性 ，还 能证明协议的安全性 以及 分析和评测系统的安全性 为现有形式语言 构造完善的数学描述 ，并进行 严谨的理论证明 ；为各种协议形式化分析方法 形成统一的形式语言表述 ，以描述可利用的必要信息，并使之能够应用于一些新的应用协议的分析中 将形式化方法应用于 协议说明和协议涉及阶段 ，使之不仅仅用于分析具体的某个安全协议的安全性，从而可以极小的代价 尽可能早地发现错误 类 形式化分析的步骤： 首先需要进行“理想化”，即将协议的消息转换为 再根据具体情况进行合理的假设 再由逻辑的推理规则，根据理想化协议和假设进
9、行推理，推断协议能否完成预期的目标 类 密文块不能被篡改，也不能用几个小的密文块来拼凑成一个新的大的密文块 一个消息中的两个密文块被看作是分两次分别到达的 加密系统是完善的，只有知道密钥的主体才能解读密文消息，任何不知道密钥的主体都不能解读密文消息，也没有办法根据密文推导密钥 密文含有足够的冗余消息，解密者可以根据解密的结果来判断他是否已经正确解密 消息中有足够的冗余消息，使得主体可以判断该消息是否来源于自身 类 主体 密钥 公式，也被称为语句或命题 依照 P， Q， X， A， 协议的每个消息表达为该逻辑的一个公式 如随机数 ) X、 推导规则 “逻辑公式 ., 成立”记为 11, , ,
10、基本公式 语义 P、 Q 主体变量，泛指参与协议的各方 X 公式变量，泛指协议中消息的含义 P |= X ； 为真 P X ； 的消息并且读到 X P | X ； 的消息 P |= X ；相信 的真值的判定 #(X) 共享一个好的密钥 k：“好”代表 k(私钥是 这个私钥只有 分享秘密 X：这个秘密只有 P、 XK 用 后的消息 Y 结合 k P推理规则 消息含义规则 使主体推知其他主体发送过的消息 说明消息的出处 共享秘钥情况 公钥情况 共享秘钥情况 | , 1:| | P P X , Qk kP be li e v e s Q P P se e s XP be li e v e s Q 1| , 2:| | P X 1, b e l i e v e s Q P s e e s XP b e l i e v e s Q s a i d X|,3:| | P P X ,X YP b e li e v e s P Q P s e e s XP b e li e v e s Q s a 推理规则 临时值验证规则 使主体推知
