第7讲《安全协议形式化分析与设计》

第七讲:安全协议形式化分析与设计主讲人：xxxxxx系2020年5月17日星期日《通信网安全理论与技术》课程实践性通信安全保障协议安全设计理论和技术基础前导性8.课程体系及主要内容——讲解内容•通信网安全现状、趋势与策略——第1讲•通信网技术基础与安全体系——第2讲•通信网安全基础理论与技术(密码学、攻击与防御技术)——第3讲•网络安全协议理论设计与分析–认证协议以及密钥建立协议——第4讲–数字签名与阈下信道设计——第5讲–零知识证明及其安全协议构造——第6讲–安全协议形式化分析与设计——第7讲–典型的网络安全协议(IPSec协议、Kerberos协议、Radius/AAA协议)——第8～10讲•通信网安全保障技术——第11讲•无线网络安全性增强技术(WLAN为主)——第12讲•网络防火墙与入侵防御技术——第13讲•网络安全实现方案设计与分析——第14讲内容提要1.安全协议存在安全缺陷2.安全协议形式化分析3.类BAN逻辑形式化分析4.例子：对NSSK认证协议的BAN逻辑分析安全协议存在安全缺陷——原因•目前安全协议因如下原因，都存在一些安全缺陷：–对于其目的、需求和概念没有明确认识和准确描述–运行环境复杂，攻击者无处不在，其攻击能力强、手段多–协议设计者误解或者采用了不恰当的技术•很多安全缺陷并不显而易见，必须采用一定的分析手段才能发现和弥补安全协议存在安全缺陷——常见缺陷•根据其产生的原因和相应的攻击方法，安全缺陷主要有：–基本协议缺陷：指在设计中没有或者很少防范攻击者的攻击而引发的协议缺陷•例如：使用公钥密码系统加密交换消息时，不能预防中间人攻击–口令/密钥猜测缺陷：指用户选择一些常用词作为其口令，而导致攻击者能进行口令猜测攻击；或者选取了不安全的伪随机数生成算法构造密钥，使攻击者能够恢复该密钥安全协议存在安全缺陷——常见缺陷–陈旧消息缺陷：指设计中对消息的新鲜性没有充分考虑，从而使攻击者能够进行消息重放攻击，包括消息源的攻击、消息目的的攻击等–并行会话缺陷：指协议对并行会话攻击缺乏防范，从而导致攻击者通过交换适当的协议消息能够获得所需要的信息。包括并行会话单角色缺陷、并行会话多角色缺陷等–内部协议缺陷：指协议的可达性存在问题，协议的参与者中至少有一方不能够完成所有必需的动作而导致的缺陷–密码系统缺陷：指协议中使用的密码算法和安全协议导致协议不能完全满足所要求的机密性、完整性等需求而产生的缺陷内容提要1.安全协议存在安全缺陷2.安全协议形式化分析3.类BAN逻辑形式化分析4.例子：对NSSK认证协议的BAN逻辑分析安全协议形式化分析——需求•从前面的认证协议、密钥建立协议来看，几乎所有协议都有安全漏洞•迫切需要一套协议的安全分析方法，以指导协议设计–安全协议形式化分析就是一种正规的、标准的方法，可有效检查协议是否满足其安全目标–形式化分析被视作分析协议安全的有效工具安全协议形式化分析——主要技术•现有的安全协议形式化分析技术主要有四种：–逻辑方法：采用基于信仰和知识逻辑的形式分析方法，比如以BAN逻辑为代表的类BAN逻辑–通用形式化分析方法：采用一些通用的形式分析方法来分析安全协议，例如应用Petri网等–模型检测方法：基于代数方法构造一个运行协议的有限状态系统模型，再利用状态检测工具来分析安全协议–定理证明方法：将密码协议的安全行作为定理来证明，这是一个新的研究热点内容提要1.安全协议存在安全缺陷2.安全协议形式化分析3.类BAN逻辑形式化分析4.例子：对NSSK认证协议的BAN逻辑分析类BAN逻辑形式化分析——BAN逻辑形式化•在众多协议形式化分析方法中，其中最具有影响的是1989年由Burrows、Abadi和Needham提出的BAN逻辑–成功地对NS协议，Kerberos等几个著名的协议进行了分析，找到了其中已知的和未知的漏洞–由此，激发了密码研究者对密码协议形式分析的兴趣．并导致许多密码协议形式分析方法的产生•BAN逻辑只在抽象层次上讨论认证协议的安全行，而不考虑其具体实现的安全缺陷和因加密体制而引发的协议缺陷类BAN逻辑形式化分析——BAN逻辑形式化•它是一种基于主体信念以及用于从已知信念推出新的信念的推理规则的逻辑•基本原理：–它可形式化定义协议的目标，并确定协议初始时刻各参与者的知识和信任，通过协议里消息的发送和接收步骤产生新知识，运用推导规则来得到目标信任和知识–如果得到最终的关于知识和信任的语句集里不包含所要得到的信任和知识的语句时，就表明协议存在安全缺陷•即：通过相互发送和接收消息，协议双方能否从最初的信念逐渐发展到协议运行最终要达到的目的类BAN逻辑形式化分析——对BAN逻辑修改或扩充•人们发现BAN逻辑在分析某些协议和协议攻击时，功能还不够完善，对协议中某些性能的推理能力有限，因此各国学者又提出了许多修改和扩充意见，其中较为著名的有：–GNY逻辑–AT逻辑–VO逻辑和SVO逻辑–……•它们统称为BAN类逻辑类BAN逻辑形式化分析——对BAN逻辑修改或扩充•GNY逻辑对BAN逻辑作了如下重要改进与推进：–通过新增加的逻辑构件与规则，推广了BAN逻辑的应用范围–增加了“拥有密钥”的表达式，增加了GNY逻辑本身的表达能力–在GNY逻辑中，区分一个主体收到的消息和一个主体可用的消息–在GNY逻辑中，进一步区分一个主体自己生成的消息和其它消息–在GNY逻辑的分析中，在理想化协议中保留明文；而在BAN逻辑分析中，明文在认证过程中不起作用类BAN逻辑形式化分析——对BAN逻辑修改或扩充•AT逻辑–AT逻辑比BAN逻辑更接近的模态逻辑：–对BAN逻辑中的定义和推理规则进行整理，抛弃其中语义和实现细节的混合部分：•对某些逻辑构件引入更直接的定义，免除对诚实性进行隐含假设•简化了推理规则，所有的概念都独立定义，不与其它概念相混淆•整个逻辑只有两条基本推理规则：–MP规则(moduspones)–Nec规则(necessitation)–在AT逻辑中有一条比BAN逻辑更加直接的管辖公理A15PcontrolsPsays^类BAN逻辑形式化分析——对BAN逻辑修改或扩充•VO逻辑–其贡献在于：拓展了BAN逻辑的应用范围。VO逻辑的设计目标就是增加分析Diffie-Hellman协议的能力，进而可以分析IETF标准——Internet密钥交换协议IKE和SSL协议等–它细化了认证协议的认证目标类BAN逻辑形式化分析——对BAN逻辑修改或扩充•虽形式化分析已获得了较大发展，但它还需在以下几方面提高：–扩展现有的形式化分析工具的能力，使之不仅能分析证明一个安全协议的不安全性，还能证明协议的安全性以及分析和评测系统的安全性–为现有形式语言构造完善的数学描述，并进行严谨的理论证明；为各种协议形式化分析方法形成统一的形式语言表述，以描述可利用的必要信息，并使之能够应用于一些新的应用协议的分析中–将形式化方法应用于协议说明和协议涉及阶段，使之不仅仅用于分析具体的某个安全协议的安全性，从而可以极小的代价尽可能早地发现错误类BAN逻辑形式化分析——BAN逻辑形式化•形式化分析的步骤：–首先需要进行“理想化”，即将协议的消息转换为BAN逻辑中的公式–再根据具体情况进行合理的假设–再由逻辑的推理规则，根据理想化协议和假设进行推理，推断协议能否完成预期的目标类BAN逻辑形式化分析——BAN逻辑形式化•BAN逻辑系统的假设如下：①密文块不能被篡改，也不能用几个小的密文块来拼凑成一个新的大的密文块②一个消息中的两个密文块被看作是分两次分别到达的③加密系统是完善的，只有知道密钥的主体才能解读密文消息，任何不知道密钥的主体都不能解读密文消息，也没有办法根据密文推导密钥④密文含有足够的冗余消息，解密者可以根据解密的结果来判断他是否已经正确解密⑤消息中有足够的冗余消息，使得主体可以判断该消息是否来源于自身⑥BAN逻辑还假设协议的参与主体是诚实的类BAN逻辑形式化分析——BAN逻辑形式化•BAN逻辑主要包含下面三种处理对象：–主体–密钥–公式，也被称为语句或命题•依照BAN逻辑的惯例，P，Q，R等表示主体变量，K表示密钥变量，X，Y表示公式变量。A，B表示主体，S表示服务器•协议的每个消息表达为该逻辑的一个公式–Na、Nb、Nc代表具体的观点(如随机数)–X、Y代表一般意义上的消息•推导规则–“逻辑公式X1,X2,….,Xn成立则Y成立”记为11,,,nXXXY类BAN逻辑形式化分析——BAN逻辑形式化基本公式语义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以及他们信任的人知道{X}K用k加密X后的消息XYX与消息Y结合kPQkPXPQBAN逻辑：推理规则•消息含义规则–使主体推知其他主体发送过的消息——说明消息的出处•共享秘钥情况•公钥情况•共享秘钥情况|,{}1:||~PQPQkkPQPPXMPQX,{}PQPQkkPbelievesQPPseesXPbelievesQsaidX1|,{}2:||~QQkkPQPXMPQX1,{}QQkkPbelievesQPseesXPbelievesQsaidX|,3:||~XYPQPPXMPQX,XYPbelievesPQPseesXPbelievesQsaidXBAN逻辑：推理规则•临时值验证规则–使主体推知其他主体的信仰|#(),||~1:||PXPQXNPQX,PbelieveXisfreshPbelieveQsaidXPbelieveQbelieveXBAN逻辑：推理规则•管辖规则–拓展了主体的推知能力•使主体可以在基于其他主体已有的信仰之上推知新的信仰||,||1:|PQXPQXJPX,PbelieveQcontrolXPbelieveQbelieveXPbelieveXBAN逻辑：推理规则•接收消息规则–定义了主体在协议运行中对消息的获取•规则1•规则2(,)1:PXYRPX2:YPXRPX(,)PsawXYPsawXYPsawXPsawXBAN逻辑：推理规则•接收消息规则–定义了主体在协议运行中对消息的获取•规则3•规则4|,{}3:PQPQkkPQPPXRPX|,{}4:kkPPPXRPX,{}PQPQkkPbelieveQPPsawXPsawX,{}kkPbelievePPsawXPsawXBAN逻辑：推理规则•接收消息规则–定义了主体在协议运行中对消息的获取•规则51|,{}5:QkkPQPXRPX1,{}QkkPbelieveQPsawXPsawXBAN逻辑：推理规则•信仰规则–反映了信念在消息的级联与分割的不同操作中的一致性•规则1•规则2|,|1:|(,)PXPYBPXY|(,)2:|PXYBPX,(,)PbelieveXPbelieveYPbelieveXY(,)PbelieveXYPbelieveXBAN逻辑：推理规则•信仰规则–反映了信念在消息的级联与分割的不同操作中的一致性•规则3•规则4||(,)3:||PQXYBPQX|~(,)4:|~PQXYBPQX(,)PbelieveQbelieveXYPbelieveQbelieveX(,)PbelieveQsaidXYPbelieveQsaidXBAN逻辑：推理规则•新鲜性规则–如果一个公式的一部分是新鲜的，则该公式的全部是新鲜的|#()1:|#(,)PXFPXY(,)PbelieveXisfreshPbeli