ＢＡＮ邏輯及其在認證協議性質分析中的應用研究

摘要：在各類安全協議中，認證協議分析正成為熱點，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。上述消息可以用公式描述如下：

消息① 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）

下面就對其進行BAN分析。

第一步進行初始假設，在此協議中，共進行如下8條初始假設：

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

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

③A︱≡S ?A Kas? SA相信S對A和S共享密鑰Kas有仲裁權

④B︱≡S ?B Kas? SB相信S對B和S共享密鑰Kbs有仲裁權

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

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

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

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

第二步進行協議理想化：

第①、②條消息省略，因為它們對分析協議的邏輯屬性沒有作用。

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

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

消息⑤ B→A：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格式閱讀原文。”