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：加密密钥；