ban逻辑及其在协议认证中的缺陷

《ban逻辑及其在协议认证中的缺陷》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、BAN逻辑及其在协议认证中的缺陷：BAN逻辑可以证明协议是否能够达到预期目标，还能够发现协议中存在的一些缺陷。论文在分析了BAN逻辑的主要规则和分析步骤之后，着重研究了BAN逻辑存在的各类缺陷，并对BAN类逻辑需要改进的方面进行了讨论。　　关键词：密码协议；BAN逻辑；形式化分析　　：TP311：A：1009-3044(2011)10-2266-03　　在复杂的X络环境下，通信安全是人们首要关注的问题。攻击者通过各种手段非法获得想要得到的有用信息。为此，人们设计了诸多密码协议，如Nssk协议、Ke

2、rberos协议等等。利用密码协议可以实现密钥的分配和交换、身份认证等，其目标不仅仅是实现通信的加密传输，更主要的是解决通信中的安全问题。但是，现有的密码协议并非像设计者想象的那样安全。很多情况下，密码协议仍然存在漏洞可能被攻击者利用，这并非是由于密码算法不够安全，而是由于协议本身的结构存在问题。密码协议的安全分析是揭示密码协议是否存在缺陷和漏洞的重要途径。通过对协议的形式化分析，可以发现其中的未知缺陷，进而可以针对这些缺陷对密码协议进行改进，提高其安全性。　　认证协议是否正确，常用的方法：1)采

3、用逐个对协议进行攻击的检验方法；2)应用形式化的分析工具，其中最典型的是BAN逻辑。BAN逻辑是1989年由Burro提出的[1]，它是一种基于信仰的模态逻辑。在BAN逻辑的推理过程中，参加协议的主体的信仰随消息交换的发展而不断变化和发展。应用BAN逻辑进行协议分析时，首先需要将协议的消息转换为BAN逻辑中的公式，即进行协议的“理想化步骤”，再根据具体情况进行合理的假设，然后利用逻辑的推理规则根据理想化协议和假设进行推理，推断协议能否达到预期的目标。　　1BAN逻辑的基本概念　　BAN逻辑在认证协

4、议的形式化分析中发挥了积极有效的作用。BAN逻辑仅从抽象的层次上来讨论认证协议的安全性，它不考虑由协议的具体实现所带来的安全缺陷，也不考虑由于加密体制的缺点所引发的协议缺陷。BAN逻辑的使用，是建立在如下所做的假设基础之上的：　　1)密文块不能被篡改，也不能用几个小的密文块组成一个新的大密文块。　　2)若一个消息中有两个密文块，则该密文块被看作是分两次分别到达的。　　3)假设加密系统是完善的，即只有掌握密钥的主体才能理解密文消息，才能解密密文而得到明文。攻击者无法从密文推断出密钥。　　4)密文含有

5、足够的冗余信息，使解密者可以判断他是否应用了正确的密钥。　　5)消息中含有足够的冗余信息，使主体可以判断该消息是否于本身。　　6)假设参与协议的主体是诚实的。　　1.1BAN逻辑的语法和语义　　A，B，S：A，B为通信主体，S为认证服务器；　　K：加密密钥；Kab,Kas,Kbs：通信主体的共享密钥；　　Ka,Kb：通信主体的公开密钥；Ka-1,Kb-1：通信主体的秘密密钥；　　Na,Nb：通信主体的观点；P,Q：主体变量；　　X,Y：一般意义上的语句；(X,Y)：X和Y的连接；　　P

6、≡X：P相

7、信X，即P认为X为真；　　PX：P看到过X，P接收到了包含X的消息，P能读出并重复X；　　P

8、~X：P曾经说过X，P在某一时刻曾发送过包含X的消息。包含两个含义：一方面是指消息X是由P发送的，即消息源是P；另一方面，指P能够确认消息X的含义，即能够识别该消息并做出正确的解释；　　P

9、X：P对X有控制权或管辖权；　　#(X)：X是新鲜的，即协议执行之前X未被传送过；　　P•Q：P和Q可使用共享密钥K通信，而且K是好的密钥。这个断言是指密钥的排他性，即只有P，Q或可信任的第三方知道K；　　

10、P：K是P的公钥；　　PQ：X是P、Q之间的共享秘密，且除P和Q以及他们相信的主体之外，其他主体都不知道X；　　{X}K：用密钥K加密X的结果；　　﹤X﹥Y：由X和Y合成的消息，其中Y是一个秘密；　　1.2BAN逻辑的主要几条推理规则　　1)消息含义规则(MessageMeaningRules)：　　对于共享密钥：　　表示如果P相信K为P和Q之间的共享密钥，且P接收到用K加密X的消息{X}K，则P相信Q发送过消息X。　　对于公开密钥：　　表示P相信K是Q的公钥，而K-1是Q的私钥，当P看到用Q的私

11、钥加密的消息时，就能够断定它是Q发送的。　　2)管辖权规则(JurisdictionRule)　　表示如果P相信Q有权控制X，且P相信Q也相信X时，则P相信X。　　3)临时值校验规则(NonceVerificationRule)　　表示如果P相信X是新鲜的，并且P相信Q曾发送过X，则P相信Q相信X。　　4)接收消息规则(SeeingRules)　　上述推理规则表示：如果一个主体曾收到一个公式，且该主体知道相关的密钥，则该主体曾收到该公式的组成部分。　　5)新鲜性规则(Freshne