BAN逻辑及其在协议认证中的缺陷
开篇：润墨网以专业的文秘视角，为您筛选了一篇BAN逻辑及其在协议认证中的缺陷范文，如需获取更多写作素材，在线客服老师一对一协助。欢迎您的阅读与分享！
摘要：ban 逻辑可以证明协议是否能够达到预期目标，还能够发现协议中存在的一些缺陷。论文在分析了BAN 逻辑的主要规则和分析步骤之后，着重研究了BAN 逻辑存在的各类缺陷，并对BAN 类逻辑需要改进的方面进行了讨论。
关键词：密码协议；BAN逻辑；形式化分析
中图分类号：TP311文献标识码：A文章编号：1009-3044(2011)10-2266-03
在复杂的网络环境下，通信安全是人们首要关注的问题。攻击者通过各种手段非法获得想要得到的有用信息。为此，人们设计了诸多密码协议，如Nssk协议、Kerberos协议等等。利用密码协议可以实现密钥的分配和交换、身份认证等，其目标不仅仅是实现通信的加密传输，更主要的是解决通信中的安全问题。但是，现有的密码协议并非像设计者想象的那样安全。很多情况下，密码协议仍然存在漏洞可能被攻击者利用，这并非是由于密码算法不够安全，而是由于协议本身的结构存在问题。密码协议的安全分析是揭示密码协议是否存在缺陷和漏洞的重要途径。通过对协议的形式化分析，可以发现其中的未知缺陷，进而可以针对这些缺陷对密码协议进行改进，提高其安全性。
认证协议是否正确，常用的方法：1) 采用逐个对协议进行攻击的检验方法；2) 应用形式化的分析工具，其中最典型的是BAN 逻辑。BAN 逻辑是1989年由Burrows，Abadi和Needham提出的[1]，它是一种基于信仰的模态逻辑。在BAN逻辑的推理过程中，参加协议的主体的信仰随消息交换的发展而不断变化和发展。应用BAN逻辑进行协议分析时，首先需要将协议的消息转换为BAN逻辑中的公式，即进行协议的“理想化步骤”，再根据具体情况进行合理的假设，然后利用逻辑的推理规则根据理想化协议和假设进行推理，推断协议能否达到预期的目标。
1 BAN逻辑的基本概念
BAN逻辑在认证协议的形式化分析中发挥了积极有效的作用。BAN逻辑仅从抽象的层次上来讨论认证协议的安全性，它不考虑由协议的具体实现所带来的安全缺陷，也不考虑由于加密体制的缺点所引发的协议缺陷。BAN逻辑的使用，是建立在如下所做的假设基础之上的：
1) 密文块不能被篡改，也不能用几个小的密文块组成一个新的大密文块。
2) 若一个消息中有两个密文块，则该密文块被看作是分两次分别到达的。
3) 假设加密系统是完善的，即只有掌握密钥的主体才能理解密文消息，才能解密密文而得到明文。攻击者无法从密文推断出密钥。
4) 密文含有足够的冗余信息，使解密者可以判断他是否应用了正确的密钥。
5) 消息中含有足够的冗余信息，使主体可以判断该消息是否来源于本身。
6) 假设参与协议的主体是诚实的。
1.1 BAN逻辑的语法和语义
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 |X：P相信X，即P认为X为真；
PX：P看到过X，P接收到了包含X的消息，P能读出并重复X；
P |~X：P曾经说过X，P在某一时刻曾发送过包含X的消息。包含两个含义：一方面是指消息X是由P发送的，即消息源是P；另一方面，指P能够确认消息X的含义，即能够识别该消息并做出正确的解释；
P | X：P对X有控制权或管辖权；
#(X)：X是新鲜的，即协议执行之前X未被传送过；
P•Q：P和Q可使用共享密钥K通信，而且K是好的密钥。这个断言是指密钥的排他性，即只有P，Q或可信任的第三方知道K；
P：K是P的公钥；
PQ：X是P、Q之间的共享秘密，且除P和Q以及他们相信的主体之外，其他主体都不知道X；
{ X }K：用密钥K加密X的结果；
XY：由X和Y合成的消息，其中Y是一个秘密；
1.2 BAN逻辑的主要几条推理规则
1) 消息含义规则(Message Meaning Rules)：
对于共享密钥：
表示如果P相信K为P和Q之间的共享密钥，且P接收到用K加密X的消息{X}K，则P相信Q发送过消息X。
对于公开密钥：
表示P相信K是Q的公钥，而K-1是Q的私钥，当P看到用Q的私钥加密的消息时，就能够断定它是Q发送的。
2) 管辖权规则(Jurisdiction Rule)
表示如果P相信Q有权控制X，且P相信Q也相信X时，则P相信X。
3) 临时值校验规则(Nonce Verification Rule)
表示如果P相信X是新鲜的，并且P相信Q曾发送过X，则P相信Q相信X。
4) 接收消息规则(Seeing Rules)
上述推理规则表示：如果一个主体曾收到一个公式，且该主体知道相关的密钥，则该主体曾收到该公式的组成部分。
5) 新鲜性规则(Freshness Rules)
如果P相信X是新鲜的，则P相信由X和Y连接的整体信息也是新鲜的。
6) 信仰规则(Belief Rules)
7) 密钥与秘密规则(Key and Secret Rules)
1.3 BAN逻辑的推理过程
BAN逻辑在对协议进行形式化分析时，主要解决4个方面的问题：① 认证协议是否正确；② 认证协议的目标是否达到；③ 认证协议的初设是否合适；④ 认证协议是否存在冗余。
BAN逻辑的推理步骤如下：[2]
l) 用逻辑语言对系统的初始状态进行描述，建立初始假设集合。
2) 建立理想化协议模型，将协议的实际消息转换成BAN逻辑所能识别的公式。
3) 对协议进行解释，将形如PQ:X的消息转换成形如 QX的逻辑语言。解释过程中遵循以下规则：① 若命题X在消息PQ:Y前成立，则在其后X和 QY都成立;② 若根据推理规则可以由命题X推导出命题Y，则命题X成立时，命题Y也成立。
4) 应用推理规则对协议进行形式化分析，推导出分析结果。
以上步骤可能会重复进行，例如，通过分析增加新的初设、改进理想化协议等。
2 BAN逻辑的缺陷（Defects of BAN Logic）
BAN逻辑存在着许多不完善的地方[3-4]，按照BAN 逻辑分析方法的规定, 如果协议能够达到最终信仰, 那么就可以相信该协议是安全无缺陷的。然而事实上, BAN 逻辑只能做到：不能达到最终信仰的协议一定是不安全的。它并不能保证达到最终信仰的协议就一定是安全的。这主意是因为：
1) 缺少良好的语义基础：BAN 逻辑缺少一个定义良好的语义, 造成了BAN 逻辑分析经常会遭受重放攻击。
2) 初始假设的不确定性：在BAN逻辑中，初始假设的正确性难以确定。在BAN逻辑中，没有形式化的规则来确定初始假设，也无法确认和自动验证初始假设的正确性和有效性。
3) 理想化步骤非形式化：BAN逻辑的理想化过程是必不可少的步聚，但是BAN逻辑的理想化步骤本身其实是非形式化的, 理想化过程应使理想化后的协议模型能够准确表达原协议，然而理想化后的协议模型与原来的协议有一定差距，对协议的内容有所增加或者有所忽略。这种差异反映到分析结果中也就不可避免地与原协议有一定的出入，不能忠实地表达原协议。这就造成BAN 逻辑分析协议缺乏有效性和正确性, 没有达到形式化方法分析协议的要求。
4) 推理规则存在缺陷：BAN逻辑由一系列的推理规则构成，根据这些推理规则可以分析协议主体能从其接收到的消息中获得怎样的信仰。例如，消息含义规则只有在“消息不可伪造”假设的前提下才能够成立。由于该假设未必成立，所以就构成了该推理规则的缺陷。
5) 无法探测对协议的攻击：BAN逻辑对于的经典重放攻击(如对NS单钥认证协议的攻击)分析效果较好，但并不意味着它可以发现所有的重放攻击，有些类型的重放攻击用BAN逻辑是难以发现的，特别是对并行会话攻击更是无能为力。
下面我们给出一个因协议中含有弱密钥而导致未能分析出密钥猜测攻击的例子。
例如，NS公钥认证协议的简化版本。
(1) AB:{Na,A} Kb (2) BA:{Na,Nb} Ka(3) AB:{Nb } Kb
协议运行的含义如下：
(1) 主体A向主体B发送包含随机数Na和自己身份的消息1，并用B的公钥Kb加密消息1；
(2) B收到并解密消息1后按协议要求向A发送用A的公钥Ka加密的内含随机数Na和Nb的消息2；
(3) 协议最后一步，A向B发送经过Kb加密的Nb。经过这样一次协议运行，主体A和B就建立了一个它们之间的共享秘密Nb=(Kab)，这个共享秘密可以为他们以后进行秘密通信确认双方身份时使用。
用BAN逻辑分析NS公钥认证协议得出协议是安全的结论，但是入侵者I可以通过两次并行运行协议来进行有效地攻击，攻击如下：
第一次运行协议：(1.1) AI:{Na,A} Ki
同时，入侵者I开始第二次运行协议:
(2.1) I(A)B:{Na,A} Kb (2.2) BI(A):{Na,Nb}Ka
(1.2) IA:{Na,Nb} Ka
(1.3) AI:{Nb} Ki
(2.3) I(A)B:{Nb}Kb
入侵者I通过解密消息 (l.1)、消息 (l.3)获取发送消息(2.1)、消息(2.3)所需要的Na、Nb，消息(1.2)则是消息(2.2)的重放。上述协议运行完，主体B认为他与A共享秘密Nb，实际上他与I共享Nb，I假冒A成功，攻击有效。对于网络系统中任何一个合法用户，只要接收到发给自己的NS公钥协议中的消息1，就可以发起上述攻击，来欺骗另外一个用户，故NS公钥协议是不安全的。
此例说明，用BAN逻辑分析是安全的认证协议，并不能保证协议没有攻击。
3 BAN逻辑的改进
从上述分析可以看到BAN 逻辑还有许多不足, 于是产生了这样的尴尬局面：当逻辑发现协议中的错误， 每个人都相信那确实是有问题；当逻辑证明一个协议是安全的, 但没有人敢相信它的正确性。故此，需要针对BAN 逻辑的缺陷进行改进。可改进的方向有：(1) 确立一个可靠的语义，用以验证初始假设的正确性和确保推理的可靠性；(2) 减少理想化步骤的模糊度，进而消除理想化步骤；(3) 建立计算机化的自动分析过程，将各类攻击模拟化并进行分析；(4) 在协议设计阶段，就引入分析从而避免可能发生的设计错误, 并确立好的协议设计方法和规则等。
4 结束语
BAN 逻辑把参与认证的主体在协议运行后所持有的信仰看作是认证协议的目标, 该逻辑从理想化的协议和初始假设出发，应用逻辑规则，对协议运行中的逻辑命题进行推理，最终推出参与协议运行的主体所持有的信仰。BAN逻辑是分析密码协议的一种重要工具，有许多可取之处。当然, BAN 逻辑也存在一些不足, 如BAN 逻辑不考虑协议的具体实现不当导致的错误和不可信主体的认证问题。针对这些缺陷和局限性，一些研究人员又提出了诸多必要的改进和扩展，如GNY逻辑、AT逻辑、MB逻辑、VO逻辑、SVO逻辑等，这些逻辑统称为BAN类逻辑。但相对来讲，BAN类逻辑推理规则更多，运用起来更复杂，不如BAN逻辑简单直观。
参考文献：
[1] M. Burrows, M. Abadi, and R. Needham. A logic of authentication.Proceedings of the Royal Society, Series A,426(1871):233C271, December 1989. Also appeared as SRC Research Report 39 and, in a shortened form, in ACM Transactions on Computer Systems 8, 1 (February 1990),18-36.
[2] 看雪.加密与解密-软件保护技术及完全解决方案[M].北京:电子工业出版社,2001.
[3] 卿斯汉.安全协议[M].北京:清华大学出版社,2005.
[4] 王亚弟,束妮娜,韩继红,王娜.密码协议形式化分析[M].北京:机械工业出版社,2006.