運用SPIN對云環境雙向認證協議Nayak的安全性驗證

肖美華 梅映天 李 偉

(華東交通大學軟件學院 江西 南昌 330013)

運用SPIN對云環境雙向認證協議Nayak的安全性驗證

肖美華 梅映天 李 偉

(華東交通大學軟件學院 江西 南昌 330013)

隨著云計算的發展，由欺詐行為驅動的竊取云資源和云服務的行為日趨嚴重，導致云資源提供商與用戶間出現信任危機。Nayak協議是一種改進的云環境雙向認證協議，用于保障用戶安全登錄云服務器，防止第三方惡意竊取用戶信息。采用對稱密鑰密碼體系對Nayak協議進行加密，基于Dolev-Yao攻擊者模型，提出四通道并行建模法描述攻擊者能力。該建模方法解決了Nayak協議并行運行過程中的模型檢測問題以及安全隱患，優化了模型復雜度與存儲狀態數。運用SPIN模型驗證工具分析表明采用對稱密鑰密碼體系對Nayak協議加密不安全。此方法可運用于類似復雜協議形式化分析與驗證。

Nayak協議 模型檢測 四通道并行建模 對稱密鑰加密

0 引 言

認證屬于云安全領域中最需要重視的安全問題之一，其中云認證安全協議涉及到對用戶與服務器的雙向認證、建立雙方的會話密鑰等相關技術，保證信息溝通的機密性、完整性、匿名性以及有效性，保證信息不泄露給任何未被授權的用戶，保證信息的完整、不被丟失與篡改等，還能保證傳輸信息的實時有效性。

形式化方法[1]主要包括模型檢測[2]與定理證明[3]兩個分支，模型檢測能夠自動驗證系統是否滿足刻畫的性質并且驗證速度快、效率高，若不滿足性質要求，會提供攻擊序列圖。SPIN(Simple Promela Interpreter)[4-5]是一種著名的模型驗證工具，具有語意清晰、通俗易懂、高效率等特點。1989年SPIN的第一版本問世，主要驗證ω-regular屬性，1995年引入線性事態邏輯和偏序規約，2001年推出的SPIN4.0支持C語言植入，改善了SPIN的使用局限性，2003年推出的SPIN4.1采用深度優先搜索算法，進一步優化了模型檢測的效率。

Nayak等提出一種改進的云環境下雙向認證協議方案[6]，成功完成雙向認證后協商好了會話密鑰;詹麗[7]用BAN邏輯對Nayak協議進行了驗證，并發現其中漏洞，但BAN邏輯從方法上看，由于其限制性很大程度上阻礙其分析范圍，學者們進行了一系列改進，得到了AT邏輯、GNY[8]邏輯等類邏輯，而文獻[7]依舊使用BAN邏輯驗證協議安全性，準確度低，代表性弱；從結果來看，使用BAN邏輯對Nayak協議的驗證，只能通過邏輯推理證明協議的不安全，不能完全直觀地反映協議的運行過程，實際操作性弱。

Maggi等[9]以Needham-Schroeder為例，基于Dolev等攻擊者模型[10]，提出一種安全協議模型檢測的建模方法。本文針對Nayak協議，對Maggi方法做出改進，以四通道并行建模方式對協議進行建模，并驗證Nayak協議是否滿足身份認證性質。

1 模型檢測技術

模型檢測是一種基于有限狀態模型并檢驗該模型的期望特性的技術，為確定檢驗的系統模型是否某些性質需搜索模型狀態空間，若驗證性質未滿足時，搜索過程將被終止并給出反例。檢測結果所得的數據信息對系統設計者排錯有極大幫助。目前模型檢測技術以其簡潔明了、自動化程度高以及實用性強等特性已經在計算機芯片設計、軟件可靠性、通信可靠性、通信協議、控制系統等領域得到廣泛應用。基本原理如圖1所示。

圖1 模型檢測基本原理圖

對于表示系統性質某種時態邏輯公式或者一類有窮狀態并發系統，模型檢測技術的關鍵在于是否能找到算法判定系統類中的任一給定系統是否滿足公式類中任意給定的一個時態邏輯公式。如圖1所示，其算法的輸入分別是待驗證系統模型M和系統屬性φ，若模型M滿足性質φ，則給出true結果，否則給出false以及反例詳細說明。

模型驗證工具SPIN是一個對并發系統進行形式化驗證的模型檢測工具。它支持promela規約語言并用于驗證并發系統進程的正確性。SPIN在仿真模式下可很好地捕捉模型中變量的變化過程，也能方便地可視化仿真過程。對與違法模型性質的反例，在驗證模式下會有詳細數據說明，在仿真模式下會給出錯誤軌跡圖。2002年，Holzmann(SPIN的設計者)得到了ACM頒發的軟件系統開發獎。仿真與驗證結構流程見圖2。

圖2 SPIN仿真與驗證結構流程

2 Nayak協議

該協議的主要思想是用戶需要注冊初始化，然后用戶通過雙向認證進行授權訪問，并且在雙向認證過程中通過確認隨機數來實現認證。注冊階段抽象協議流程如圖3所示。

(1) 當用戶需要訪問云資源時，需要一個有效的郵箱賬號(Email_id)。 用戶選擇一個合法的用戶賬號(User_id)，服務器檢驗該賬號是否有效。

(2) 用戶輸入有效的郵箱賬號，服務器通過該賬號發送動態口令(Token)給用戶，用戶輸入動態口令。

(3) 服務器檢測動態口令以及密碼(Pwd),如有效則成功。

(4) 通過單向哈希函數生成的B發送給用戶。

圖3 注冊抽象協議流程

登錄與驗證抽象協議流程如圖4所示。

(1) 用戶生成一個隨機數Nc，然后通過AES(Advanced Encryption Standard)加密技術生成密鑰K得到消息(M_client)，將其發送給服務器。

(2) 服務器收到消息后，對其解密，將解密獲得的Nc與隨機生成的Ns加密成M_server發送給用戶。

(3) 用戶收到M_server后解密，檢測獲得的Nc與擁有的Nc是否相等，相等則認為服務器可信。

(4) 用戶將解密獲取的Ns用密鑰K′加密成消息(M)發送給服務器。

(5) 服務器計算出K′,得到Ns，將其與擁有的Ns進行比對，相等則認為用戶和服務器都可信。

圖4 登錄與驗證抽象協議流程

本文將對登錄與驗證階段進行研究與分析，由于協議使用對稱密鑰加密解密，我們可將步驟(1)使用的加密技術得到的密鑰K，看成是用戶與服務器的共享密鑰，步驟(4)使用的加密技術得到的K′，看成用戶與服務器的新共享密鑰，得到的Nayak協議如下：

(1) client→server:{Nc}Kcs

(2) server→client:{Nc,Ns}Kcs

(3) client→server:{Ns}K_cs

其中Kcs表示用戶與服務器的共享密鑰， 表示用戶與服務器的新共享密鑰。

3 Nayak協議建模

本文要驗證的協議共有兩個合法主體和一個非法主體，分別是Client、Server和Intruder。為了方便，簡寫成C、S、I。

3.1 四通道并行建模

攻擊者模型遵循Dolev-Yao模型,Dolev-Yao規定攻擊者可以竊取合法主體發送的所有消息，并能對所竊取的消息進行刪除、轉發、篡改等。然而，在模型檢測中，對攻擊者能力的描述可能會出現大量重復子消息項以及忽略多輪協議并行的情況，造成進程間交叉運行所產生的狀態遷移量增大，甚至可能發生狀態爆炸[11-12]問題。本文以四通道并行建模方式來描述攻擊者能力。

模型定義了四個通道：發起者與攻擊者兩個通道；響應者與攻擊者兩個通道。

兩個合法主體之間是沒有通道相連的，因為兩個合法主體在進行消息交換時，攻擊者總是能竊聽或竊取到合法主體發送的所有消息，合法主體所接收的消息總是攻擊者發送的。并行建模是指合法主體C、S既扮演了發起者，也扮演了響應者，例如C在發送消息的同時，可能會收到S發送的消息。示意圖如圖5所示。

圖5 四通道并行建模

3.2 誠實主體建模

首先對協議數據項名稱進行簡化命名，主體名：C、S、I，挑戰數：Nc(C作為發起者所用的隨機數)、N_c(C作為響應者所用的隨機數)、Ns(S作為響應者所用的隨機數)、N_s(S作為發起者所用的隨機數)，共享密鑰：CS、C_S(新共享密鑰)。

Nayak協議的誠實主體為Client發起者與Server響應者，proctype PC()、proctype PS()為其對應的進程。四個通道分別是發起者PC的消息通道為ch1與ch2，響應者PS的消息通道為ch3與ch4。

由于協議中傳輸的消息數不同，發起者PC的通道定義如下：

chan ch1=[0] of {mtype, mtype, mtype};

chan ch2=[0] of {mtype, mtype, mtype,mtype};

同理，響應者PS的通道定義如下：

chan ch3=[0] of {mtype, mtype, mtype};

chan ch4=[0] of {mtype, mtype, mtype,mtype};

其中[0]表示通道中傳遞數據和接收數據同步。

對本文所用的消息類型做枚舉說明：

mtype = {C,S,Nc,Ns,N_c,N_s,R,gD,CS,C_S,,x};

這里符號表示：R為不可識別的主體，x代表任意誠實主體，gD為泛型數據量符號化。

對Client的描述，具體實現代碼如下：

{

mtype g1;

mtype g2;

atomic {

IniRunning(self, party);

ch1!self,nonce, CS;

}

atomic {

After investigation, your obedient servants find that on the 25th of the first month of the 36th year of Qianlong, Lifan Yuan presented this memorial:

ch2?g2,eval(nonce), g1, eval(CS);

IniCommit(self, party);

ch1! self,g1,C_S;}}

在PC發起者進程中，self與party分別表示消息發起者與接收者，g1、g2表示泛型變量，發起者一共完成了兩次發送操作和一次接收操作。其中發送消息語句ch1？self,nonce,CS的含義是：self(發送者C)發送自己的隨機數，用C與S的共享密鑰加密。atomic表示promela語言定義的原子序列語法規則，運用該語法規則可使進程交叉運行次數減少，把接收操作與下一次發送操作放在一個atomic中同時完成，能有效地減少狀態空間。原子謂詞表示協議的性質，原子謂詞變量的值由模型的宏定義來更新記錄，IniRunning、IniCommit和ResRunning、ResCommit為模型程序中定義的四個宏，其中IniRunning表示發起者與響應者會話，IniCommit表示發起者提交了與響應者的會話，宏定義如下：

#define IniRunning(x,y) if

::((x==C)&&(y==S))->IniRunningCS=1

::((x==S)&&(y==C))->IniRunningSC=1

:: else skip

fi

#define IniCommit(x,y) if

::((x==C)&&(y==S))->IniCommitCS=1

::((x==S)&&(y==C))->IniRunningSC=1

:: else skip

fi

#define ResRunning(x,y) if

::((x==C)&&(y==S))->ResRunningCS=1

::((x==S)&&(y==C))->ResRunningSC=1

:: else skip

fi

#define ResCommit(x,y) if

::((x==C)&&(y==S))->ResCommitCS=1

::((x==S)&&(y==C))->ResCommitSC=1

:: else skip

fi

3.3 運用LTL公式刻畫Nayak協議安全性質

LTL線性時態邏輯[13-14]被運用于描述協議所需要滿足的屬性，通過判斷所建立的模型是否滿足所描述的屬性公式來驗證協議的安全性。

模型的每一條性質都需要用一個promela全局變量表示，初始化操作如下所示：

bit IniRunningCS = 0;bit IniCommitCS = 0;

bit ResRunningCS = 0;bit ResCommitCS = 0;

bit IniRunningSC = 0;bit IniCommitSC = 0;

bit ResRunningSC = 0;bit ResCommitSC = 0;

其中IniRunningCS表示client發起與server的會話，初始值為0表示client沒有發起與server的會話，IniCommitCS表示client提交與server的會話，初始值為0表示client沒有提交與server的會話，其他與之類似。

根據3.2節給出的所有屬性描述函數的定義與屬性變量的初始化，用戶與服務器間的身份認證屬性具體描述如下：

C必須在S發起會話后才能提交與S的對話或者S從來沒有發起與C的會話，LTL(線性時態邏輯)刻畫如下：

([](([]!IniCommitCS)||(!IniCommitCS U

ResRunningCS)))

S必須在C發起會話后才能提交與C的對話或者C從來沒有發起與S的會話，LTL(線性時態邏輯)刻畫如下：

([](([]!IniCommitSC)||(!IniCommitSC U

ResRunningSC)))

將這兩個LTL公式運用邏輯符連接后得到完整LTL屬性描述：

([](([]!IniCommitCS)||(!IniCommitCS U

ResRunningCS)))&&([](([]!IniCommitSC)||

(!IniCommitSC U ResRunningSC)))

3.4 攻擊者建模

攻擊者建模通常是模型檢測中最重要的一部分，攻擊者能力的強弱也會直接影響模型檢測的效果以及效率。根據Dolev-Yao模型構建攻擊者知識庫函數，把攻擊者獲取的知識提取出來，建立單獨的知識庫存儲攻擊者知識，攻擊者根據這些知識偽造、轉發消息。構建攻擊者知識庫函數需要找到攻擊者需要表示的知識，而攻擊者可以學會的知識集合A與攻擊者需要學會的知識集合B的交集即攻擊者需要表示的知識，具體如下：

攻擊者可以學會的知識：由誠實主體的發生語句所得。

ch1!self,nonce, CS;

ch1! self,g1,C_S;

ch4!self,g1, nonce, CS;

利用靜態分析法縮減隨機變量的取值范圍，降低搜索狀態數，例如client將隨機變量g1用新共享密鑰C_S加密發送給server，對于client來說，它不確定g1是不是server的隨機數，因此變量g1取值范圍為{Nc,N_c,Ns,N_s}，nonce的取值范圍為{Nc，N_s},響應者進程中變量g1取值范圍為{Nc,N_c,Ns,N_s},具體如表1。

表1 攻擊者可以學會的知識

攻擊者需要學會的知識:由誠實主體的接收語句所得。

ch2?g2,eval(nonce), g1, eval(CS);

ch3 ?g2,g1, eval(CS);

ch3?g3,eval(nonce),eval(C_S);

利用靜態分析法分析得出，發起者進程中nonce取值范圍為{Nc,N_s}，變量g1取值范圍為{Nc,N_c,Ns,N_s}，響應者進程中變量g1取值范圍為{Nc_,Ns}，具體如表2。

表2 攻擊者需要學會的知識

表1與表2的交集即攻擊者需要表示的知識項:

{Nc}Kcs,{N_s}Kcs,{N_c}K_cs,{Ns}K_cs,{Nc,Ns}Kcs,{Nc,N_c}Kcs,{N_s,Ns}Kcs,{N_s,N_c}Kcs

根據以上分析，攻擊者模型的代碼框架如下：

proctype PI() {

bit k_Nc_CS=0;

…

bit k_N_s_N_c_CS=0;

/*需要表示的知識初始化*/

mtype x1;mtype x2;mtype x3;

do

::ch2!x,Nc,Ns,(k_Nc_Ns_CS->CS:R)

::ch4!x,Nc,Ns,(k_Nc_Ns_CS->CS:R)

::ch2!x,Nc,N_c,(k_Nc_N_c_CS->CS:R)

::ch4!x,Nc,N_c,(k_Nc_N_c_CS->CS:R)

::ch2!x,Ns,Ns,(k_N_s_Ns_CS->CS:R)

::ch4!x,N_s,Ns,(k_N_s_Ns_CS->CS:R)

::ch2!x,N_s_,N_c,(k_N_s_N_c_CS->CS:R)

::ch4!x,N_s_,N_c,(k_N_s_N_c_CS->CS:R)

::ch3!x,Nc,(k_Nc_CS->CS:R)

::ch1!x,Nc,(k_Nc_CS->CS:R)

::ch3!x,N_s_,(k_N_s_CS->CS:R)

::ch1!x,N_s_,(k_N_s_CS->CS:R)

::ch3!x,N_c_,(k_N_c_C_S->C_S:R)

::ch1!x,N_c_,(k_N_c_C_S->C_S:R)

::ch3!x,Ns,(k_Ns_C_S->C_S:R)

::ch1!x,Ns,(k_Ns_C_S->C_S:R)

::d_step { ch2? _,x1,x2,x3->k2(x1,x2,x3);

x1 = 0;x2 = 0;x3 = 0; }

::d_step { ch4? _,x1,x2,x3->k2(x1,x2,x3);

x1 = 0;x2 = 0;x3 = 0; }

:: d_step { ch1 ? _,x1,x2->k1(x1,x2);

x1 = 0;x2 = 0; }

:: d_step { ch3 ? _,x1,x2->k1(x1,x2);

x1 = 0;x2 = 0;}

od}

4 實驗結果與分析

使用SPIN驗證工具對上述模型進行驗證，發生了屬性違反，自動生成了并行攻擊路徑，攻擊序列圖如圖6所示。

圖6 攻擊序列圖

得到如下攻擊序列：

C→I:{Nc}Kcs I→C:{Nc}Kcs

C→I:{Nc,N_c}Kcs I→C:{Nc,N_c}Kcs

C→I:{N_c}K_cs I→C:{N_c}K_cs

協議開始運行時，發起者C將Nc(C作為發起者所用的隨機數)以CS共享密鑰加密發送給攻擊者，這樣攻擊者I就掌握了相關信息，隨后發起者C又將N_c(C作為響應者所用的隨機數)以CS共享密鑰加密發送給攻擊者，攻擊者I冒充了響應者S與發起者C進行了三次會話。然而，響應者S與發起者C卻并不知情，這就表明該協議充滿危險性。

如圖7所示，ResCommitCS,ResRunningCS，IniCommitSC,IniRunningSC為0，IniCommitCS，IniRunningCS,ResCommitSC,ResRunningSC為1，表示在整個協議運行中，發起者(響應者)C開始并提交與響應者(發起者)S的會話，但響應者(發起者)S沒有參與或提交一次會話。

圖7 性質違反信息

圖8描述單個全局系統狀態需要64字節的內存，檢測后狀態樹的高度達到27層，并且檢測到1項錯誤。transitions和states-stored的數量越少表示狀態遷移量越少，系統存儲的狀態量越少，驗證效率越高，且不易引起狀態爆炸。state-vector和depth-reached屬性表示狀態矢量數和深度優先搜索的深度，數量越少表明模型越優秀，檢測效率越高。并且，從圖8可知，本文構建的模型并未出現狀態爆炸等情況。

圖8 模型驗證結果信息

5 結 語

隨著信息網絡的快速發展，云服務走進人們的視野。與此同時，因云環境的開放性等特點給云計算的安全帶來極大的挑戰。因此，云安全協議為了能夠有更多功能和更強大的安全性，也需更為復雜。本文以Nayak協議為例，采用對稱密鑰密碼體系對Nayak協議進行加密，提出四通道并行建模法對協議建模，該建模方法適用于多協議或多主體并行運行的環境，有效緩解了狀態爆炸問題。最后運用SPIN模型檢測工具找到一條攻擊路徑，發現協議中存在的安全漏洞。下一步研究將嘗試對Nayak協議進行改進，并對其安全性進行驗證。

[1] Xiao M,Jiang Y,Liu Q.On formal analysis of cryptographic protocols and supporting tool[J].Chinese Journal of Electronics,2010,19(2):223-228.

[2] Clarke E M.Model checking[M].Cambridge,MA:MIT Press,1999.

[3] Xiao M,Ma C,Deng C,et al.A Novel Approach to Automatic Security Protocol Analysis Based on Authentication Event Logic[J].Chinese Journal of Electronics,2015,24(1):187-192.

[4] Holzmann G J.The model checker SPIN[J].IEEE Transactions on software engineering,1997,23(5):279-295.

[5] Xiao Meihua,Wan Zilong,Liu Hongling.The Formal Verification and Improvement of Simplified SET Protocol[J].Journal of Software,2014,9(9):2302-2308.

[6] Nayak S K,Mohapatra S,Majhi B.An Improved Mutual Authentication Framework for Cloud Computing[J].International Journal of Computer Applications,2012,52(5):36-41.

[7] 詹麗.云計算中基于Smartcard的雙向認證安全協議的研究與形式化分析[D].廣州:暨南大學,2014.

[8] 馬成林,肖美華,鄧春艷,等.基于改進GNY邏輯的Kerberos*協議安全性分析[J].計算機與數字工程,2014(10):1758-1762,1882.

[9] Maggi P,Sisto R.Using SPIN to verify security properties of cryptographic protocols[M]//Model Checking Software.Springer Berlin Heidelberg,2002:187-204.

[10] Dolev D,Yao A C.On the security of public key protocols[J].Information Theory,IEEE Transactions on,1983,29(2):198-208.

[11] 侯剛,周寬久,勇嘉偉,等.模型檢測中狀態爆炸問題研究綜述[J].計算機科學,2013,40(6A):77-86,111.

[12] Groote J F,Kouters T W D M,Osaiweran A.Specification guidelines to avoid the state space explosion problem[J].Software Testing,Verification and Reliability,2015,25(1):4-33.

[13] Barnat J,Cerná I.Distributed breadth-first search LTL model checking[J].Formal Methods in System Design,2006,29(2):117-134.

[14] Xiao M,Bickford M.Logic of Events for Proving Security Properties of Protocols[C]//International Conference on Web Information Systems and Mining.IEEE Computer Society,2009:519-523.

SECURITYVERIFICATIONOFMUTUALAUTHENTICATIONPROTOCOLNAYAKINCLOUDENVIRONMENTWITHSPIN

Xiao Meihua Mei Yingtian Li Wei

(SchoolofSoftware,EastChinaJiaotongUniversity,Nanchang330013,Jiangxi,China)

With the development of cloud computing, the behavior of cloud resources and cloud services driven by fraud is becoming more and more serious, leading to cloud trust crisis between resource providers and users. Nayak protocol is an improved mutual authentication protocol in cloud environment, it used to protect the user’s security login cloud server and prevent the third-party malicious theft of user information. We use the symmetric key cryptosystem to encrypt the Nayak protocol. On the basis of Dolev-Yao attacker model, we propose a four-channel parallel modeling method to describe the attacker’s ability. The modeling method solved the problem of model detection and security hidden trouble while Nayak protocol run in parallel, and optimized the model complexity and storage state. We introduced the SPIN model validation tools in this paper. The validation tool analysis shows that the symmetric key cryptography is not secure for Nayak protocol encryption. This method can be applied to formal analysis and verification of similar complex protocols.

Nayak protocol Model checking Four-channel parallel modeling method Symmetric-key cryptography

TP309

A

10.3969/j.issn.1000-386x.2017.10.053

2016-11-17。國家自然科學基金項目(61163005，61562026)；計算機軟件新技術國家重點實驗室開放課題項目(KFKT2012B18)；江西省自然科學基金項目(2013BAB201033)；江西省高校科技落地計劃項目(KJLD13038)；江西省對外科技合作技術項目(20151BDH80005)；華東交通大學研究生創新計劃項目(YC2014-X007)。肖美華，教授，主研領域：信息安全，軟件形式化方法。梅映天，碩士生。李偉，碩士生。