肖美華 梅映天 李 偉

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

運用SPIN對云環(huán)境雙向認證協(xié)議Nayak的安全性驗證

肖美華 梅映天 李 偉

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

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

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

0 引 言

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

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

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

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

1 模型檢測技術(shù)

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

圖1 模型檢測基本原理圖

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

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

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

2 Nayak協(xié)議

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

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

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

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

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

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

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

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

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

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

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

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

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

本文將對登錄與驗證階段進行研究與分析，由于協(xié)議使用對稱密鑰加密解密，我們可將步驟(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é)議建模

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

3.1 四通道并行建模

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

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

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

圖5 四通道并行建模

3.2 誠實主體建模

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

Nayak協(xié)議的誠實主體為Client發(fā)起者與Server響應(yīng)者，proctype PC()、proctype PS()為其對應(yīng)的進程。四個通道分別是發(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ù)同步。

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

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

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

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

#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協(xié)議安全性質(zhì)

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

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

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

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

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

ResRunningCS)))

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

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

ResRunningSC)))

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

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

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

(!IniCommitSC U ResRunningSC)))

3.4 攻擊者建模

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

攻擊者可以學(xué)會的知識：由誠實主體的發(fā)生語句所得。

ch1!self,nonce, CS;

ch1! self,g1,C_S;

ch4!self,g1, nonce, CS;

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

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

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

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

ch3 ?g2,g1, eval(CS);

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

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

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

表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

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

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 實驗結(jié)果與分析

使用SPIN驗證工具對上述模型進行驗證，發(fā)生了屬性違反，自動生成了并行攻擊路徑，攻擊序列圖如圖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é)議開始運行時，發(fā)起者C將Nc(C作為發(fā)起者所用的隨機數(shù))以CS共享密鑰加密發(fā)送給攻擊者，這樣攻擊者I就掌握了相關(guān)信息，隨后發(fā)起者C又將N_c(C作為響應(yīng)者所用的隨機數(shù))以CS共享密鑰加密發(fā)送給攻擊者，攻擊者I冒充了響應(yīng)者S與發(fā)起者C進行了三次會話。然而，響應(yīng)者S與發(fā)起者C卻并不知情，這就表明該協(xié)議充滿危險性。

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

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

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

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

5 結(jié) 語

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

[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的雙向認證安全協(xié)議的研究與形式化分析[D].廣州:暨南大學(xué),2014.

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