運(yùn)用SPIN對(duì)云環(huán)境雙向認(rèn)證協(xié)議Nayak的安全性驗(yàn)證

肖美華 梅映天 李 偉

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

運(yùn)用SPIN對(duì)云環(huán)境雙向認(rèn)證協(xié)議Nayak的安全性驗(yàn)證

肖美華 梅映天 李 偉

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

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

Nayak協(xié)議 模型檢測(cè) 四通道并行建模 對(duì)稱密鑰加密

0 引 言

認(rèn)證屬于云安全領(lǐng)域中最需要重視的安全問(wèn)題之一，其中云認(rèn)證安全協(xié)議涉及到對(duì)用戶與服務(wù)器的雙向認(rèn)證、建立雙方的會(huì)話密鑰等相關(guān)技術(shù)，保證信息溝通的機(jī)密性、完整性、匿名性以及有效性，保證信息不泄露給任何未被授權(quán)的用戶，保證信息的完整、不被丟失與篡改等，還能保證傳輸信息的實(shí)時(shí)有效性。

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

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

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

1 模型檢測(cè)技術(shù)

模型檢測(cè)是一種基于有限狀態(tài)模型并檢驗(yàn)該模型的期望特性的技術(shù)，為確定檢驗(yàn)的系統(tǒng)模型是否某些性質(zhì)需搜索模型狀態(tài)空間，若驗(yàn)證性質(zhì)未滿足時(shí)，搜索過(guò)程將被終止并給出反例。檢測(cè)結(jié)果所得的數(shù)據(jù)信息對(duì)系統(tǒng)設(shè)計(jì)者排錯(cuò)有極大幫助。目前模型檢測(cè)技術(shù)以其簡(jiǎn)潔明了、自動(dòng)化程度高以及實(shí)用性強(qiáng)等特性已經(jīng)在計(jì)算機(jī)芯片設(shè)計(jì)、軟件可靠性、通信可靠性、通信協(xié)議、控制系統(tǒng)等領(lǐng)域得到廣泛應(yīng)用?；驹砣鐖D1所示。

圖1 模型檢測(cè)基本原理圖

對(duì)于表示系統(tǒng)性質(zhì)某種時(shí)態(tài)邏輯公式或者一類有窮狀態(tài)并發(fā)系統(tǒng)，模型檢測(cè)技術(shù)的關(guān)鍵在于是否能找到算法判定系統(tǒng)類中的任一給定系統(tǒng)是否滿足公式類中任意給定的一個(gè)時(shí)態(tài)邏輯公式。如圖1所示，其算法的輸入分別是待驗(yàn)證系統(tǒng)模型M和系統(tǒng)屬性φ，若模型M滿足性質(zhì)φ，則給出true結(jié)果，否則給出false以及反例詳細(xì)說(shuō)明。

模型驗(yàn)證工具SPIN是一個(gè)對(duì)并發(fā)系統(tǒng)進(jìn)行形式化驗(yàn)證的模型檢測(cè)工具。它支持promela規(guī)約語(yǔ)言并用于驗(yàn)證并發(fā)系統(tǒng)進(jìn)程的正確性。SPIN在仿真模式下可很好地捕捉模型中變量的變化過(guò)程，也能方便地可視化仿真過(guò)程。對(duì)與違法模型性質(zhì)的反例，在驗(yàn)證模式下會(huì)有詳細(xì)數(shù)據(jù)說(shuō)明，在仿真模式下會(huì)給出錯(cuò)誤軌跡圖。2002年，Holzmann(SPIN的設(shè)計(jì)者)得到了ACM頒發(fā)的軟件系統(tǒng)開發(fā)獎(jiǎng)。仿真與驗(yàn)證結(jié)構(gòu)流程見圖2。

圖2 SPIN仿真與驗(yàn)證結(jié)構(gòu)流程

2 Nayak協(xié)議

該協(xié)議的主要思想是用戶需要注冊(cè)初始化，然后用戶通過(guò)雙向認(rèn)證進(jìn)行授權(quán)訪問(wèn)，并且在雙向認(rèn)證過(guò)程中通過(guò)確認(rèn)隨機(jī)數(shù)來(lái)實(shí)現(xiàn)認(rèn)證。注冊(cè)階段抽象協(xié)議流程如圖3所示。

(1) 當(dāng)用戶需要訪問(wèn)云資源時(shí)，需要一個(gè)有效的郵箱賬號(hào)(Email_id)。 用戶選擇一個(gè)合法的用戶賬號(hào)(User_id)，服務(wù)器檢驗(yàn)該賬號(hào)是否有效。

(2) 用戶輸入有效的郵箱賬號(hào)，服務(wù)器通過(guò)該賬號(hào)發(fā)送動(dòng)態(tài)口令(Token)給用戶，用戶輸入動(dòng)態(tài)口令。

(3) 服務(wù)器檢測(cè)動(dòng)態(tài)口令以及密碼(Pwd),如有效則成功。

(4) 通過(guò)單向哈希函數(shù)生成的B發(fā)送給用戶。

圖3 注冊(cè)抽象協(xié)議流程

登錄與驗(yàn)證抽象協(xié)議流程如圖4所示。

(1) 用戶生成一個(gè)隨機(jī)數(shù)Nc，然后通過(guò)AES(Advanced Encryption Standard)加密技術(shù)生成密鑰K得到消息(M_client)，將其發(fā)送給服務(wù)器。

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

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

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

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

圖4 登錄與驗(yàn)證抽象協(xié)議流程

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

(1) client→server:{Nc}Kcs

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

(3) client→server:{Ns}K_cs

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

3 Nayak協(xié)議建模

本文要驗(yàn)證的協(xié)議共有兩個(gè)合法主體和一個(gè)非法主體，分別是Client、Server和Intruder。為了方便，簡(jiǎn)寫成C、S、I。

3.1 四通道并行建模

攻擊者模型遵循Dolev-Yao模型,Dolev-Yao規(guī)定攻擊者可以竊取合法主體發(fā)送的所有消息，并能對(duì)所竊取的消息進(jìn)行刪除、轉(zhuǎn)發(fā)、篡改等。然而，在模型檢測(cè)中，對(duì)攻擊者能力的描述可能會(huì)出現(xiàn)大量重復(fù)子消息項(xiàng)以及忽略多輪協(xié)議并行的情況，造成進(jìn)程間交叉運(yùn)行所產(chǎn)生的狀態(tài)遷移量增大，甚至可能發(fā)生狀態(tài)爆炸[11-12]問(wèn)題。本文以四通道并行建模方式來(lái)描述攻擊者能力。

模型定義了四個(gè)通道：發(fā)起者與攻擊者兩個(gè)通道；響應(yīng)者與攻擊者兩個(gè)通道。

兩個(gè)合法主體之間是沒(méi)有通道相連的，因?yàn)閮蓚€(gè)合法主體在進(jìn)行消息交換時(shí)，攻擊者總是能竊聽或竊取到合法主體發(fā)送的所有消息，合法主體所接收的消息總是攻擊者發(fā)送的。并行建模是指合法主體C、S既扮演了發(fā)起者，也扮演了響應(yīng)者，例如C在發(fā)送消息的同時(shí)，可能會(huì)收到S發(fā)送的消息。示意圖如圖5所示。

圖5 四通道并行建模

3.2 誠(chéng)實(shí)主體建模

首先對(duì)協(xié)議數(shù)據(jù)項(xiàng)名稱進(jìn)行簡(jiǎn)化命名，主體名：C、S、I，挑戰(zhàn)數(shù)：Nc(C作為發(fā)起者所用的隨機(jī)數(shù))、N_c(C作為響應(yīng)者所用的隨機(jī)數(shù))、Ns(S作為響應(yīng)者所用的隨機(jī)數(shù))、N_s(S作為發(fā)起者所用的隨機(jī)數(shù))，共享密鑰：CS、C_S(新共享密鑰)。

Nayak協(xié)議的誠(chéng)實(shí)主體為Client發(fā)起者與Server響應(yīng)者，proctype PC()、proctype PS()為其對(duì)應(yīng)的進(jìn)程。四個(gè)通道分別是發(fā)起者PC的消息通道為ch1與ch2，響應(yīng)者PS的消息通道為ch3與ch4。

由于協(xié)議中傳輸?shù)南?shù)不同，發(fā)起者PC的通道定義如下：

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

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

同理，響應(yīng)者PS的通道定義如下：

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

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

其中[0]表示通道中傳遞數(shù)據(jù)和接收數(shù)據(jù)同步。

對(duì)本文所用的消息類型做枚舉說(shuō)明：

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

這里符號(hào)表示：R為不可識(shí)別的主體，x代表任意誠(chéng)實(shí)主體，gD為泛型數(shù)據(jù)量符號(hào)化。

對(duì)Client的描述，具體實(shí)現(xiàn)代碼如下：

{

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發(fā)起者進(jìn)程中，self與party分別表示消息發(fā)起者與接收者，g1、g2表示泛型變量，發(fā)起者一共完成了兩次發(fā)送操作和一次接收操作。其中發(fā)送消息語(yǔ)句ch1？self,nonce,CS的含義是：self(發(fā)送者C)發(fā)送自己的隨機(jī)數(shù)，用C與S的共享密鑰加密。atomic表示promela語(yǔ)言定義的原子序列語(yǔ)法規(guī)則，運(yùn)用該語(yǔ)法規(guī)則可使進(jìn)程交叉運(yùn)行次數(shù)減少，把接收操作與下一次發(fā)送操作放在一個(gè)atomic中同時(shí)完成，能有效地減少狀態(tài)空間。原子謂詞表示協(xié)議的性質(zhì)，原子謂詞變量的值由模型的宏定義來(lái)更新記錄，IniRunning、IniCommit和ResRunning、ResCommit為模型程序中定義的四個(gè)宏，其中IniRunning表示發(fā)起者與響應(yīng)者會(huì)話，IniCommit表示發(fā)起者提交了與響應(yīng)者的會(huì)話，宏定義如下：

#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 運(yùn)用LTL公式刻畫Nayak協(xié)議安全性質(zhì)

LTL線性時(shí)態(tài)邏輯[13-14]被運(yùn)用于描述協(xié)議所需要滿足的屬性，通過(guò)判斷所建立的模型是否滿足所描述的屬性公式來(lái)驗(yàn)證協(xié)議的安全性。

模型的每一條性質(zhì)都需要用一個(gè)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發(fā)起與server的會(huì)話，初始值為0表示client沒(méi)有發(fā)起與server的會(huì)話，IniCommitCS表示client提交與server的會(huì)話，初始值為0表示client沒(méi)有提交與server的會(huì)話，其他與之類似。

根據(jù)3.2節(jié)給出的所有屬性描述函數(shù)的定義與屬性變量的初始化，用戶與服務(wù)器間的身份認(rèn)證屬性具體描述如下：

C必須在S發(fā)起會(huì)話后才能提交與S的對(duì)話或者S從來(lái)沒(méi)有發(fā)起與C的會(huì)話，LTL(線性時(shí)態(tài)邏輯)刻畫如下：

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

ResRunningCS)))

S必須在C發(fā)起會(huì)話后才能提交與C的對(duì)話或者C從來(lái)沒(méi)有發(fā)起與S的會(huì)話，LTL(線性時(shí)態(tài)邏輯)刻畫如下：

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

ResRunningSC)))

將這兩個(gè)LTL公式運(yùn)用邏輯符連接后得到完整LTL屬性描述：

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

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

(!IniCommitSC U ResRunningSC)))

3.4 攻擊者建模

攻擊者建模通常是模型檢測(cè)中最重要的一部分，攻擊者能力的強(qiáng)弱也會(huì)直接影響模型檢測(cè)的效果以及效率。根據(jù)Dolev-Yao模型構(gòu)建攻擊者知識(shí)庫(kù)函數(shù)，把攻擊者獲取的知識(shí)提取出來(lái)，建立單獨(dú)的知識(shí)庫(kù)存儲(chǔ)攻擊者知識(shí)，攻擊者根據(jù)這些知識(shí)偽造、轉(zhuǎn)發(fā)消息。構(gòu)建攻擊者知識(shí)庫(kù)函數(shù)需要找到攻擊者需要表示的知識(shí)，而攻擊者可以學(xué)會(huì)的知識(shí)集合A與攻擊者需要學(xué)會(huì)的知識(shí)集合B的交集即攻擊者需要表示的知識(shí)，具體如下：

攻擊者可以學(xué)會(huì)的知識(shí)：由誠(chéng)實(shí)主體的發(fā)生語(yǔ)句所得。

ch1!self,nonce, CS;

ch1! self,g1,C_S;

ch4!self,g1, nonce, CS;

利用靜態(tài)分析法縮減隨機(jī)變量的取值范圍，降低搜索狀態(tài)數(shù)，例如client將隨機(jī)變量g1用新共享密鑰C_S加密發(fā)送給server，對(duì)于client來(lái)說(shuō)，它不確定g1是不是server的隨機(jī)數(shù)，因此變量g1取值范圍為{Nc,N_c,Ns,N_s}，nonce的取值范圍為{Nc，N_s},響應(yīng)者進(jìn)程中變量g1取值范圍為{Nc,N_c,Ns,N_s},具體如表1。

表1 攻擊者可以學(xué)會(huì)的知識(shí)

攻擊者需要學(xué)會(huì)的知識(shí):由誠(chéng)實(shí)主體的接收語(yǔ)句所得。

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

ch3 ?g2,g1, eval(CS);

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

利用靜態(tài)分析法分析得出，發(fā)起者進(jìn)程中nonce取值范圍為{Nc,N_s}，變量g1取值范圍為{Nc,N_c,Ns,N_s}，響應(yīng)者進(jìn)程中變量g1取值范圍為{Nc_,Ns}，具體如表2。

表2 攻擊者需要學(xué)會(huì)的知識(shí)

表1與表2的交集即攻擊者需要表示的知識(shí)項(xiàng):

{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

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

proctype PI() {

bit k_Nc_CS=0;

…

bit k_N_s_N_c_CS=0;

/*需要表示的知識(shí)初始化*/

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 實(shí)驗(yàn)結(jié)果與分析

使用SPIN驗(yàn)證工具對(duì)上述模型進(jìn)行驗(yàn)證，發(fā)生了屬性違反，自動(dòng)生成了并行攻擊路徑，攻擊序列圖如圖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

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

如圖7所示，ResCommitCS,ResRunningCS，IniCommitSC,IniRunningSC為0，IniCommitCS，IniRunningCS,ResCommitSC,ResRunningSC為1，表示在整個(gè)協(xié)議運(yùn)行中，發(fā)起者(響應(yīng)者)C開始并提交與響應(yīng)者(發(fā)起者)S的會(huì)話，但響應(yīng)者(發(fā)起者)S沒(méi)有參與或提交一次會(huì)話。

圖7 性質(zhì)違反信息

圖8描述單個(gè)全局系統(tǒng)狀態(tài)需要64字節(jié)的內(nèi)存，檢測(cè)后狀態(tài)樹的高度達(dá)到27層，并且檢測(cè)到1項(xiàng)錯(cuò)誤。transitions和states-stored的數(shù)量越少表示狀態(tài)遷移量越少，系統(tǒng)存儲(chǔ)的狀態(tài)量越少，驗(yàn)證效率越高，且不易引起狀態(tài)爆炸。state-vector和depth-reached屬性表示狀態(tài)矢量數(shù)和深度優(yōu)先搜索的深度，數(shù)量越少表明模型越優(yōu)秀，檢測(cè)效率越高。并且，從圖8可知，本文構(gòu)建的模型并未出現(xiàn)狀態(tài)爆炸等情況。

圖8 模型驗(yàn)證結(jié)果信息

5 結(jié) 語(yǔ)

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

[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] 詹麗.云計(jì)算中基于Smartcard的雙向認(rèn)證安全協(xié)議的研究與形式化分析[D].廣州:暨南大學(xué),2014.

[8] 馬成林,肖美華,鄧春艷,等.基于改進(jìn)GNY邏輯的Kerberos*協(xié)議安全性分析[J].計(jì)算機(jī)與數(shù)字工程,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] 侯剛,周寬久,勇嘉偉,等.模型檢測(cè)中狀態(tài)爆炸問(wèn)題研究綜述[J].計(jì)算機(jī)科學(xué),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。國(guó)家自然科學(xué)基金項(xiàng)目(61163005，61562026)；計(jì)算機(jī)軟件新技術(shù)國(guó)家重點(diǎn)實(shí)驗(yàn)室開放課題項(xiàng)目(KFKT2012B18)；江西省自然科學(xué)基金項(xiàng)目(2013BAB201033)；江西省高?？萍悸涞赜?jì)劃項(xiàng)目(KJLD13038)；江西省對(duì)外科技合作技術(shù)項(xiàng)目(20151BDH80005)；華東交通大學(xué)研究生創(chuàng)新計(jì)劃項(xiàng)目(YC2014-X007)。肖美華，教授，主研領(lǐng)域：信息安全，軟件形式化方法。梅映天，碩士生。李偉，碩士生。