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

《《通信网安全理论与技术》课程第7讲《安全协议形式化分析与设计》课件.ppt》由会员分享，可在线阅读，更多相关《《通信网安全理论与技术》课程第7讲《安全协议形式化分析与设计》课件.ppt（46页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、 第七讲第七讲:安全协议形式化分析与设计安全协议形式化分析与设计主讲人：主讲人：xxxxxxxxxxxx系系10 10 四月四月 2023 2023通信网安全理论与技术通信网安全理论与技术课程课程实践性通信安全保障协议安全设计理论和技术基础前导性8.课程体系及主要内容讲解内容 通信网安全现状、趋势与策略通信网安全现状、趋势与策略第第第第1 1讲讲讲讲 通信网技术基础与安全体系通信网技术基础与安全体系第第第第2 2讲讲讲讲 通信网安全基础理论与技术通信网安全基础理论与技术(密码学、攻击与防御技术密码学、攻击与防御技术)第第第第3 3讲讲讲讲 网络安全协议理论设计与分析网络安全协议理论设计与分析

2、认证协议以及密钥建立协议认证协议以及密钥建立协议第第第第4 4讲讲讲讲 数字签名与阈下信道设计数字签名与阈下信道设计第第第第5 5讲讲讲讲 零知识证明及其安全协议构造零知识证明及其安全协议构造第第第第6 6讲讲讲讲 安全协议形式化分析与设计安全协议形式化分析与设计第第第第7 7讲讲讲讲 典型的网络安全协议典型的网络安全协议(IPSec(IPSec协议、协议、KerberosKerberos协议、协议、Radius/AAARadius/AAA协协议议)第第第第8 81010讲讲讲讲 通信网安全保障技术通信网安全保障技术第第第第1111讲讲讲讲 无线网络安全性增强技术无线网络安全性增强技术(WLA

3、N(WLAN为主为主)第第第第1212讲讲讲讲 网络防火墙与入侵防御技术网络防火墙与入侵防御技术第第第第1313讲讲讲讲 网络安全实现方案设计与分析网络安全实现方案设计与分析第第第第1414讲讲讲讲内容提要1.1.安全协议存在安全缺陷安全协议存在安全缺陷2.2.安全协议形式化分析安全协议形式化分析3.3.类类BANBAN逻辑形式化分析逻辑形式化分析4.4.例子：对例子：对NSSKNSSK认证协议的认证协议的BANBAN逻辑分析逻辑分析安全协议存在安全缺陷原因 目前安全协议因如下原因，都存在一些安全缺陷目前安全协议因如下原因，都存在一些安全缺陷：对于其目的、需求和概念没有明确认识和准确描述对于其

4、目的、需求和概念没有明确认识和准确描述 运行环境复杂，攻击者无处不在，其攻击能力强、手段多运行环境复杂，攻击者无处不在，其攻击能力强、手段多 协议设计者误解或者采用了不恰当的技术协议设计者误解或者采用了不恰当的技术 很多安全缺陷并不显而易见，必须采用一定的分析手段才能发现和很多安全缺陷并不显而易见，必须采用一定的分析手段才能发现和弥补弥补安全协议存在安全缺陷常见缺陷 根据其产生的原因和相应的攻击方法，安全缺陷主要有：根据其产生的原因和相应的攻击方法，安全缺陷主要有：基本协议缺陷：基本协议缺陷：基本协议缺陷：基本协议缺陷：指在设计中没有或者很少防范攻击者的攻击而引指在设计中没有或者很少防范攻击者

5、的攻击而引发的协议缺陷发的协议缺陷 例如：使用公钥密码系统加密交换消息时，不能预防中间人攻击例如：使用公钥密码系统加密交换消息时，不能预防中间人攻击 口令口令口令口令/密钥猜测缺陷：密钥猜测缺陷：密钥猜测缺陷：密钥猜测缺陷：指用户选择一些常用词作为其口令，而导致指用户选择一些常用词作为其口令，而导致攻击者能进行口令猜测攻击；或者选取了不安全的伪随机数生成攻击者能进行口令猜测攻击；或者选取了不安全的伪随机数生成算法构造密钥，使攻击者能够恢复该密钥算法构造密钥，使攻击者能够恢复该密钥安全协议存在安全缺陷常见缺陷 陈旧消息缺陷：陈旧消息缺陷：陈旧消息缺陷：陈旧消息缺陷：指设计中对消息的新鲜性没有充分

6、考虑，从而使指设计中对消息的新鲜性没有充分考虑，从而使攻击者能够进行消息重放攻击，包括消息源的攻击、消息目的的攻击者能够进行消息重放攻击，包括消息源的攻击、消息目的的攻击等攻击等 并行会话缺陷：并行会话缺陷：并行会话缺陷：并行会话缺陷：指协议对并行会话攻击缺乏防范，从而导致攻击指协议对并行会话攻击缺乏防范，从而导致攻击者通过交换适当的协议消息能够获得所需要的信息。包括并行会者通过交换适当的协议消息能够获得所需要的信息。包括并行会话单角色缺陷、并行会话多角色缺陷等话单角色缺陷、并行会话多角色缺陷等 内部协议缺陷：内部协议缺陷：内部协议缺陷：内部协议缺陷：指协议的可达性存在问题，协议的参与者中至少

7、指协议的可达性存在问题，协议的参与者中至少有一方不能够完成所有必需的动作而导致的缺陷有一方不能够完成所有必需的动作而导致的缺陷 密码系统缺陷：密码系统缺陷：密码系统缺陷：密码系统缺陷：指协议中使用的密码算法和安全协议导致协议不指协议中使用的密码算法和安全协议导致协议不能完全满足所要求的机密性、完整性等需求而产生的缺陷能完全满足所要求的机密性、完整性等需求而产生的缺陷 内容提要1.1.安全协议存在安全缺陷安全协议存在安全缺陷2.2.安全协议形式化分析安全协议形式化分析3.3.类类BANBAN逻辑形式化分析逻辑形式化分析4.4.例子：对例子：对NSSKNSSK认证协议的认证协议的BANBAN逻辑分

8、析逻辑分析安全协议形式化分析需求 从前面的认证协议、密钥建立协议来看，几乎所有协议都有安全漏从前面的认证协议、密钥建立协议来看，几乎所有协议都有安全漏洞洞 迫切需要一套协议的安全分析方法，以指导协议设计迫切需要一套协议的安全分析方法，以指导协议设计 安全协议形式化分析就是一种正规的、标准的方法，可有效检查安全协议形式化分析就是一种正规的、标准的方法，可有效检查协议是否满足其安全目标协议是否满足其安全目标 形式化分析被视作分析协议安全的有效工具形式化分析被视作分析协议安全的有效工具 安全协议形式化分析主要技术 现有的安全协议形式化分析技术主要有四种：现有的安全协议形式化分析技术主要有四种：逻辑方

9、法：逻辑方法：逻辑方法：逻辑方法：采用基于信仰和知识逻辑的形式分析方法，比如以采用基于信仰和知识逻辑的形式分析方法，比如以BANBAN逻辑为代表的类逻辑为代表的类BANBAN逻辑逻辑 通用形式化分析方法：通用形式化分析方法：通用形式化分析方法：通用形式化分析方法：采用一些通用的形式分析方法来分析安全采用一些通用的形式分析方法来分析安全协议，例如应用协议，例如应用PetriPetri网等网等 模型检测方法：模型检测方法：模型检测方法：模型检测方法：基于代数方法构造一个运行协议的有限状态系统基于代数方法构造一个运行协议的有限状态系统模型，再利用状态检测工具来分析安全协议模型，再利用状态检测工具来分

10、析安全协议 定理证明方法：定理证明方法：定理证明方法：定理证明方法：将密码协议的安全行作为定理来证明，这是一个将密码协议的安全行作为定理来证明，这是一个新的研究热点新的研究热点 内容提要1.1.安全协议存在安全缺陷安全协议存在安全缺陷2.2.安全协议形式化分析安全协议形式化分析3.3.类类BANBAN逻辑形式化分析逻辑形式化分析4.4.例子：对例子：对NSSKNSSK认证协议的认证协议的BANBAN逻辑分析逻辑分析类类BAN逻辑形式化分析逻辑形式化分析BAN逻辑形式化逻辑形式化 在众多协议形式化分析方法中，其中最具有影响的是在众多协议形式化分析方法中，其中最具有影响的是19891989年由年由

11、BurrowsBurrows、AbadiAbadi和和NeedhamNeedham提出的提出的BANBAN逻辑逻辑 成功地对成功地对NSNS协议，协议，KerberosKerberos等几个著名的协议进行了分析，找到等几个著名的协议进行了分析，找到了其中已知的和未知的漏洞了其中已知的和未知的漏洞 由此，激发了密码研究者对密码协议形式分析的兴趣并导致许由此，激发了密码研究者对密码协议形式分析的兴趣并导致许多密码协议形式分析方法的产生多密码协议形式分析方法的产生 BANBAN逻辑只在逻辑只在抽象层次抽象层次上讨论认证协议的安全行，而不考虑其具体上讨论认证协议的安全行，而不考虑其具体实现的安全缺陷和

12、因加密体制而引发的协议缺陷实现的安全缺陷和因加密体制而引发的协议缺陷类类BAN逻辑形式化分析逻辑形式化分析BAN逻辑形式化逻辑形式化 它是一种基于主体信念以及用于从已知信念推出新的信念的推理规它是一种基于主体信念以及用于从已知信念推出新的信念的推理规则的逻辑则的逻辑 基本原理：基本原理：它可形式化定义协议的目标，并确定协议初始时刻各参与者的知它可形式化定义协议的目标，并确定协议初始时刻各参与者的知识和信任，通过协议里消息的发送和接收步骤产生新知识，运用识和信任，通过协议里消息的发送和接收步骤产生新知识，运用推导规则来得到目标信任和知识推导规则来得到目标信任和知识 如果得到最终的关于知识和信任的

13、语句集里不包含所要得到的信如果得到最终的关于知识和信任的语句集里不包含所要得到的信任和知识的语句时，就表明协议存在安全缺陷任和知识的语句时，就表明协议存在安全缺陷 即：通过相互发送和接收消息，协议双方能否从最初的信念逐渐发即：通过相互发送和接收消息，协议双方能否从最初的信念逐渐发展到协议运行最终要达到的目的展到协议运行最终要达到的目的类类BAN逻辑形式化分析逻辑形式化分析对对BAN逻辑修改或扩充逻辑修改或扩充 人们发现人们发现BANBAN逻辑在分析某些协议和协议攻击时，功能还不够完善，逻辑在分析某些协议和协议攻击时，功能还不够完善，对协议中某些性能的推理能力有限，因此各国学者又提出了许多修对协

14、议中某些性能的推理能力有限，因此各国学者又提出了许多修改和扩充意见，其中较为著名的有：改和扩充意见，其中较为著名的有：GNYGNY逻辑逻辑 ATAT逻辑逻辑 VOVO逻辑和逻辑和SVOSVO逻辑逻辑 它们统称为它们统称为BANBAN类逻辑类逻辑类类BAN逻辑形式化分析逻辑形式化分析对对BAN逻辑修改或扩充逻辑修改或扩充 GNYGNY逻辑对逻辑对BANBAN逻辑作了如下重要改进与推进：逻辑作了如下重要改进与推进：通过新增加的逻辑构件与规则，推广了通过新增加的逻辑构件与规则，推广了BANBAN逻辑的应用范围逻辑的应用范围 增加了增加了“拥有密钥拥有密钥”的表达式，增加了的表达式，增加了GNYGNY

15、逻辑本身的表达能力逻辑本身的表达能力 在在GNYGNY逻辑中，区分一个主体收到的消息和一个主体可用的消息逻辑中，区分一个主体收到的消息和一个主体可用的消息 在在GNYGNY逻辑中，进一步区分一个主体自己生成的消息和其它消息逻辑中，进一步区分一个主体自己生成的消息和其它消息 在在GNYGNY逻辑的分析中，在理想化协议中保留明文；而在逻辑的分析中，在理想化协议中保留明文；而在BANBAN逻辑逻辑分析中，明文在认证过程中不起作用分析中，明文在认证过程中不起作用类类BAN逻辑形式化分析逻辑形式化分析对对BAN逻辑修改或扩充逻辑修改或扩充 ATAT逻辑逻辑 ATAT逻辑比逻辑比BANBAN逻辑更接近的模

16、态逻辑：逻辑更接近的模态逻辑：对对BANBAN逻辑中的定义和推理规则进行整理，抛弃其中语义和实现逻辑中的定义和推理规则进行整理，抛弃其中语义和实现细节的混合部分：细节的混合部分：对某些逻辑构件引入更直接的定义，免除对诚实性进行隐含假设对某些逻辑构件引入更直接的定义，免除对诚实性进行隐含假设 简化了推理规则，所有的概念都独立定义，不与其它概念相混淆简化了推理规则，所有的概念都独立定义，不与其它概念相混淆 整个逻辑只有两条基本推理规则：整个逻辑只有两条基本推理规则：MP MP 规则规则(modus pones)(modus pones)NecNec规则规则(necessitation)(neces

17、sitation)在在ATAT逻辑中有一条比逻辑中有一条比BANBAN逻辑更加直接的管辖公理逻辑更加直接的管辖公理A15A15类类BAN逻辑形式化分析逻辑形式化分析对对BAN逻辑修改或扩充逻辑修改或扩充 VOVO逻辑逻辑 其贡献在于：拓展了其贡献在于：拓展了BANBAN逻辑的应用范围。逻辑的应用范围。VOVO逻辑的设计目标就逻辑的设计目标就是增加分析是增加分析Diffie-HellmanDiffie-Hellman协议的能力，进而可以分析协议的能力，进而可以分析IETFIETF标准标准InternetInternet密钥交换协议密钥交换协议IKEIKE和和SSLSSL协议等协议等 它细化了认证

18、协议的认证目标它细化了认证协议的认证目标类类BAN逻辑形式化分析逻辑形式化分析对对BAN逻辑修改或扩充逻辑修改或扩充 虽形式化分析已获得了较大发展，但它还需在以下几方面提高：虽形式化分析已获得了较大发展，但它还需在以下几方面提高：扩展现有的形式化分析工具的能力，使之不仅能扩展现有的形式化分析工具的能力，使之不仅能分析证明一个安分析证明一个安分析证明一个安分析证明一个安全协议的不安全性全协议的不安全性全协议的不安全性全协议的不安全性，还，还能证明协议的安全性能证明协议的安全性能证明协议的安全性能证明协议的安全性以及以及分析和评测系统分析和评测系统分析和评测系统分析和评测系统的安全性的安全性的安全

19、性的安全性 为现有形式语言为现有形式语言构造完善的数学描述构造完善的数学描述构造完善的数学描述构造完善的数学描述，并进行，并进行严谨的理论证明严谨的理论证明严谨的理论证明严谨的理论证明；为各种协议形式化分析方法为各种协议形式化分析方法形成统一的形式语言表述形成统一的形式语言表述形成统一的形式语言表述形成统一的形式语言表述，以描述可，以描述可利用的必要信息，并使之能够应用于一些新的应用协议的分析中利用的必要信息，并使之能够应用于一些新的应用协议的分析中 将形式化方法应用于将形式化方法应用于协议说明和协议涉及阶段协议说明和协议涉及阶段协议说明和协议涉及阶段协议说明和协议涉及阶段，使之不仅仅用于，使

20、之不仅仅用于分析具体的某个安全协议的安全性，从而可以极小的代价分析具体的某个安全协议的安全性，从而可以极小的代价尽可能尽可能尽可能尽可能早地发现错误早地发现错误早地发现错误早地发现错误 类类BAN逻辑形式化分析逻辑形式化分析BAN逻辑形式化逻辑形式化 形式化分析的步骤：形式化分析的步骤：首先需要进行首先需要进行“理想化理想化”，即将协议的消息转换为，即将协议的消息转换为BANBAN逻辑中的逻辑中的公式公式 再根据具体情况进行合理的假设再根据具体情况进行合理的假设 再由逻辑的推理规则，根据理想化协议和假设进行推理，推断协再由逻辑的推理规则，根据理想化协议和假设进行推理，推断协议能否完成预期的目标

21、议能否完成预期的目标 类类BAN逻辑形式化分析逻辑形式化分析BAN逻辑形式化逻辑形式化 BANBAN逻辑系统的假设如下：逻辑系统的假设如下：密文块不能被篡改，也不能用几个小的密文块来拼凑成一个新密文块不能被篡改，也不能用几个小的密文块来拼凑成一个新的大的密文块的大的密文块一个消息中的两个密文块被看作是分两次分别到达的一个消息中的两个密文块被看作是分两次分别到达的加密系统是完善的，只有知道密钥的主体才能解读密文消息，加密系统是完善的，只有知道密钥的主体才能解读密文消息，任何不知道密钥的主体都不能解读密文消息，也没有办法根据任何不知道密钥的主体都不能解读密文消息，也没有办法根据密文推导密钥密文推导

22、密钥密文含有足够的冗余消息，解密者可以根据解密的结果来判断密文含有足够的冗余消息，解密者可以根据解密的结果来判断他是否已经正确解密他是否已经正确解密消息中有足够的冗余消息，使得主体可以判断该消息是否来源消息中有足够的冗余消息，使得主体可以判断该消息是否来源于自身于自身BANBAN逻辑还假设协议的参与主体是诚实的逻辑还假设协议的参与主体是诚实的 类类BAN逻辑形式化分析逻辑形式化分析BAN逻辑形式化逻辑形式化 BANBAN逻辑主要包含下面三种处理对象：逻辑主要包含下面三种处理对象：主体主体 密钥密钥 公式，也被称为语句或命题公式，也被称为语句或命题 依照依照BANBAN逻辑的惯例，逻辑的惯例，P

23、 P，QQ，R R等表示主体变量，等表示主体变量，K K表示密钥变量，表示密钥变量，X X，Y Y表示公式变量。表示公式变量。A A，B B表示主体，表示主体，S S表示服务器表示服务器 协议的每个消息表达为该逻辑的一个公式协议的每个消息表达为该逻辑的一个公式 N Na a、N Nb b、N Nc c代表具体的观点代表具体的观点(如随机数如随机数)X X、Y Y代表一般意义上的消息代表一般意义上的消息 推导规则推导规则“逻辑公式逻辑公式X X1 1,X X2 2,.,.,X Xn n成立则成立则Y Y成立成立”记为记为类类BAN逻辑形式化分析逻辑形式化分析BAN逻辑形式化逻辑形式化基本公式基本

24、公式语义语义P、Q主体变量，泛指参与协议的各方X公式变量，泛指协议中消息的含义P|=XP相信X；P相信X为真P XP看见X；P曾经收到过包含X的消息并且读到XP|XP曾经说过X；P曾经发送过包含X的消息P|=XP可以裁定X；相信P对于X的真值的判定#(X)X是新鲜的；X在当前协议运行前没有被发现过P和Q共享一个好的密钥k：“好”代表k依旧具有保密性P具有密钥公钥k(私钥是k-1)，这个私钥只有P以及他信任的人知道P和Q分享秘密X：这个秘密只有P、Q以及他们信任的人知道XK用k加密X后的消息YX与消息Y结合BAN逻辑：推理规则推理规则 消息含义规则消息含义规则消息含义规则消息含义规则 使主体推知

25、其他主体发送过的消息使主体推知其他主体发送过的消息说明消息的出处说明消息的出处 共享秘钥情况共享秘钥情况共享秘钥情况共享秘钥情况 公钥情况公钥情况公钥情况公钥情况 共享秘钥情况共享秘钥情况共享秘钥情况共享秘钥情况BAN逻辑：推理规则推理规则 临时值验证规则临时值验证规则临时值验证规则临时值验证规则 使主体推知其他主体的信仰使主体推知其他主体的信仰BAN逻辑：推理规则推理规则 管辖规则管辖规则管辖规则管辖规则 拓展了主体的推知能力拓展了主体的推知能力 使主体可以在基于其他主体已有的信仰之上推知新的信仰使主体可以在基于其他主体已有的信仰之上推知新的信仰BAN逻辑：推理规则推理规则 接收消息规则接收

26、消息规则接收消息规则接收消息规则 定义了主体在协议运行中对消息的获取定义了主体在协议运行中对消息的获取 规则规则1 1 规则规则2 2BAN逻辑：推理规则推理规则 接收消息规则接收消息规则接收消息规则接收消息规则 定义了主体在协议运行中对消息的获取定义了主体在协议运行中对消息的获取 规则规则3 3 规则规则4 4BAN逻辑：推理规则推理规则 接收消息规则接收消息规则接收消息规则接收消息规则 定义了主体在协议运行中对消息的获取定义了主体在协议运行中对消息的获取 规则规则5 5BAN逻辑：推理规则推理规则 信仰规则信仰规则信仰规则信仰规则 反映了信念在消息的级联与分割的不同操作中的一致性反映了信念

27、在消息的级联与分割的不同操作中的一致性 规则规则1 1 规则规则2 2BAN逻辑：推理规则推理规则 信仰规则信仰规则信仰规则信仰规则 反映了信念在消息的级联与分割的不同操作中的一致性反映了信念在消息的级联与分割的不同操作中的一致性 规则规则3 3 规则规则4 4BAN逻辑：推理规则推理规则 新鲜性规则新鲜性规则新鲜性规则新鲜性规则 如果一个公式的一部分是新鲜的，则该公式的全部是新鲜的如果一个公式的一部分是新鲜的，则该公式的全部是新鲜的BAN逻辑：推理规则推理规则 密钥与秘密共享规则密钥与秘密共享规则密钥与秘密共享规则密钥与秘密共享规则 共享密钥和共享秘密具有对称性共享密钥和共享秘密具有对称性

28、规则规则1 1 规则规则2 2BAN逻辑：推理规则推理规则 密钥与秘密共享规则密钥与秘密共享规则密钥与秘密共享规则密钥与秘密共享规则 共享密钥和共享秘密具有对称性共享密钥和共享秘密具有对称性 规则规则3 3 规则规则4 4内容提要1.1.安全协议存在安全缺陷安全协议存在安全缺陷2.2.安全协议形式化分析安全协议形式化分析3.3.类类BANBAN逻辑形式化分析逻辑形式化分析4.4.例子：对例子：对NSSKNSSK认证协议的认证协议的BANBAN逻辑分析逻辑分析对NSSK认证协议的BAN逻辑分析分析步骤分析步骤 BANBAN逻辑的分析步骤逻辑的分析步骤逻辑的分析步骤逻辑的分析步骤 对协议的进行对协

29、议的进行理想化理想化 将协议的实际消息转换成将协议的实际消息转换成BANBAN逻辑的公式逻辑的公式 给出协议初始状态及其所基于的假设给出协议初始状态及其所基于的假设 对协议进行解释对协议进行解释注释注释 将形如将形如P PQ Q:X X的协议步骤转换成形如的协议步骤转换成形如Q Q X X的逻辑语言的逻辑语言 形式化说明协议将达成的安全目标形式化说明协议将达成的安全目标 应用公理和推理规则以及协议会话事实和假设，从协议的开始进行推证直至验应用公理和推理规则以及协议会话事实和假设，从协议的开始进行推证直至验证协议是否满足其最终运行目标证协议是否满足其最终运行目标对NSSK认证协议的BAN逻辑分析

30、理想化协议 协议的理想化协议的理想化协议的理想化协议的理想化 目的目的 非形式化的符号表达非常模糊非形式化的符号表达非常模糊 示例一示例一 理想化之前：理想化之前：A A-B B:A A,k kABAB k kBSBS 告诉告诉B B(它知道它知道k kBSBS)k kABAB是它和是它和A A的通信秘钥的通信秘钥 理想化之后：理想化之后：对NSSK认证协议的BAN逻辑分析理想化协议 协议的理想化协议的理想化协议的理想化协议的理想化 理想化的一些简单的指导方针理想化的一些简单的指导方针 如果任何时候接收者得到一个真实消息如果任何时候接收者得到一个真实消息m m后能推导出发送者必须相信后能推导出

31、发送者必须相信X X，那么，那么m m能被解能被解释成一个公式释成一个公式X X 现实中的随机数被转化为任意的新公式现实中的随机数被转化为任意的新公式 假定在整个过程中发送者都相信这些公式：假定在整个过程中发送者都相信这些公式：Y Y 把把Y Y作为一个秘密使用，仅当该秘密用作身份证明时有效作为一个秘密使用，仅当该秘密用作身份证明时有效 出于实用性目的，每个主体总是相信它作为消息产生的公式出于实用性目的，每个主体总是相信它作为消息产生的公式对NSSK认证协议的BAN逻辑分析理想化协议 协议的注释协议的注释协议的注释协议的注释 在协议执行过程中，一系列关于各个主体的信条和所看到的内容的说明在协议

32、执行过程中，一系列关于各个主体的信条和所看到的内容的说明 发送第一条消息以前的公式表示各主体在协议开始时的信条发送第一条消息以前的公式表示各主体在协议开始时的信条初始假设初始假设 各主体之间共享了哪些密钥各主体之间共享了哪些密钥 那些主体能产生新鲜的随机数那些主体能产生新鲜的随机数 哪些主体在哪方面被信任哪些主体在哪方面被信任 合法注释的主要规则合法注释的主要规则 如果在如果在P-Q:Y P-Q:Y 之前之前X X成立，则之后成立，则之后X X和和Q Q Y Y都成立都成立 如果根据推理规则，能从已知的如果根据推理规则，能从已知的X X推到出推到出Y Y，则，则X X成立时成立时Y Y必然成立

33、必然成立 如果能从如果能从X X得到得到Y Y，则，则X X成立时成立时Y Y也成立也成立对NSSK认证协议的BAN逻辑分析分析NS协议 Needham-Schroeder(Needham-Schroeder(NSNS)协议协议协议协议 A A-S S:A A,B B,N Na a S S-A A:N Na a,B B,k kabab,A A k kbsbs k kasas A A-B B:k kabab,A A k kbsbs B B-A A:N Nb b k kabab A-B:A-B:N Nb b-1-1k kabab对NSSK认证协议的BAN逻辑分析分析NS协议 理想化协议理想化协议理

34、想化协议理想化协议对NSSK认证协议的BAN逻辑分析分析NS协议 初始假设初始假设初始假设初始假设对NSSK认证协议的BAN逻辑分析分析NS协议 注释注释注释注释NSNS协议协议协议协议对NSSK认证协议的BAN逻辑分析分析NS协议 NSNS协议的目标公式协议的目标公式协议的目标公式协议的目标公式对NSSK认证协议的BAN逻辑分析分析NS协议 BANBAN逻辑的推导过程逻辑的推导过程逻辑的推导过程逻辑的推导过程对NSSK认证协议的BAN逻辑分析分析NS协议 BANBAN逻辑的推导过程逻辑的推导过程逻辑的推导过程逻辑的推导过程对NSSK认证协议的BAN逻辑分析分析NS协议 重新审视对重新审视对重新审视对重新审视对NSNS协议的分析协议的分析协议的分析协议的分析 A A-S S:A A,B B,N Na a S S-A A:N Na a,B B,k kabab,A A k kbsbs k kasas A A-B B:k kabab,A A k kbsbs B B-A A:N Nb b k kabab A-B:A-B:N Nb b-1-1k kababl假设kab泄露u攻击者在第三步冒充A重发消息u攻击者截获第四步消息u攻击者构造第五步消息u攻击者成功建立一个冒名顶替的会话密钥假设条件的合理性至关重要：假设条件的合理性至关重要：END