ＢＡＮ邏輯在一類中間入侵攻擊協議分析中的缺陷

摘 要：BAN邏輯通過對密鑰協商協議的運行進行形式化分析，研究密鑰協商雙方通過相互接收和發送消息從最初的信仰逐漸發展到協議最終要達到的目的，證明協議是否能夠達到預期目標，以此發現協議中存在的一些缺陷。通過一個端到端協議例子的證明和分析，指出BAN邏輯對于一類密鑰協商協議中存在的中間入侵攻擊分析方面存在缺陷，還需要結合非形式化的分析方法來加以解決。

關鍵詞： BAN邏輯；密鑰協商協議；中間入侵；棣弗—赫爾曼

中圖分類號：TP301.6文獻標志碼：A

文章編號：1001—3695(2007)03—0149—03

密碼協議分析與設計的首要因素是協議安全性問題。已有許多被開發出來分析密碼協議的形式化方法，但是它們都有其局限性，沒有一種方法能夠斷言協議是數學上安全的。密鑰協商協議是最基本的協議之一。協議是否正確，常用的方法有兩種，即采用逐個對協議進行攻擊的檢驗方法和應用形式化的分析工具。其中最典型的是BAN邏輯，但是BAN邏輯的抽象級別過高，分析范圍過于狹窄，在協議分析中存在一些缺陷。本文通過一個端到端(Station to Station)密鑰協商協議的證明和分析來指出其不足，并對密鑰協商協議進行了改進。

1 使用的BAN邏輯規則子集

BAN邏輯是一種基于信念的模態邏輯；在BAN邏輯的推理過程中，參加協議主體的信念隨消息交換而不斷演進。

1.1 BAN邏輯結構語句要素

A，B，P，Q表示通信主體；

KAB表示A和B共享的通信密鑰。

X，Y表示任意語句。

K表示任意密鑰。

1.2 BAN邏輯的幾條主要規則

2 BAN邏輯對STS協議的安全性分析

以一個端到端（STS）密鑰協商協議的正確性證明來對BAN邏輯進行一些分析。

2.1 STS協議描述

STS協議是Diffie—Hellman密鑰交換方案的一個應用，它是一個典型的密鑰協商協議，用于網絡環境下用戶雙方能夠安全地交換一個密鑰。

2.2 BAN邏輯對STS協議的推理

(1)初始狀態形式化描述

在協議的運行中，有部分信息是用發送方的私鑰來簽名的，需要用發送方的公鑰來進行驗證：

A向B發送自己的身份標志，A試圖與B建立通信；而攻擊者I截獲該信息，然后冒充A向B發送自己的身份標志I；于是B開始與I協商通信密鑰。在整個協議運行過程中，A認為它正在與B運行協議，然而B認為它在與I運行協議，因為它不會收到A的信息。雖然該協議運行不會導致嚴重的后果，中間入侵者不可能得到密鑰等有價值的信息，但是它導致A持有不正確的信仰：A始終相信B，認為B正在與A進行通信。

對STS協議的攻擊很容易防范，只需在A和B的簽名中包括A和B的身份標志即可。協議改進如下：

4 結束語

通過BAN邏輯對STS密鑰協商協議的分析，可以證明協議是否能夠達到預期目標。但是通過上述分析發現，BAN邏輯對于密鑰協商過程中諸如中間入侵攻擊卻不能加以分析，還需借助于非形化的方法來分析和改進協議，這是BAN邏輯還需要不斷完善的地方。通過以上分析，筆者認為，在BAN邏輯的改進和研究中，應該增加對入侵者行為的描述能力，適應更多類型的安全協議分析；使理想化過程形式化或符號化；建立基于邏輯驗證法和模型檢測技術的組合協議分析理論；在語法分析的同時進行語義分析等。

本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文。