BAN逻辑及其在认证协议性质分析中的应用研究

摘要：在各类安全协议中，认证协议分析正成为热点，BAN逻辑是近年来主要的认证协议分析工具之一。在分析了BAN逻辑主要规则和分析步骤之后，研究了BAN逻辑存在的各类缺陷，并对BAN 类逻辑需要改进的方面进行了讨论。

关键词：认证协议；形式化分析；BAN 逻辑

中图分类号：TP311文献标识码：A文章编号：1009-3044(2008)12-2pppp-0c

BAN Logic and It's Application in Authentication Protocol Analysis

JIN Li-ping,GU Xiang,JI Li-na

(School of Computer Science and Technology,Nantong University,Nantong 226019,China)

Abstract:The security of Internet becomes more and more important today.Now the authentication protocol analysis has become a hot topic.BAN logic is one of main tools of protocol analysis.The paper analyzed constitute of BAN logic and analysis steps. Then it pointed out various kinds of demerit of BAN logic. It also discussed some possible improvement.

Key words:Authentication Protocol;Formalized Analysis;BAN Logic

1 BAN逻辑分析方法

BAN 逻辑是由美国DEC公司研究人员Burrows，Abadi和Needham提出的一种可用于认证协议形式化分析的逻辑[1]。借助此逻辑，认证双方可以对相互身份进行确认。此逻辑是基于知识和信仰的，认证双方通过相互接受和发送消息来从最初的信仰逐渐发展到最终信仰。

BAN逻辑在协议分析时假设协议采用的密码算法是完美的，即不考虑密码算法被攻破[2]。

1.1 BAN逻辑的基本符号

BAN逻辑的对象包括：主体（用P、Q表示），密钥（用K表示）和公式。其基本符号有：

P颉X：P相信X，即主体P在某一时刻曾发送过包含X的消息。

② P颉X：P曾说过X，即主体P在某一时刻发送过包含X的消息。

③ P?X：P看到过X，即某些主体曾发送过包含X的消息，P能读出并重复X。

④ P?X：P对X有仲裁权。

⑤ #（X）：X是最新的。

⑥ P ? KQ：P，Q之间共享密钥K。

⑦ K?P：K是P的公开密钥。

1.2 BAN逻辑的主要推理规则

①消息意义规则 jlp01.tif

P相信P和Q之间共享密钥K，而且P看到过用密钥K加密过的消息{X}K；由此可知P相信Q曾经发送过包含X的消息。

②随机数验证规则 jlp02.tif

P相信X是最新的，P相信Q曾经发送过包含X的消息；由此可知P相信Q也相信X。

③仲裁规则 jlp03.tif

P相信Q对X有仲裁权，且P相信Q相信X；由此可知P也相信X。

④信仰规则 jlp04.tif

P相信X，P相信Y；由此可知P相信X、Y组合而成的消息。

jlp05.tif

P相信X、Y组合而成的消息；由此可知P相信X。

jlp06.tif

P相信Q相信X、Y组合而成的消息；由此可知P相信Q相信X。

⑤ 新鲜性规则jlp07.tif

P相信X是最新的；由此可知到P相信X、Y组合而成的消息是最新的。

⑥jlp08.tif

一次性随机数N是最新的，且存在N和会话密钥K的组合；由此可知会话密钥K是最新的。

⑦jlp09.tif

会话密钥K是最新的，P看到过用密钥K加密的消息{X}K，P相信P和Q之间共享密钥K，由以上三个条件可知P相信Q曾经发送过包含X的消息，P相信Q相信P和Q之间共享密钥K。

1.3 BAN逻辑形式化分析步骤

一般而言, BAN逻辑对协议形式化分析分为以下三步：

①初始假设。除了协议约定，在使用BAN逻辑分析时，另需约定一些常规条件（假设）。

②协议描述（理想化）。将协议消息转化为BAN逻辑描述的公式，在此过程中可去除协议中的对协议分析无关的部分。

③逻辑推理。对假设和描述公式运用推理规则推理，得出各认证主体的最终信仰。

1.4 BAN逻辑分析的结论

协议分析中存在两种级别的信仰：一级信仰为主体A相信和主体B共享密钥K，主体B相信和主体A共享密钥B；二级信仰为主体A相信主体B相信它和A共享密钥K，主体B相信它和主体A共享密钥K。

即一级信仰：A颉AK?BB颉AK?B

二级信仰：A颉B颉AK?B B颉A颉AK?B

通过判断分析结果能否达到最终信仰，可以确定协议是否安全。

2 BAN协议的BAN逻辑分析

下面以BAN协议为例，来说明BAN逻辑分析协议的过程。

BAN协议的基本思想是：主体A和主体B在通信时，主体A先向B发送自己的身份信息A和产生的一次性随机数Na；B收到后，向认证机构S发送自己的身份信息B和产生一次性随机数Nb，并转发A刚才发送的消息；S收到B所发送的消息后，认为主体A和主体B要进行通信而且正在申请会话密钥，它就向A发送包含A，B之间会话密钥Kab及A，B身份的加密消息；A收到后判断一次性随机数Na及B的身份后，就可获得会话密钥Kab，然后用会话密钥Kab对Nb、B杂凑后，连同从S收到的消息一起发送给B；B收到A发送的消息后，用和S共享的密钥对第一部分解密，得到会话密钥Kab，并由随机数Nb的新鲜性来判断会话密钥Kab的新鲜性；最后B对Na、A杂凑后，向A传送以表示自己得到了会话密钥Kab。上述消息可以用公式描述如下：

消息① AB：A，Na

消息② BS：A，NA，B，Nb

消息③ SA：{Na，B，Nb，Kab } ，{ ，A， }

消息④ AB：{Nb，A，Kab} ，MACKab（Nb，B）

消息⑤ BA：MACKab（Na，A）

下面就对其进行BAN分析。

第一步进行初始假设，在此协议中，共进行如下8条初始假设：

①A颉A Kas?S A相信A和S共享密钥Kas

②B颉B Kbs?S B相信B和S共享密钥Kbs

③A颉S ?A Kas? S A相信S对A和S共享密钥Kas有仲裁权

④B颉S ?B Kas? S B相信S对B和S共享密钥Kbs有仲裁权

⑤S颉A Kas? S S相信A和S共享密钥Kas

⑥S颉B Kas? S S相信B和S共享密钥Kbs

⑦A颉#（Na） A相信Na是最新的

⑧B颉#（Nb） B相信Nb是最新的

第二步进行协议理想化：

第①、②条消息省略，因为它们对分析协议的逻辑属性没有作用。

消息③ SA：{Na，A?KabB，Nb}Kas，{NB，A?KabB }Kbs

消息④ AB：{Nb，AKabB }Kbs，MACKab（Nb，B）

消息⑤ BA：MACkAB（Na，A）

第三步进行逻辑推理

由消息③，应用规则①得jlp10.tif （a）

利用假设⑦和规则⑤，得jlp11.tif （b）

由公式（a）和（b），利用规则②，得jlp12.tif （c）

由公式（c），利用规则④，得A颉{A Kab?B} （d）

由公式（d），利用规则③，得 A颉A Kab?B（e）

消息④中的第一部分的分析与以上的分析相似，得B颉A Kab?B

消息④中的第二部分和公式（b），应用规则（7），得B颉A颉{A Kab?B}

消息⑤和公式（b），应用规则⑦，得 A颉B颉{A Kab?B}

上面的结论符合最终信仰，所以可以认为该协议是安全的。

3 BAN逻辑的缺陷

3.1 BAN逻辑的缺陷

按照BAN逻辑分析方法的规定，如果协议能够达到最终信仰，那么就可以相信该协议是安全无缺陷的。然而事实上，BAN逻辑只能做到：不能达到最终信仰的协议一定是不安全的；它并不能保证达到最终信仰的协议就一定是安全的。参考文献[3]就给出了一个因协议中含有弱密钥而导致未能分析出密钥猜测攻击的例子。

3.2 BAN逻辑缺陷产生的原因分析

之所以会产生上述问题，是因为在BAN逻辑分析时，存在着一些不精确的地方[4]：

① 初始假设：初始假设是BAN逻辑分析的一个重要步骤，然而对于这个步骤并没有明确的可以依据的方法。通常这一步骤和分析人员的经验有着较大的关系。在进行BAN逻辑分析时，如果增加一个初始假设，就会得到协议是安全的结论；而如果去除这个条件，则会得出相反的结论。这一点是导致BAN逻辑缺陷的一个重要原因。

②协议理想化：理想化其实就是将要分析的协议用逻辑公式表示出来，但是BAN逻辑的理想化步骤本身其实是非形式化的，这就造成BAN逻辑分析协议缺乏有效性和正确性，没有达到形式化方法分析协议的要求。

③语义：BAN逻辑缺少一个定义良好的语义，造成了BAN逻辑分析经常会遭受重放攻击。

④对协议的攻击探测能力较弱：在BAN逻辑分析过程中有时不能有效检测出对协议的重放攻击，同时它也无法检查出协议的并发运行所带来的各类攻击。

3.3 BAN逻辑的改进

为克服BAN逻辑的不足，学者们对BAN逻辑进行了某些必要的改进或扩展，提出了许多扩展的BAN 逻辑[5]。

GNY逻辑等对推理系统进行了改进；AT逻辑、VO逻辑、SVO逻辑等对语义进行了改进；MB逻辑等对理想化进行了改进。

归纳这些扩展的BAN逻辑，在克服BAN逻辑的缺陷和推广其应用范围上，取得了很大的成功。但相对来讲扩展的BAN逻辑推理规则更多，运用起来复杂，还不如BAN逻辑简单直观实用。同时，它们的工作方式基本上与BAN逻辑一样，并没有从根本上有效地克服形式逻辑分析方法所特有的理想化步骤缺陷。

4 结束语

BAN逻辑为密码协议第一次提供了一整套形式化分析方法，成功地找到密码协议的许多缺陷及攻击，这极大地推动了密码协议的分析及设计。但它也存在着致命的缺陷：当逻辑发现协议中的错误，每个人都相信那确实是有问题；当逻辑证明一个协议是安全的，但没有人敢相信它的正确性。所以采用BAN类逻辑这种方法可以进行密码协议分析和辅助设计，但还不能完全信任其分析结果。

参考文献：

[1]Michael Burrows,Martin Abadi,Roger M Needham.A logic of Authentication[J].ACM Transactions on Computer Systems,1990,8(1):18-36.

[2]R.Needham．Using encryption for authentication in large networks of computers[J].Communications of the ACM,1978,21(12):993-999.

[3]杨世平,李祥.BAN逻辑在协议分析中的密钥猜测分析缺陷[J].计算机工程,2006,32(9):126-127,130.

[4]王亚弟,等.密码协议形式化分析[M].北京:机械工业出版社,2006.

[5]冯彬.关于BAN 逻辑分析的改进[J].中国科学院研究生院学报,2002,19(3):306-310.

收稿日期：2008-01-12

基金项目：江苏省高校自然科学研究计划（05KJD520166）；江苏省高校“青蓝工程”资助；南通大学学生课外科技计划资助

作者简介：顾翔（1973-），男，江苏南通人，副教授，硕士生导师，博士，研究方向：为协议工程，形式化技术。

注：“本文中所涉及到的图表、注解、公式等内容请以PDF格式阅读原文。”