齊愛琴

（西北民族大學(xué)數(shù)學(xué)與計算機(jī)科學(xué)學(xué)院，甘肅 蘭州 730000）

用戶認(rèn)證協(xié)議的安全分析*

齊愛琴

（西北民族大學(xué)數(shù)學(xué)與計算機(jī)科學(xué)學(xué)院，甘肅 蘭州 730000）

認(rèn)證是網(wǎng)絡(luò)安全中最重要的一個安全目標(biāo)，所有其他的安全屬性例如完整性、不可否認(rèn)性、可信性等都依賴于通信雙方的認(rèn)證。因此，很多安全認(rèn)證協(xié)議被提出。而判斷協(xié)議是否有效的方法主要是模擬。模擬只能證明協(xié)議在制定的模擬環(huán)境下是否可以達(dá)到安全目標(biāo)。而對于正常真實的各種情況無法真正反應(yīng)。本文提出了模型檢測的方法來對其中一種用戶認(rèn)證協(xié)議進(jìn)行了驗證，通過模型檢測協(xié)議的安全屬性可以檢測系統(tǒng)能達(dá)到的任何狀態(tài),比模擬的結(jié)果更有效。

Needham-Schroeder協(xié)議;規(guī)范化;Casper和FDR2

1 概述

當(dāng)今，企業(yè)、政府或個人每天都需要通過網(wǎng)絡(luò)進(jìn)行信息交換。隨著網(wǎng)絡(luò)的普及，安全問題也日益突出。認(rèn)證是安全通信的基礎(chǔ)，也是網(wǎng)絡(luò)安全中最重要的一個安全目標(biāo)，所有其他的安全屬性例如完整性、不可否認(rèn)性、可信性等都依賴于通信雙方的認(rèn)證。因此，很多安全認(rèn)證協(xié)議被提出。但協(xié)議的設(shè)計極其容易出錯，使之不能正常工作。在實現(xiàn)和使用這些協(xié)議前，他們聲稱的安全屬性應(yīng)該被驗證，而普通的常用的方法是模擬。模擬只能證明模擬的協(xié)議在特定的模擬環(huán)境下可以達(dá)到的安全目標(biāo)。而對于正常的各種情況無法真實反應(yīng)。需要一個更有效的方法來完成這個功能。模型檢測就是其中之一。通過模型檢測協(xié)議的安全屬性可以在系統(tǒng)能達(dá)到的任何狀態(tài)被驗證。常用的工具是Ban logic[5，6], CAPl-es[2]和SPIN[3，4],安全協(xié)議的正式驗證仍然是一個新的領(lǐng)域。文獻(xiàn)1和文獻(xiàn)7采用BAN邏輯對特定協(xié)議進(jìn)行了驗證和分析。但由于BAN邏輯存在著初始假設(shè)沒有明確依據(jù)的方法、協(xié)議理想化、語義定義不明確、對協(xié)議的攻擊探測能力較弱等問題，使得協(xié)議分析的結(jié)果還有待進(jìn)一步驗證。在這篇論文中，我們采用Casper和FDR2工具對一種經(jīng)典的用戶認(rèn)證協(xié)議進(jìn)行了模型檢測和驗證。這種方法不是新的，只是將這種方法應(yīng)用在用戶認(rèn)證中是之前沒有的。

2 協(xié)議描述

經(jīng)典的Needham-Schroeder用戶認(rèn)證協(xié)議是基于對稱加密和第三方仲裁機(jī)構(gòu)的。整個系統(tǒng)的結(jié)構(gòu)包括申請發(fā)起用戶、第三方仲裁機(jī)構(gòu)和目標(biāo)用戶三個部分。每個用戶都有與第三方仲裁機(jī)構(gòu)共享的秘密密鑰。當(dāng)用戶之間要進(jìn)行通信時，需先通過第三方仲裁機(jī)構(gòu)完成用戶之間的認(rèn)證。認(rèn)證過程如圖1所示：

圖1 認(rèn)證過程圖

A、B是用戶的身份，S是第三方仲裁機(jī)構(gòu)的身份，Na是用戶A產(chǎn)生的隨機(jī)數(shù)，Nb是用戶B產(chǎn)生的隨機(jī)數(shù)。Kas是用戶A與第三方機(jī)構(gòu)S的共享密鑰，Kbs是用戶B與第三方機(jī)構(gòu)的共享密鑰，Kab是第三方機(jī)構(gòu)為用戶A和B通信產(chǎn)生的會話密鑰。我們給出對應(yīng)的協(xié)議描述如下：

第一步中，用戶A向第三方第三方仲裁機(jī)構(gòu)S發(fā)出申請自己想和用戶B通信的請求，第二步：收到消息的第三方仲裁機(jī)構(gòu)查找與用戶的共享密鑰Kas，并產(chǎn)生用戶A、B之間通信的會話密鑰Kab，用與用戶B的共享密鑰Kbs加密信息Kab，A即 {Kab，A}Kbs，然后將Na，B，Kab，{Kab，A}Kbs信息用Kas加密之后發(fā)送給用戶A，在第三步中，用戶A用Kas解密收到的信息，得到與用戶B的會話密鑰Kab，將{Kab，A}Kbs發(fā)送給用戶B。第四步：用戶B用與第三方仲裁機(jī)構(gòu)的共享密鑰解密收到的信息得到Kab，A，然后生成一個隨機(jī)數(shù)Nb，用得到的會話密鑰Kab加密之后發(fā)送給用戶A。第五步：用戶A收到B的信息后，用Kab解密得到隨機(jī)數(shù)Nb，計算Nb-1，并用會話密鑰加密后發(fā)給用戶B，用戶B收到信息后，得到A是合法用戶，從而認(rèn)證A的身份，認(rèn)證過程結(jié)束。

3 協(xié)議的形式化驗證

根據(jù)協(xié)議中用戶的工作方式，我們選擇模型檢查器FDR2來驗證模型的安全性，這是一個基于并發(fā)理論和CSP的模型檢測器。它主要用來檢查系統(tǒng)的安全屬性例如訪問控制、認(rèn)證、電子商務(wù)、移動代理、web服務(wù)、AXML文檔等。FDR2中的規(guī)范化語言是CSP。但使用這種語言來模型化系統(tǒng)是耗時的并且易于出錯。所以我們使用Casper產(chǎn)生CSP模型。Casper傳遞安全協(xié)議的規(guī)范給CSP以便于被FDR2分析。它也可以用于傳遞輸出消息到可讀格式。

驗證認(rèn)證協(xié)議的第一步是用Casper模型化協(xié)議。協(xié)議的模型化包括兩部分：帶有形式變量的模板參數(shù)的協(xié)議描述和協(xié)議實際使用的場景描述。形式變量最終會被實際變量所替代。

關(guān)于用戶認(rèn)證協(xié)議的模板如下：

協(xié)議的描述用來規(guī)范化消息交換。第1步對應(yīng)協(xié)議中的第1步，用戶將自己的身份A、用戶B的身份B和隨機(jī)數(shù)Na發(fā)給第三方機(jī)構(gòu)。第2步對應(yīng)協(xié)議第2步，第三方機(jī)構(gòu)回復(fù)信息給用戶A，用戶A用密鑰Kas解密消息得到Na，B，Kab，{Kab，A}Kbs，與自己存儲的Na比較看是否相等，若相等證實信息是第三方機(jī)構(gòu)發(fā)來的。第3步對應(yīng)協(xié)議第3步，用戶A將{Kab，A} Kbs發(fā)送給用戶B，用戶B解密信息，得到Kab，A，從而知道是用戶A要與自己通信。第4步對應(yīng)協(xié)議第4步，用戶B生成一個隨機(jī)數(shù)Nb并用Kab加密之后發(fā)送給用戶A來驗證A的身份的真實性。用戶A解密得到Nb。第5步對應(yīng)協(xié)議第5步，用戶A將得到的隨機(jī)數(shù)減一，用Kab加密之后發(fā)送給用戶B，用戶B比較自己存儲的隨機(jī)數(shù)與收到隨機(jī)數(shù)之間是否差一，若是，認(rèn)證通過。

我們只給出了一對用戶之間認(rèn)證的模型，事實上，所有用戶之間的通信都是相同的，因此檢測一對用戶結(jié)點的安全屬性是足夠的。如果對一對用戶結(jié)點有效，那么對所有用戶節(jié)點都有效。這對FDR2的驗證也是非常有益的。如果有很多個用戶結(jié)點同時驗證的話，機(jī)器的內(nèi)存會全部耗盡，檢查無法終止。

定義了協(xié)議的模板后，需要檢測的安全屬性也就規(guī)范化了。在用戶認(rèn)證協(xié)議中，安全屬性是用戶之間的認(rèn)證。相應(yīng)的輸入文件是#specification。這個認(rèn)證規(guī)范可以用下面的聲明來完成：Agreement[A，B，[Nb]]協(xié)議規(guī)定A被B認(rèn)證，Agreement[B，A，[Nb]]協(xié)議規(guī)定B被A認(rèn)證。

正如我們之前提到的，協(xié)議的安全驗證不是在協(xié)議的模板上來完成，而是在一個特定的場景中。對用戶認(rèn)證協(xié)議來說，場景包括二個部分：協(xié)議的初始方（想去被認(rèn)證的用戶）和響應(yīng)方（第三方仲裁機(jī)構(gòu)和執(zhí)行認(rèn)證的用戶）。場景的定義使用真實變量來給出：

在模型化協(xié)議的最后一步是關(guān)于惡意分子的規(guī)范說明，惡意分子可以破壞協(xié)議，它知道所有用戶和第三方的身份，由于本協(xié)議是建立在第三方仲裁機(jī)構(gòu)是可信的、公平的基礎(chǔ)上的。如果第三方機(jī)構(gòu)與惡意分子勾結(jié)來產(chǎn)生對應(yīng)的會話密鑰Kis，并產(chǎn)生一個隨機(jī)數(shù)am，那相應(yīng)的惡意分子的場景描述如下：

完成輸入文件后，Casper用來生成協(xié)議的CSP規(guī)范，這個規(guī)范用作FDR2的輸入。完成協(xié)議的模型化之后,在linux環(huán)境中采用FDR2進(jìn)行驗證，F(xiàn)DR2驗證的第一步是構(gòu)造模型化系統(tǒng)的狀態(tài)。然后指定的屬性在每種狀態(tài)下被驗證。如果在每個狀態(tài)下都可以通過驗證，則協(xié)議的屬性是安全的。否則被認(rèn)為是無效的。在正常的狀態(tài)下即只有用戶和第三方仲裁機(jī)構(gòu)的情況下，協(xié)議運行正常，認(rèn)證安全屬性得到驗證。在有惡意分子存在情況下或者第三方仲裁機(jī)構(gòu)與惡意分子勾結(jié)情況下，協(xié)議的認(rèn)證安全屬性驗證錯誤。由此可以分析出Needham-Schroeder協(xié)議的安全性有待改進(jìn)，可以對第三方仲裁機(jī)構(gòu)設(shè)置可信值來評估他的真實可信性或者采用公鑰基礎(chǔ)設(shè)施來進(jìn)一步完善協(xié)議，從而提高協(xié)議的認(rèn)證安全。

4 總結(jié)

在這篇論文中，我們演示了如何用規(guī)范化驗證技術(shù)來檢測一個安全協(xié)議的有效性。使用的工具是Casper和FDR2。這個方法也可以適用于任何模型檢測。首先，使用驗證工具的規(guī)范化語言明確規(guī)定協(xié)議的各個部分。轉(zhuǎn)換成一個驗證執(zhí)行的實際協(xié)議。這步很重要，如果模型錯誤或者與實際協(xié)議比較缺少相關(guān)限制條件的話，驗證結(jié)果將會出錯。接下來制定需要驗證的安全屬性。在這里我們只驗證了認(rèn)證屬性，其他的屬性也可以被驗證。最后一步是實際執(zhí)行的驗證情況。FDR2證明了該協(xié)議的安全性有待提高，沒有達(dá)到安全目標(biāo)。接下來我們可以完成對稱密鑰的建立或者公鑰基礎(chǔ)設(shè)施的改進(jìn)等工作，協(xié)議的使用范圍可以進(jìn)一步擴(kuò)展。

[1] 田建波,王育民.認(rèn)證協(xié)議的形式分析[J].通信保密,1998, 76(4)：8-12.

[2] John D.Aprshall,an analysis of the secure routing protocol for mobile ad hoc network route discovery：using intuitive. reasoning and formal verification to identify flaws,Msc thesis, Florida State University,2003.

[3] Davor Obradovic,Formal Analysis of convergence of routing protocols,PH.Dthesis,university of pensylvania,2000.

[4] Todd R.Andel,Formal Security Evaluation of ad hoc routing protocols,PH.Dthesis,,Florida State University,2007.

[5] 張玉清,李繼紅，肖國鎮(zhèn).密碼協(xié)議分析工具—BAN邏輯及其缺陷[J].西安電子科技大學(xué)學(xué)報,1999,26(3)：376-378.

[6] 張玉清,吳建平，李星.BAN類邏輯的由來與發(fā)展[J].清華大學(xué)學(xué)報,2002,42(1)：96-99.

[7] 王正才,許道云,王曉峰,等.BAN邏輯的可靠性分析與改進(jìn)[J].計算機(jī)工程,2012,38(17)：110-115.

TN915.04

中央高校科研項目(x31920150079)。