《通信网安全理论与技术》课程第7讲《安全协议形式化分析与设计》.ppt

BAN逻辑：推理规则 密钥与秘密共享规则 共享密钥和共享秘密具有对称性 规则1 规则2 BAN逻辑：推理规则 密钥与秘密共享规则 共享密钥和共享秘密具有对称性 规则3 规则4 内容提要 安全协议存在安全缺陷 安全协议形式化分析 类BAN逻辑形式化分析 例子：对NSSK认证协议的BAN逻辑分析 对NSSK认证协议的BAN逻辑分析——分析步骤 BAN逻辑的分析步骤 对协议的进行理想化 将协议的实际消息转换成BAN逻辑的公式 给出协议初始状态及其所基于的假设 对协议进行解释——注释 将形如P→Q: X的协议步骤转换成形如Q△X的逻辑语言 形式化说明协议将达成的安全目标 应用公理和推理规则以及协议会话事实和假设，从协议的开始进行推证直至验证协议是否满足其最终运行目标 对NSSK认证协议的BAN逻辑分析——理想化协议 协议的理想化 目的 非形式化的符号表达非常模糊 示例一 理想化之前：A-B:{A, kAB}kBS 告诉B(它知道kBS) kAB是它和A的通信秘钥 理想化之后： 对NSSK认证协议的BAN逻辑分析——理想化协议 协议的理想化 理想化的一些简单的指导方针 如果任何时候接收者得到一个真实消息m后能推导出发送者必须相信X，那么m能被解释成一个公式X 现实中的随机数被转化为任意的新公式 假定在整个过程中发送者都相信这些公式：XY 把Y作为一个秘密使用，仅当该秘密用作身份证明时有效 出于实用性目的，每个主体总是相信它作为消息产生的公式 对NSSK认证协议的BAN逻辑分析——理想化协议 协议的注释 在协议执行过程中，一系列关于各个主体的信条和所看到的内容的说明 发送第一条消息以前的公式表示各主体在协议开始时的信条——初始假设 各主体之间共享了哪些密钥 那些主体能产生新鲜的随机数 哪些主体在哪方面被信任 合法注释的主要规则 如果在P-Q: Y 之前X成立，则之后X和Q△Y都成立 如果根据推理规则，能从已知的X推到出Y，则X成立时Y必然成立 如果能从X得到Y ，则X成立时Y也成立 对NSSK认证协议的BAN逻辑分析——分析NS协议 Needham-Schroeder(NS)协议 A-S: A, B , Na S-A: {Na, B, {kab, A}kbs}kas A-B: {kab, A}kbs B-A: {Nb}kab A-B: {Nb - 1}kab 对NSSK认证协议的BAN逻辑分析——分析NS协议 理想化协议 对NSSK认证协议的BAN逻辑分析——分析NS协议 初始假设 对NSSK认证协议的BAN逻辑分析——分析NS协议 注释NS协议 对NSSK认证协议的BAN逻辑分析——分析NS协议 NS协议的目标公式 对NSSK认证协议的BAN逻辑分析——分析NS协议 BAN逻辑的推导过程 对NSSK认证协议的BAN逻辑分析——分析NS协议 BAN逻辑的推导过程 对NSSK认证协议的BAN逻辑分析——分析NS协议 重新审视对NS协议的分析 A-S: A, B , Na S-A: {Na, B, {kab, A}kbs}kas A-B: {kab, A}kbs B-A: {Nb}kab A-B: {Nb - 1}kab 假设kab泄露 攻击者在第三步冒充A重发消息 攻击者截获第四步消息 攻击者构造第五步消息 攻击者成功建立一个冒名顶替的会话密钥 假设条件的合理性至关重要： END 第七讲:安全协议形式化分析与设计 主讲人：xxx xxx系 * 《通信网安全理论与技术》课程 实践性 通信安全保障 协议安全设计 理论和技术基础 前导性 8. 课程体系及主要内容——讲解内容 通信网安全现状、趋势与策略——第1讲 通信网技术基础与安全体系——第2讲 通信网安全基础理论与技术(密码学、攻击与防御技术)——第3讲 网络安全协议理论设计与分析 认证协议以及密钥建立协议——第4讲 数字签名与阈下信道设计——第5讲 零知识证明及其安全协议构造——第6讲 安全协议形式化分析与设计——第7讲 典型的网络安全协议(IPSec协议、Kerberos协议、 Radius/AAA协议) ——第8～10讲 通信网安全保障技术——第11讲 无线网络安全性增强技术(WLAN为主)——第12讲 网络防火墙与入侵防御技术——第13讲 网络安全实现方案设计与分析——第14讲 内容提要 安全协议存在安全缺陷 安全协议形式化分析 类BAN逻辑形式化分析 例子：对NSSK认证协议的BAN逻辑分析 安全协议存在安全缺陷——原因 目前安全协议因如下原因，都存在一些安全缺陷： 对于其目的、需求和概念没有明确认识和准确描述 运行环境复杂，攻击者无处不在，其攻击能力强、手段多 协议设计者误解或者采用了不恰当的技术 很多安全缺陷并不显而易见，必须采用一定的分析