摘要：在各類安全協(xié)議中，認(rèn)證協(xié)議分析正成為熱點(diǎn)，BAN邏輯是近年來主要的認(rèn)證協(xié)議分析工具之一。在分析了BAN邏輯主要規(guī)則和分析步驟之后，研究了BAN邏輯存在的各類缺陷，并對(duì)BAN 類邏輯需要改進(jìn)的方面進(jìn)行了討論。

關(guān)鍵詞：認(rèn)證協(xié)議；形式化分析；BAN 邏輯

中圖分類號(hào)：TP311文獻(xiàn)標(biāo)識(shí)碼：A文章編號(hào)：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提出的一種可用于認(rèn)證協(xié)議形式化分析的邏輯[1]。借助此邏輯，認(rèn)證雙方可以對(duì)相互身份進(jìn)行確認(rèn)。此邏輯是基于知識(shí)和信仰的，認(rèn)證雙方通過相互接受和發(fā)送消息來從最初的信仰逐漸發(fā)展到最終信仰。

BAN邏輯在協(xié)議分析時(shí)假設(shè)協(xié)議采用的密碼算法是完美的，即不考慮密碼算法被攻破[2]。

1.1 BAN邏輯的基本符號(hào)

BAN邏輯的對(duì)象包括：主體（用P、Q表示），密鑰（用K表示）和公式。其基本符號(hào)有：

P︱≡X：P相信X，即主體P在某一時(shí)刻曾發(fā)送過包含X的消息。

② P︱～X：P曾說過X，即主體P在某一時(shí)刻發(fā)送過包含X的消息。

③ P?X：P看到過X，即某些主體曾發(fā)送過包含X的消息，P能讀出并重復(fù)X。

④ P︱?X：P對(duì)X有仲裁權(quán)。

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

⑥ P ? KQ：P，Q之間共享密鑰K。

⑦ K?P：K是P的公開密鑰。

1.2 BAN邏輯的主要推理規(guī)則

①消息意義規(guī)則 jlp01.tif

P相信P和Q之間共享密鑰K，而且P看到過用密鑰K加密過的消息{X}K；由此可知P相信Q曾經(jīng)發(fā)送過包含X的消息。

②隨機(jī)數(shù)驗(yàn)證規(guī)則 jlp02.tif

P相信X是最新的，P相信Q曾經(jīng)發(fā)送過包含X的消息；由此可知P相信Q也相信X。

③仲裁規(guī)則 jlp03.tif

P相信Q對(duì)X有仲裁權(quán)，且P相信Q相信X；由此可知P也相信X。

④信仰規(guī)則 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。

⑤ 新鮮性規(guī)則jlp07.tif

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

⑥jlp08.tif

一次性隨機(jī)數(shù)N是最新的，且存在N和會(huì)話密鑰K的組合；由此可知會(huì)話密鑰K是最新的。

⑦jlp09.tif

會(huì)話密鑰K是最新的，P看到過用密鑰K加密的消息{X}K，P相信P和Q之間共享密鑰K，由以上三個(gè)條件可知P相信Q曾經(jīng)發(fā)送過包含X的消息，P相信Q相信P和Q之間共享密鑰K。

1.3 BAN邏輯形式化分析步驟

一般而言， BAN邏輯對(duì)協(xié)議形式化分析分為以下三步：

①初始假設(shè)。除了協(xié)議約定，在使用BAN邏輯分析時(shí)，另需約定一些常規(guī)條件（假設(shè)）。

②協(xié)議描述（理想化）。將協(xié)議消息轉(zhuǎn)化為BAN邏輯描述的公式，在此過程中可去除協(xié)議中的對(duì)協(xié)議分析無關(guān)的部分。

③邏輯推理。對(duì)假設(shè)和描述公式運(yùn)用推理規(guī)則推理，得出各認(rèn)證主體的最終信仰。

1.4 BAN邏輯分析的結(jié)論

協(xié)議分析中存在兩種級(jí)別的信仰：一級(jí)信仰為主體A相信和主體B共享密鑰K，主體B相信和主體A共享密鑰B；二級(jí)信仰為主體A相信主體B相信它和A共享密鑰K，主體B相信它和主體A共享密鑰K。

即一級(jí)信仰：A︱≡AK?BB︱≡AK?B

二級(jí)信仰：A︱≡B︱≡AK?B B︱≡A︱≡AK?B

通過判斷分析結(jié)果能否達(dá)到最終信仰，可以確定協(xié)議是否安全。

2 BAN協(xié)議的BAN邏輯分析

下面以BAN協(xié)議為例，來說明BAN邏輯分析協(xié)議的過程。

BAN協(xié)議的基本思想是：主體A和主體B在通信時(shí)，主體A先向B發(fā)送自己的身份信息A和產(chǎn)生的一次性隨機(jī)數(shù)Na；B收到后，向認(rèn)證機(jī)構(gòu)S發(fā)送自己的身份信息B和產(chǎn)生一次性隨機(jī)數(shù)Nb，并轉(zhuǎn)發(fā)A剛才發(fā)送的消息；S收到B所發(fā)送的消息后，認(rèn)為主體A和主體B要進(jìn)行通信而且正在申請(qǐng)會(huì)話密鑰，它就向A發(fā)送包含A，B之間會(huì)話密鑰Kab及A，B身份的加密消息；A收到后判斷一次性隨機(jī)數(shù)Na及B的身份后，就可獲得會(huì)話密鑰Kab，然后用會(huì)話密鑰Kab對(duì)Nb、B雜湊后，連同從S收到的消息一起發(fā)送給B；B收到A發(fā)送的消息后，用和S共享的密鑰對(duì)第一部分解密，得到會(huì)話密鑰Kab，并由隨機(jī)數(shù)Nb的新鮮性來判斷會(huì)話密鑰Kab的新鮮性；最后B對(duì)Na、A雜湊后，向A傳送以表示自己得到了會(huì)話密鑰Kab。上述消息可以用公式描述如下：

消息① A→B：A，Na

消息② B→S：A，NA，B，Nb

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

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

消息⑤ B→A：MACKab（Na，A）

下面就對(duì)其進(jìn)行BAN分析。

第一步進(jìn)行初始假設(shè)，在此協(xié)議中，共進(jìn)行如下8條初始假設(shè)：

①A︱≡A Kas?SA相信A和S共享密鑰Kas

②B︱≡B Kbs?SB相信B和S共享密鑰Kbs

③A︱≡S ?A Kas? SA相信S對(duì)A和S共享密鑰Kas有仲裁權(quán)

④B︱≡S ?B Kas? SB相信S對(duì)B和S共享密鑰Kbs有仲裁權(quán)

⑤S︱≡A Kas? S S相信A和S共享密鑰Kas

⑥S︱≡B Kas? SS相信B和S共享密鑰Kbs

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

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

第二步進(jìn)行協(xié)議理想化：

第①、②條消息省略，因?yàn)樗鼈儗?duì)分析協(xié)議的邏輯屬性沒有作用。

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

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

消息⑤ B→A：MACkAB（Na，A）

第三步進(jìn)行邏輯推理

由消息③，應(yīng)用規(guī)則①得jlp10.tif （a）

利用假設(shè)⑦和規(guī)則⑤，得jlp11.tif （b）

由公式（a）和（b），利用規(guī)則②，得jlp12.tif （c）

由公式（c），利用規(guī)則④，得A︱≡{A Kab?B} （d）

由公式（d），利用規(guī)則③，得A︱≡A Kab?B（e）

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

消息④中的第二部分和公式（b），應(yīng)用規(guī)則（7），得B︱≡A︱≡{A Kab?B}

消息⑤和公式（b），應(yīng)用規(guī)則⑦，得 A︱≡B︱≡{A Kab?B}

上面的結(jié)論符合最終信仰，所以可以認(rèn)為該協(xié)議是安全的。

3 BAN邏輯的缺陷

3.1 BAN邏輯的缺陷

按照BAN邏輯分析方法的規(guī)定，如果協(xié)議能夠達(dá)到最終信仰，那么就可以相信該協(xié)議是安全無缺陷的。然而事實(shí)上，BAN邏輯只能做到：不能達(dá)到最終信仰的協(xié)議一定是不安全的；它并不能保證達(dá)到最終信仰的協(xié)議就一定是安全的。參考文獻(xiàn)[3]就給出了一個(gè)因協(xié)議中含有弱密鑰而導(dǎo)致未能分析出密鑰猜測攻擊的例子。

3.2 BAN邏輯缺陷產(chǎn)生的原因分析

之所以會(huì)產(chǎn)生上述問題，是因?yàn)樵贐AN邏輯分析時(shí)，存在著一些不精確的地方[4]：

① 初始假設(shè)：初始假設(shè)是BAN邏輯分析的一個(gè)重要步驟，然而對(duì)于這個(gè)步驟并沒有明確的可以依據(jù)的方法。通常這一步驟和分析人員的經(jīng)驗(yàn)有著較大的關(guān)系。在進(jìn)行BAN邏輯分析時(shí)，如果增加一個(gè)初始假設(shè)，就會(huì)得到協(xié)議是安全的結(jié)論；而如果去除這個(gè)條件，則會(huì)得出相反的結(jié)論。這一點(diǎn)是導(dǎo)致BAN邏輯缺陷的一個(gè)重要原因。

②協(xié)議理想化：理想化其實(shí)就是將要分析的協(xié)議用邏輯公式表示出來，但是BAN邏輯的理想化步驟本身其實(shí)是非形式化的，這就造成BAN邏輯分析協(xié)議缺乏有效性和正確性，沒有達(dá)到形式化方法分析協(xié)議的要求。

③語義：BAN邏輯缺少一個(gè)定義良好的語義，造成了BAN邏輯分析經(jīng)常會(huì)遭受重放攻擊。

④對(duì)協(xié)議的攻擊探測能力較弱：在BAN邏輯分析過程中有時(shí)不能有效檢測出對(duì)協(xié)議的重放攻擊，同時(shí)它也無法檢查出協(xié)議的并發(fā)運(yùn)行所帶來的各類攻擊。

3.3 BAN邏輯的改進(jìn)

為克服BAN邏輯的不足，學(xué)者們對(duì)BAN邏輯進(jìn)行了某些必要的改進(jìn)或擴(kuò)展，提出了許多擴(kuò)展的BAN 邏輯[5]。

GNY邏輯等對(duì)推理系統(tǒng)進(jìn)行了改進(jìn)；AT邏輯、VO邏輯、SVO邏輯等對(duì)語義進(jìn)行了改進(jìn)；MB邏輯等對(duì)理想化進(jìn)行了改進(jìn)。

歸納這些擴(kuò)展的BAN邏輯，在克服BAN邏輯的缺陷和推廣其應(yīng)用范圍上，取得了很大的成功。但相對(duì)來講擴(kuò)展的BAN邏輯推理規(guī)則更多，運(yùn)用起來復(fù)雜，還不如BAN邏輯簡單直觀實(shí)用。同時(shí)，它們的工作方式基本上與BAN邏輯一樣，并沒有從根本上有效地克服形式邏輯分析方法所特有的理想化步驟缺陷。

4 結(jié)束語

BAN邏輯為密碼協(xié)議第一次提供了一整套形式化分析方法，成功地找到密碼協(xié)議的許多缺陷及攻擊，這極大地推動(dòng)了密碼協(xié)議的分析及設(shè)計(jì)。但它也存在著致命的缺陷：當(dāng)邏輯發(fā)現(xiàn)協(xié)議中的錯(cuò)誤，每個(gè)人都相信那確實(shí)是有問題；當(dāng)邏輯證明一個(gè)協(xié)議是安全的，但沒有人敢相信它的正確性。所以采用BAN類邏輯這種方法可以進(jìn)行密碼協(xié)議分析和輔助設(shè)計(jì)，但還不能完全信任其分析結(jié)果。

參考文獻(xiàn)：

[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邏輯在協(xié)議分析中的密鑰猜測分析缺陷[J].計(jì)算機(jī)工程，2006，32(9):126-127，130.

[4]王亞弟，等.密碼協(xié)議形式化分析[M].北京:機(jī)械工業(yè)出版社，2006.

[5]馮彬.關(guān)于BAN 邏輯分析的改進(jìn)[J].中國科學(xué)院研究生院學(xué)報(bào)，2002，19(3):306-310.

收稿日期：2008-01-12

基金項(xiàng)目：江蘇省高校自然科學(xué)研究計(jì)劃（05KJD520166）；江蘇省高?！扒嗨{(lán)工程”資助；南通大學(xué)學(xué)生課外科技計(jì)劃資助

作者簡介：顧翔（1973-），男，江蘇南通人，副教授，碩士生導(dǎo)師，博士，研究方向：為協(xié)議工程，形式化技術(shù)。

注：“本文中所涉及到的圖表、注解、公式等內(nèi)容請(qǐng)以PDF格式閱讀原文?！?/p>