NSSK協(xié)議的SPIN模型檢測

黃鵬

摘要：安全協(xié)議是以密碼學(xué)為基礎(chǔ)的消息交換協(xié)議。針對傳統(tǒng)的改進NSSK安全協(xié)議，通過使用Promela語言對協(xié)議進行建模，并使用SPIN模型檢測工具進行驗證，發(fā)現(xiàn)仍然存在安全漏洞，攻擊者可以冒充合法者進行通信。針對上述缺陷，提出了一種有效的改進方案，主要是在協(xié)議中增加了自身產(chǎn)生的隨機數(shù)和發(fā)送者的身份標(biāo)識，該改進方案提高了協(xié)議安全性。

關(guān)鍵詞：安全協(xié)議； 安全漏洞；NSSK；SPIN；模型檢測

DOIDOI：10.11907/rjdk.171239

中圖分類號：TP309文獻標(biāo)識碼：A文章編號：16727800（2017）010018504

0引言

如今，隨著信息逐漸成為重要的戰(zhàn)略資源，信息化水平已成為衡量一個國家現(xiàn)代化水平和綜合國力的重要標(biāo)志。同時，信息安全問題也成為人們重點關(guān)注的一個問題。安全協(xié)議是以密碼學(xué)為基礎(chǔ)的消息交換協(xié)議，其目的是在網(wǎng)絡(luò)環(huán)境下提供各種安全服務(wù)。安全協(xié)議可以分為密鑰交換協(xié)議、認證協(xié)議、電子商務(wù)協(xié)議、安全多方計算協(xié)議等多種類型。簡單安全協(xié)議雖然只是簡單消息的傳遞，但消息之間存在微妙、復(fù)雜的關(guān)系。NSSK協(xié)議[12]是一個經(jīng)典的認證密碼協(xié)議，不少學(xué)者在NSSK協(xié)議研究中提出了一些NSSK認證方案，但這些方案也不是完全安全的，仍然存在風(fēng)險。2014年Hu等主要根據(jù)GSMR系統(tǒng)現(xiàn)有的安全威脅和必須采取的安全措施，采用一種改進的NSSK安全協(xié)議來保障車載設(shè)備與RBC之間的安全通信。通過分析發(fā)現(xiàn)，其存在著一些安全缺陷，因此提出了改進方案。

本文使用SPIN模型檢測工具對NSSK協(xié)議的改進方案進行驗證和分析，發(fā)現(xiàn)存在著攻擊。因此，針對該攻擊提出一種改進方案，以提高協(xié)議安全性。

1模型檢測及工具SPIN

系統(tǒng)的設(shè)計和驗證需要SPIN模型檢測器的支持，首先形式化描述整個系統(tǒng)模型，對模型進行分析，發(fā)現(xiàn)語法錯誤，如果沒有發(fā)現(xiàn)語法錯誤，則需要對系統(tǒng)進行交互模擬運行，直到系統(tǒng)設(shè)計達到預(yù)期為止。然后，SPIN會生成一個優(yōu)化的onthefly驗證程序，該程序?qū)⒈痪幾g后執(zhí)行，如果在執(zhí)行過程中發(fā)現(xiàn)了任何違背正確性的反例，則會返回交互模擬執(zhí)行狀態(tài)，繼續(xù)進行檢測診斷，以確定產(chǎn)生反例的原因。因此，它的建模方法是：定義進程模板，將每個進程模板的行為視為一種行為規(guī)范，實際系統(tǒng)可以被看作一個或多個異步進程模板實例的組合。SPIN是一種基于計算機科學(xué)的形式化方法，它將先進的理論驗證方法應(yīng)用于大型軟件系統(tǒng)的驗證中，目前在工業(yè)界和學(xué)術(shù)界得到了廣泛應(yīng)用。

SPIN的基本結(jié)構(gòu)如圖1所示，其描述了整個檢測過程。

2協(xié)議介紹

2.1NSSK協(xié)議原理及存在的問題

NSSK協(xié)議是一個經(jīng)典的認證密碼協(xié)議。協(xié)議先通過對兩個主體的身份進行認證，通信主體需要經(jīng)過5個階段的通信過程，才能獲得安全通信過程的會話密鑰。

協(xié)議符號說明：A表示用戶A的身份標(biāo)識；B表示用戶B的身份標(biāo)識；S表示服務(wù)器；Nb表示用戶B產(chǎn)生的隨機數(shù)；Na表示用戶A產(chǎn)生的隨機數(shù)；Kbs表示用戶B與S之間的共享密鑰；Kas表示用戶A與S之間的共享密鑰；Kab表示用戶A和用戶B的會話密鑰。

協(xié)議的步驟如下：

（1）A→S：A，B，Na

（2）S→A：{Na，B，Kab，{Kab，A}Kbs}Kas

（3）A→B：{Kab，A}Kbs

（4）B→A：{Nb}Kab

（5）A→B：{Nb-1}Kab

在此協(xié)議中，用戶A和用戶B進行秘密通信，用戶A會向服務(wù)器S請求分配一個會話密鑰來保證通信內(nèi)容的秘密性。協(xié)議前3個消息主要是服務(wù)器分配會話密鑰給合法用戶，后兩個消息主要是合法用戶之間的相互驗證。

具體過程為：①協(xié)議開始時，合法用戶A將用戶A的身份標(biāo)識、用戶B的身份標(biāo)識以及用戶A產(chǎn)生的隨機數(shù)Na組成消息1，發(fā)送給服務(wù)器S，告訴服務(wù)器它將與用戶B進行通信；②服務(wù)器S在接收到消息1時，隨機產(chǎn)生一個Kab，這是為雙方分配的會話密鑰，同時將A的身份標(biāo)識和Kab用B的密鑰Kbs加密生成一個證書，然后將證書、用戶A在消息1發(fā)送的Na、用戶B的身份標(biāo)識和會話密鑰Kab用A的密鑰Kas加密組成消息2發(fā)送給A；③用戶A接收到消息2時，用密鑰Kas解密消息得到會話密鑰Kab和證書{Kab，A}Kbs，然后再將證書組成消息3發(fā)送給用戶B；④用戶B接收到消息3時，用密鑰Kbs解密得到會話密鑰Kab，再用Kab加密自身產(chǎn)生的隨機數(shù)Nb組成消息4，發(fā)送給用戶A；⑤用戶A接收到消息4后，用會話密鑰Kab解密得到Nb，再將Nb與1進行運算后，將得到的結(jié)果用Kab進行加密組成消息5發(fā)送給用戶B。這里的Nb-1可以用Nb來代替，只是用來區(qū)別消息4，而消息4和消息5是為了防止中間人攻擊。

在此協(xié)議中，在消息4中用戶A是通過Nb來確認用戶B的身份，在消息5中用戶B是通過Nb-1來確認用戶A的身份。這里的Kab表示用戶A和用戶B之間的會話密鑰，只有用戶A和用戶B可以對其解密。

該協(xié)議比較簡單，實現(xiàn)起來也較為容易，但在文獻[8]中，Denning和Sacco在1981年發(fā)現(xiàn)了一個攻擊，發(fā)現(xiàn)此協(xié)議不能抵抗“新鮮性”攻擊，如果一個攻擊者擁有過期的會話密鑰，能夠冒充用戶A，通過重放消息3，來實施以下攻擊：

（1）A→S：A，B，Na

（2）S→A：{Na，B，Kab，{Kab，A}Kbs}Kas

（3）I（A）→B：{ K′ab，A}Kbs

（4）B→I（A）：{N′b}K′ab

（5）I（A）→B：{N′b-1}K′ab

其中，I（X）表示攻擊者可以冒充合法用戶X接收和發(fā)送消息。通過上面的攻擊過程，使合法用戶B相信自己得到的會話密鑰K′ab是執(zhí)行當(dāng)前協(xié)議回合的結(jié)果。因此，該攻擊是有效的。endprint

在2001年，王貴林、卿斯?jié)h等在文獻[12]又提出攻擊者可以冒充合法用戶B實施以下攻擊：

（1）A→S：A，B，Na

（2）S→A：{Na，B，Kab，{Kab，A}Kbs}Kas

（3）A→I（B）：{Kab，A}Kbs

（4）I（B）→A：NI

（5）A→I（B）：{{NI}K-1ab-1}Kab

其中，NI和{Nb}Kab格式相同，攻擊者冒充用戶B發(fā)送消息給用戶A，用戶A收到消息4，然后對其進行所謂的解密，并將得到的結(jié)果與1進行運算后，將運算后的結(jié)果用Kab加密發(fā)給用戶B。用戶A以為用戶B知道了會話密鑰，但實際上，B根本沒有參加整個協(xié)議的執(zhí)行過程，甚至可能還是離線的。因此，該攻擊是有效的。

2.2協(xié)議改進方案

文獻[7]分析了NSSK協(xié)議后，提出一種改進方案，該方案采用的符號與原協(xié)議相同，而且消息形式與原協(xié)議相似，修改后的完整協(xié)議簡單描述如下：

（1）A→S：A，B，Na。用戶A通過發(fā)送消息1給服務(wù)器S，它將與用戶B進行通信，主要將用戶A的身份標(biāo)識、用戶B的身份標(biāo)識和用戶A產(chǎn)生的隨機數(shù)Na組成消息1提供給服務(wù)器S。

（2）S→B：A。當(dāng)服務(wù)器S接收到消息1后，隨即發(fā)送A的用戶標(biāo)識給用戶B。S通過發(fā)送消息告訴用戶B，用戶A要與其進行通信。

（3）B→S：{ Nb} Kbs。當(dāng)用戶B接收到消息2后，知道用戶A將與它通信，然后將自身產(chǎn)生的隨機數(shù)Nb用密鑰Kbs進行加密組成消息3，將其發(fā)送給服務(wù)器S。

（4）S→A：{ Na ，B，Kab} Kas。當(dāng)服務(wù)器S收到消息3后，將用戶A產(chǎn)生的隨機數(shù)Na、用戶B的身份標(biāo)識、用戶A與用戶B之間的密鑰Kab用A的密鑰Kas進行加密，組成消息4發(fā)送給用戶A，告訴用戶A，用戶B已經(jīng)準(zhǔn)備好與之通信。

（5）S→B：{ Nb ，A，Kab} Kbs。服務(wù)器S收到消息3后，解密消息3得到Nb，然后再將用戶B的隨機數(shù)Nb、用戶A的身份標(biāo)識、用戶A與用戶B之間的密鑰Kab用B的密鑰Kbs進行加密，組成消息5發(fā)送給用戶B，通知用戶B，用戶A已經(jīng)準(zhǔn)備好與之通信。

（6）B→A：{N′b}Kab。當(dāng)用戶B接收到消息5后，將自己產(chǎn)生的隨機數(shù)N′b用會話密鑰Kab加密組成消息6，再發(fā)送給用戶A。

（7）A→B：{N′b-1}Kab。當(dāng)用戶A接收到消息6后，用會話密鑰Kab解密消息6，得到N′b，然后將N′b與1計算后得到N′b-1，用會話密鑰Kab加密N′b-1組成消息7，再發(fā)送給用戶B。

此改進協(xié)議也是用戶A通過N′b來確認用戶B的身份。同樣，用戶B通過N′b-1來確認用戶A的身份。

3改進協(xié)議Promela建模及分析

3.1攻擊者建模

攻擊者[11]可以根據(jù)自身的知識能力對網(wǎng)絡(luò)和信息采取敵意的行為，其可以具備如下知識能力：①在合法主體通信過程中，對其進行截獲或者轉(zhuǎn)發(fā)任何消息；②可以冒充合法用戶或服務(wù)器參與協(xié)議運行；③可以對協(xié)議里的任何消息進行解密和加密；④可以對協(xié)議里的任何消息進行重構(gòu)，通過重構(gòu)消息來試圖欺騙用戶和服務(wù)器。

3.2協(xié)議系統(tǒng)屬性

NSSK協(xié)議及其改進方案都是在秘密狀態(tài)下，用戶與用戶之間身份的相互鑒別，同時協(xié)商了會話密鑰，所以該協(xié)議必須滿足認證性和秘密性。認證性的含義為：A與B如果成功運行了一次協(xié)議，那么用戶A要相信通信對方就是用戶B，同時用戶B相信通信對方就是用戶A，即通信雙方的真實身份要相互鑒別。用LTL公式表示如下：

[]（（statusA==ok&&partnerA==responserID）？（statusB=ok&&partnerB==askerID））

其中&&表示邏輯與，←→表示邏輯等價，[]表示always。

秘密性的含義為：要確保需要加密的協(xié)議消息內(nèi)容在傳送過程中不被攻擊者非法竊取。根據(jù)協(xié)議特點，從消息3到消息7都有密鑰進行加密，攻擊者無法獲得其隨機數(shù)N′b，也無法冒充用戶或服務(wù)器進行攻擊。因此，只要成功運行了一次協(xié)議，LTL公式則能保證其秘密性。

3.3驗證結(jié)果分析

通過模型檢測工具Xspin檢測改進后的協(xié)議可發(fā)現(xiàn)漏洞，并得到入侵者的攻擊路徑。入侵者利用獲得的消息，重構(gòu)消息冒充B與A通信，最終使A誤認為它與B通信，其實是I與之進行通信，成功地對其進行了攻擊。

其中askerID代表A的身份標(biāo)識，responserID代表B的身份標(biāo)識，nonceA、nonceI分別代表A、I產(chǎn)生的隨機數(shù)，nonceB1和nonceB2分別代表B在協(xié)議消息1和消息6產(chǎn)生的隨機數(shù)，keyAB代表A與B之間的會話密鑰，keyBS代表B的密鑰，keyAS代表A的密鑰，key代表I產(chǎn)生的密鑰，temp代表空值。為了簡化建模過程，最后一步驗證消息沒有減1。攻擊路徑如圖2所示。

圖2協(xié)議改進受攻擊軌跡

由圖2得知入侵者攻擊時序如下：

（1）A→S：A，B，Na

（2）S→B：A

（3）B→S：{ Nb} Kbs

（4）S→A：{ Na，B，Kab} Kas

（5）S→I（B）：{ Nb，A，Kab} Kbs

（6）I（B）→A：NI

（7）A→I（B）：{{NI}K-1ab-1}Kab

攻擊過程描述如下：攻擊過程的前4個消息都是A、S、B接收消息或轉(zhuǎn)發(fā)消息，攻擊過程主要是在后面3個消息中：先是入侵者I冒充用戶B發(fā)送NI給A，其中NI與{N′b}Kab格式相同，A接收到消息6后對其進行所謂的解密，得到結(jié)果后，將結(jié)果與1運算后用Kab加密后組成消息7發(fā)送給B，I將其截獲。endprint

通過上述分析，在文獻[7]的改進協(xié)議中，前5個消息是分配會話密鑰，在消息4和消息5分別加上了隨機數(shù)，從而可以抵抗文獻[8]提出的新鮮性攻擊。但發(fā)現(xiàn)的攻擊與王貴林、卿斯?jié)h等在文獻[12]發(fā)現(xiàn)的攻擊類似，B在消息4之后就沒有收到消息，一直在等待消息，但A不知B在等待消息，以為它還在與B進行通信，其實I在與A進行通信，攻擊有效，所以說其無法抵抗該攻擊。

3.4NSSK協(xié)議改進

NSSK協(xié)議受攻擊的原因是，文獻[7]改進的協(xié)議消息6太過簡單，容易被重構(gòu)騙過合法的參與者。

針對上述攻擊，對協(xié)議的改進如下：

（1）A→S：A，B，Na

（2）S→B：A

（3）B→S：{ Nb} Kbs

（4）S→A：{ Na ，Nb，B，Kab} Kas

（5）S→B：{ Na，Nb，A，Kab} Kbs

（6）B→A：{Nb，Na，B}Kab

（7）A→B：{Nb-1，Nb，A}Kab

對其改進的協(xié)議進行建模，改進的協(xié)議和文獻[7]改進協(xié)議格式相同，只是傳遞的消息內(nèi)容有所差別，建模過程和上文的建模過程相似，用模型檢測工具Xspin對上述改進后的協(xié)議進行驗證，驗證結(jié)果如圖3所示。

圖3對改進NSSK協(xié)議的驗證結(jié)果

通過驗證結(jié)果發(fā)現(xiàn)，結(jié)果顯示錯誤為0，則新改進的協(xié)議沒有發(fā)現(xiàn)漏洞，說明新改進的協(xié)議是安全的。

3.5改進方案安全性分析

定理1改進方案能加強雙向認證。

證明在協(xié)議的后兩條消息中分別加上了自己之前產(chǎn)生的隨機數(shù)，在消息6中，當(dāng)合法用戶A解密消息得到自己的隨機數(shù)和B的身份標(biāo)識，才會相信是用戶B發(fā)來的消息，在消息7中原理相同。因此，該協(xié)議能夠加強雙向認證。

定理2改進方案能抵抗中間人攻擊。

證明對于文獻[7]的改進協(xié)議，主要是消息6容易被攻擊者篡改，偽裝攻擊欺騙合法用戶，所以在消息6和消息7中分別增加前面產(chǎn)生的隨機數(shù)和身份標(biāo)識，如果解密消息不是自己產(chǎn)生的隨機數(shù)和身份標(biāo)識，用戶會拒絕該消息，攻擊者則無法重構(gòu)信息來欺騙合法用戶。因此，改進方案能抵抗中間人攻擊。

定理3改進方案能夠抵抗重放攻擊。

證明對于文獻[7]的改進協(xié)議，攻擊者截取到消息6后，會重放該消息來騙過合法用戶，所以在消息6加上合法用戶前面產(chǎn)生的隨機數(shù)和身份標(biāo)識，如果解密消息得不到期望的消息，用戶會拒絕該消息，使攻擊者無法通過重放消息6來欺騙合法用戶。因此，改進方案能抵抗重放攻擊。

4結(jié)語

本文使用Promela語言對NSSK協(xié)議[7]的改進方案進行建模，根據(jù)協(xié)議必須滿足的安全性質(zhì)描述（LTL公式、斷言）進行驗證，用模型檢測工具Xspin進行檢測，成功地找出了反例。通過分析攻擊序列產(chǎn)生的原因，給出了一種修改方案。通過驗證和分析發(fā)現(xiàn)，改進后的協(xié)議可以滿足安全協(xié)議要求。SPIN模型檢測技術(shù)是分析安全協(xié)議的有效工具，下一步工作可以使用SPIN工具檢測和改進其它安全協(xié)議。

參考文獻參考文獻：

[1]LIAO J， ZHU B， YONG H. Security analysis of NSSK protocol and its improvement[C].Eighth IEEE International Conference on Dependable， Autonomic and Secure Computing， Dasc 2009， Chengdu， China， DBLP， 2009：115118.

[2]CHEN L， WANG W. An improved NSSK protocol and its security analysis based on logic approach[C]. International Conference on Communications， Circuits and Systems. IEEE， 2008：772775.

[3]TINGYUAN L， XIAODONG L， ZHIGUANG Q， et al. An improved security protocol formal analysis with BAN logic[C].International Conference on Electronic Commerce and Business Intelligence. IEEE Xplore， 2009：102105.

[4]WANG X， YUAN C W. Formal analysis method of security protocol[J]. Computer Engineering， 2010， 36（7）：8284.

[5]CHEN H，CLARK J A，JOCOB J L.A searchbased approach to the automated design of security protocols，YCS 376[R].New York：University of York，Department of Computer Science，2004.

[6]LERDA F， SISTO R. Distributedmemory model checking with SPIN[C]. SpringerVerlag， 1999：2239.

[7]胡曉輝，陳慧麗，石廣田，等.CTCT4級安全通信協(xié)議的形式化建模與驗證[J]. 計算機工程與應(yīng)用， 2014，50（4）：8185.

[8]DENNING D E， SACCO G M. Timestamps in key distribution protocols[J]. Communications of the Acm， 1981，24（8）：533536.

[9]王巧麗.SPIN模型檢測的研究與應(yīng)用[D].貴陽：貴州大學(xué)，2006.

[10]楊霓霏，劉曉斌，盧佩玲，等.CTCS3級列控系統(tǒng)車地?zé)o線通信消息認證和加密技術(shù)的研究[J].鐵道通信信號，2010，46 （10）：15.

[11]尤啟房，楊晉吉.SIP協(xié)議的SPIN模型檢測[J].計算機工程與應(yīng)用，2014，50（13）：8789.

[12]王貴林，卿斯?jié)h，周展飛.認證協(xié)議的一些新攻擊方法[J].軟件學(xué)報，2001，12（6）：907913.

[13]萬子龍.基于模型檢測的SET協(xié)議形式化驗證與改進[D].南昌：南昌大學(xué)，2014.

[14]李翠翠.基于SPIN模型檢測的電子商務(wù)協(xié)議分析與驗證[D].上海：華東理工大學(xué)，2012.

責(zé)任編輯（責(zé)任編輯：黃?。〆ndprint