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

齊愛琴

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

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

齊愛琴

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

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

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

1 概述

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

2 協(xié)議描述

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

圖1 認證過程圖

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

第一步中，用戶A向第三方第三方仲裁機構S發(fā)出申請自己想和用戶B通信的請求，第二步：收到消息的第三方仲裁機構查找與用戶的共享密鑰Kas，并產生用戶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用與第三方仲裁機構的共享密鑰解密收到的信息得到Kab，A，然后生成一個隨機數(shù)Nb，用得到的會話密鑰Kab加密之后發(fā)送給用戶A。第五步：用戶A收到B的信息后，用Kab解密得到隨機數(shù)Nb，計算Nb-1，并用會話密鑰加密后發(fā)給用戶B，用戶B收到信息后，得到A是合法用戶，從而認證A的身份，認證過程結束。

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

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

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

關于用戶認證協(xié)議的模板如下：

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

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

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

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

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

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

4 總結

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

[1] 田建波,王育民.認證協(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].西安電子科技大學學報,1999,26(3)：376-378.

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

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

TN915.04

中央高?？蒲许椖?x31920150079)。