鐘小妹，肖美華，李 偉，諶 佳，李婭楠

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

1 引言

物聯(lián)網(wǎng)的飛速發(fā)展掀起了繼計(jì)算機(jī)、互聯(lián)網(wǎng)后世界信息產(chǎn)業(yè)的第三次浪潮。無(wú)線射頻識(shí)別RFID(Radio Frequency IDentification)是實(shí)現(xiàn)物聯(lián)網(wǎng)的關(guān)鍵技術(shù)［1］。RFID是一種非接觸式的自動(dòng)識(shí)別技術(shù)，通過無(wú)線射頻信道實(shí)現(xiàn)電子標(biāo)簽(Tag)與終端讀寫器(Reader)之間的數(shù)據(jù)交換。由于Tag與Reader之間使用無(wú)線信道進(jìn)行通信，因此在實(shí)際應(yīng)用中標(biāo)簽極易遭受各種攻擊，例如對(duì)標(biāo)簽進(jìn)行惡意跟蹤、惡意偽裝、竊取、篡改數(shù)據(jù)等。當(dāng)前，安全認(rèn)證協(xié)議成為確保RFID系統(tǒng)安全的重要手段，RFID系統(tǒng)中認(rèn)證協(xié)議的安全性保障了RFID系統(tǒng)的通信安全。

在RFID系統(tǒng)中，根據(jù)認(rèn)證協(xié)議復(fù)雜性將協(xié)議劃分為輕量級(jí)安全協(xié)議與非輕量級(jí)安全協(xié)議［2，3］。非輕量級(jí)安全協(xié)議使用基于對(duì)稱加密和基于公鑰加密系統(tǒng)等運(yùn)算復(fù)雜度高的加密方式，可獲得較高安全性，但功耗大、硬件資源消耗高，有一定的應(yīng)用局限;輕量級(jí)安全協(xié)議多數(shù)采用基礎(chǔ)位運(yùn)算和邏輯函數(shù)等加密方式，在滿足安全性的同時(shí)，兼?zhèn)涔牡?、運(yùn)行效率高等特點(diǎn)，更易被廣泛運(yùn)用。

超輕量級(jí)雙向認(rèn)證協(xié)議UMAP(Ultra-lightweight Mutual Authentication Protocols)是輕量級(jí)安全協(xié)議中的一個(gè)重要分支［4］。UMAP在標(biāo)簽端使用簡(jiǎn)單逐位(bitwise)操作(比如 XOR、AND、OR、循環(huán)移位和模加等運(yùn)算)以加密通信數(shù)據(jù)。輕量級(jí)雙向認(rèn)證協(xié)議 LAMP(2006)［5］、SASI(2007)［6］和Gossamer(2009)［7］是UMAP家族的典型代表。盡管有很多UMAP被提出［8-11］，但是有一些協(xié)議很快被發(fā)現(xiàn)存在攻擊漏洞。

RCIA協(xié)議是由Mujahi等人［10］在2015年 International Journal of Distributed Sensor Networks中提出的超輕量級(jí)雙向認(rèn)證協(xié)議。該協(xié)議采用一種新的加密原語(yǔ):遞歸哈希(recursive hash)，聲稱遞歸哈希原語(yǔ)將給RCIA協(xié)議帶來(lái)高安全性。然而，2016年Safkhani等人［12］描述了在超輕量級(jí)相互認(rèn)證協(xié)議中存在去同步攻擊漏洞，并指出該漏洞同樣存在最近提出的RCIA協(xié)議中。2017年，Yasear等人［13］發(fā)現(xiàn)RCIA中存在惡意跟蹤攻擊，并且提出基于逐位操作的隨機(jī)數(shù)生成器(RNG)技術(shù)以克服該攻擊。

造成這些缺陷的主要原因是采用了弱安全分析模型，或者是采用了非形式化方法驗(yàn)證UMAP的安全性。形式化方法是提高軟件系統(tǒng)，特別是safety-critical系統(tǒng)的安全性與可靠性的重要手段，主要包括模型檢測(cè)與定理證明兩個(gè)分支。SPIN(Simple Promela INterpreter)［14］是一個(gè)著名的模型檢測(cè)工具，在2002年榮獲ACM頒發(fā)的“Soft System Award”獎(jiǎng)。

本文以RCIA作為研究對(duì)象，采用模型檢測(cè)方法分析驗(yàn)證該協(xié)議，在利用SPIN工具發(fā)現(xiàn)該協(xié)議存在漏洞后對(duì)其進(jìn)行改進(jìn)，改進(jìn)結(jié)果分析表明，改進(jìn)的RCIA協(xié)議具有更高的安全性。本文內(nèi)容組織如下:第2節(jié)描述RCIA協(xié)議，并對(duì)該協(xié)議進(jìn)行抽象建模及形式化表示;第3節(jié)闡述RCIA協(xié)議的Promela建模過程;第4節(jié)對(duì)RCIA協(xié)議進(jìn)行分析與驗(yàn)證;第5節(jié)描述由SPIN工具發(fā)現(xiàn)的去同步攻擊，對(duì)RCIA協(xié)議進(jìn)行改進(jìn)并進(jìn)行分析驗(yàn)證;第6節(jié)給出結(jié)論及未來(lái)的研究工作。

2 RCIA協(xié)議及協(xié)議抽象建模

2．1 RCIA 協(xié)議

RCIA協(xié)議使用三種基本操作:逐位運(yùn)算與操作(AND)、逐位運(yùn)算異或操作(XOR)和逐位循環(huán)左移操作(記為Rot());加密原語(yǔ)遞歸哈希函數(shù)(recursive hash)記為Rh()，底層操作由Rot()和XOR實(shí)現(xiàn)。

在RCIA協(xié)議中，標(biāo)簽與閱讀器共享ID，IDS(ID的索引假名)及兩個(gè)會(huì)話密鑰K1，K2，共同存儲(chǔ){IDSold，K1old，K2old，IDSnew，K1new，K2new} 以抵御去同步攻擊。RCIA協(xié)議交互如下:

閱讀器首先向標(biāo)簽發(fā)送Hello消息，標(biāo)簽收到后回復(fù)索引假名IDS消息給閱讀器。閱讀器運(yùn)用IDS在數(shù)據(jù)庫(kù)中搜索與當(dāng)前IDS匹配的密鑰信息{ID，K1，K2}。匹配成功后，閱讀器生成兩個(gè)隨機(jī)數(shù)n1，n2，計(jì)算消息A、B和C發(fā)送給標(biāo)簽。

標(biāo)簽端從閱讀器端收到A、B和C消息后，首先從消息A、B中解出閱讀器生成的兩個(gè)隨機(jī)數(shù)n1和n2;然后通過R=n1⊕n2;wt(R)mod b計(jì)算函數(shù)Rh()所需要的種子，其中，wt(R)表示R的漢明權(quán)重(Hamming Weight)，即二進(jìn)制位碼串中1的個(gè)數(shù);b表示將待加密的二進(jìn)制位碼串分塊個(gè)數(shù)。接著，標(biāo)簽端繼續(xù)計(jì)算K1*和K2*用來(lái)生成本地C*，與收到的C比對(duì)。若C*與C值相等，閱讀器被標(biāo)簽認(rèn)證，標(biāo)簽端將執(zhí)行兩個(gè)任務(wù):第一，生成并發(fā)送消息D給閱讀器;第二，執(zhí)行IDS和共享密鑰K1，K2的更新操作。

閱讀器收到消息D后，首先計(jì)算本地D*，若D*與接收的D匹配，閱讀器對(duì)標(biāo)簽進(jìn)行認(rèn)證，將執(zhí)行更新操作，即更新此標(biāo)簽在數(shù)據(jù)庫(kù)存儲(chǔ)的IDS、K1、K2數(shù)據(jù)。

2．2 協(xié)議抽象建模方法

針對(duì)超輕量級(jí)RFID雙向協(xié)議底層加密操作復(fù)雜，難以直接運(yùn)用形式化方法進(jìn)行分析的困境，本文提出一種協(xié)議抽象建模方法，便于抽象和簡(jiǎn)化研究對(duì)象。協(xié)議抽象建模方法基于以下原則:

(1)RFID系統(tǒng)的三個(gè)實(shí)體:標(biāo)簽(Tag)、閱讀器(Reader)和后臺(tái)系統(tǒng)(Back-end Sever)簡(jiǎn)化為兩個(gè)實(shí)體:Tag和Reader。閱讀器與后臺(tái)系統(tǒng)之間通常采用有線直接相連，能運(yùn)用經(jīng)典的加密系統(tǒng)創(chuàng)建通信信道，其基礎(chǔ)通信相對(duì)安全，因此將閱讀器和后臺(tái)系統(tǒng)看成一體。

(2)簡(jiǎn)化密鑰串表示，協(xié)議中的共享密鑰串K1，K2，K3，…記為密鑰元組 Key，即 Key={K1，K2，K3，…};

(3)定義一個(gè)密鑰基礎(chǔ)信息更新函數(shù)UPDATE()，此函數(shù)實(shí)現(xiàn)Reader端與Tag端密鑰更新操作;

(4)假設(shè)用于協(xié)議的密碼系統(tǒng)是完美的，為此，將協(xié)議中所有的加密操作抽象成函數(shù)ENC()，ENCkey為用函數(shù)ENC()加密的密鑰，這樣，研究的安全漏洞就是協(xié)議本身的缺陷。

遵循上述四條原則，運(yùn)用協(xié)議抽象建模方法可構(gòu)建出RCIA協(xié)議抽象交互模型，如圖1所示。

假設(shè)在協(xié)議會(huì)話初始時(shí)，Tag始終能夠響應(yīng)Hello消息并返回IDS數(shù)據(jù)，那么根據(jù)圖1模型，將RCIA協(xié)議交互流程進(jìn)一步簡(jiǎn)化并用形式化表示，得到如下協(xié)議:

其中，ID是標(biāo)簽的唯一身份信息，IDS是標(biāo)簽的假名信息，Key為密鑰元組，ENC()為加密函數(shù)，UPDATE()是更新函數(shù);Reader端和Tag端存儲(chǔ)的密鑰信息均為{Keyold，Keynew}。

3 RCIA協(xié)議Promela建模

Promela是一種描述并發(fā)系統(tǒng)的建模語(yǔ)言，用于有限狀態(tài)機(jī)系統(tǒng)建模。RCIA協(xié)議的Promela模型構(gòu)建包括:(1)誠(chéng)實(shí)主體的構(gòu)建，如消息通道定義、誠(chéng)實(shí)主體行為描述;(2)攻擊者構(gòu)建，如攻擊者知識(shí)庫(kù)構(gòu)建以及攻擊者行為描述。

3．1 誠(chéng)實(shí)主體建模

(1)消息通道構(gòu)建。

為了便于在模型中表示協(xié)議交互過程，構(gòu)建一個(gè)數(shù)據(jù)項(xiàng)的有限集合，定義如下:

該集合中定義了參與協(xié)議的各主體，發(fā)送的消息、密鑰信息及泛型數(shù)據(jù)，用來(lái)表示協(xié)議交互過程中的所有消息項(xiàng)，Key為協(xié)議所使用的密鑰，gD為泛型數(shù)據(jù)，Rt為不可識(shí)別的主體，后文將解釋Rt的作用。若協(xié)議中存在不同消息結(jié)構(gòu)，那么所需的消息通道也會(huì)不同。在RCIA協(xié)議交互過程中，根據(jù)發(fā)送和接收消息項(xiàng)數(shù)目不同，分別定義兩個(gè)不同的消息通道，即:

chan ca= ［0］ of{mtype，mtype，mtype，mtype，mtype，

byte};

chan cb=［0］of{mtype，mtype，mtype，byte};

以ca通道為例:

ca!Reader，A，B，C，Key，1;//消息發(fā)送語(yǔ)句

ca?eval(Reader)，x2，x3，x4，eval(Key)，x6;/* 消息接

收語(yǔ)句*/

在發(fā)送語(yǔ)句中，Reader為消息發(fā)送者，A、B和C為信息項(xiàng)，Key為加密密鑰，1為使用的密鑰版本;在消息接收語(yǔ)句中，函數(shù)eval()判斷接收值是否與目標(biāo)值相同，若相同則接受該消息，反之丟棄該消息。

(2)誠(chéng)實(shí)主體行為描述。

RCIA協(xié)議誠(chéng)實(shí)主體包括Reader和Tag，定義主體的各自進(jìn)程，分別命名為:proctype Reader()和proctype Tag()。在RCIA協(xié)議中，依據(jù)Reader和Tag初始存儲(chǔ)信息，分別定義各端的密鑰信息。Reader端存儲(chǔ){Keyold，Keynew}，Tag 端同樣存儲(chǔ){Keyold，Keynew}密鑰信息。因此，在Reader端定義一個(gè)長(zhǎng)度為2的密鑰數(shù)組表示密鑰信息:reader-KeySet［2］;類似地，Tag端密鑰數(shù)組為 TagKeySet［2］，并規(guī)定數(shù)組索引下標(biāo)為0是舊密鑰，為1是新密鑰。

RCIA協(xié)議運(yùn)行之初，Reader和Tag首先協(xié)商密鑰信息，確定初始會(huì)話所使用的密鑰版本。定義函數(shù)ChooseKey()協(xié)商密鑰信息，協(xié)商出的密鑰信息用curKey_use表示。協(xié)商好密鑰信息后，誠(chéng)實(shí)主體借助ca，cb通道發(fā)送和接收消息。協(xié)議交互過程中需要更新密鑰信息，定義函數(shù)Update(x，y，z，m，n)以更新密鑰信息。函數(shù)ChooseKey()基本思想是依次將Tag中密鑰信息與Reader中存儲(chǔ)的密鑰信息進(jìn)行比對(duì)，若匹配成功將當(dāng)前密鑰賦值給curKey_use;函數(shù) Update(x，y，z，m，n)中 x 為 IDS，y為Key，z為Reader或者Tag，m和n是接收到消息項(xiàng)內(nèi)容。Reader端更新規(guī)則:若curKey_use是舊密鑰，則更新 readerKeySet［1］;若 curKey_use是新密鑰，則將 readerKeySet［1］賦值給 readerKeySet［0］，賦值后更新 readerKeySet［1］。Tag端更新規(guī)則同Reader端，不作詳述。進(jìn)程Reader和Tag具體實(shí)現(xiàn)代碼如下:

proctype Reader(mtype self;mtype party;mtype msg1;mtype msg2;mtype msg3){

mtype g1;

mtype g2;

atomic{

ChooseKey();//選擇密鑰通信

IniRunning(self，party);

ca!self，msg1，msg2，msg3，Key，curKey_use;

}

atomic{

cb?eval(self)，g1，eval(Key)，eval(curKey_use);

Update(IDS，Key，Reader，g1，g2);/* 執(zhí)行密鑰更新

操作*/

IniCommit(self，party);

}

…}

proctype Tag(mtype self;mtype party;mtype msg){

mtype g1，g2，g3，g4;

atomic{

ca?eval(self)，g1，g2，g3，eval(Key)，eval(curKey_

use);

ResRunning(party，self);

}

atomic{

cb!self，msg，Key，1;

Update(IDS，Key，Tag，g1，g4);/* 執(zhí)行密鑰更新操

作*/

ResCommit(party，self);

}

proctype Reader()、proctype Tag()將各個(gè)操作語(yǔ)句定義在atomic塊中，有效縮減了狀態(tài)空間遷移數(shù)，以緩解狀態(tài)爆炸問題。

3．2 攻擊者建模

RCIA協(xié)議的攻擊者模型主要遵循Dolev-Yao［15］建模思想。在運(yùn)用Promela語(yǔ)言構(gòu)建攻擊者模型中，作出如下假設(shè):(1)攻擊者可以冒充任何合法主體;(2)攻擊者只有知道對(duì)應(yīng)的密鑰才能加解密消息;(3)攻擊者始終能截獲 Tag發(fā)送給Reader的IDS消息。

(1)攻擊者知識(shí)庫(kù)的構(gòu)建。

攻擊者知識(shí)庫(kù)由基礎(chǔ)知識(shí)集和可學(xué)習(xí)到的知識(shí)集構(gòu)成?；A(chǔ)知識(shí)集為攻擊者所擁有的初始知識(shí);可學(xué)習(xí)到的知識(shí)是指攻擊者通過截獲消息，用當(dāng)前已有知識(shí)解密得到的知識(shí)，而對(duì)于不能解密的消息，將其完整地存入知識(shí)庫(kù)。攻擊者最有價(jià)值的信息是由攻擊者可學(xué)會(huì)的知識(shí)(Set1)與需要學(xué)會(huì)的知識(shí)(Set2)求交集得到，如圖2所示。

集合Set1:攻擊者可學(xué)會(huì)的知識(shí)，在RCIA協(xié)議中，閱讀器與標(biāo)簽之間的密鑰信息是預(yù)共享的，攻擊者只能將所截獲的消息完全存儲(chǔ)。

集合Set2:攻擊者需要學(xué)會(huì)的知識(shí)，即攻擊者分析接收通道，構(gòu)建所有可能接收的消息時(shí)需要的知識(shí)。

在RCIA協(xié)議中，通過截獲發(fā)送通道的消息，攻擊者可學(xué)會(huì)的知識(shí)如表1所示。由于并無(wú)相關(guān)密鑰來(lái)解密消息，攻擊者只能學(xué)習(xí)到整條消息。

Table 1 Knowledge that an attacker can learn表1 攻擊者可學(xué)會(huì)的知識(shí)

分析攻擊者需要學(xué)會(huì)的知識(shí)，通過分析Reader端和Tag端接收語(yǔ)句:

其中，接收語(yǔ)句 g1、g2、g3 取值范圍{(A，B，C，D)，(A2，B2，C2，D2)}。對(duì)于 ca 通道，攻擊者可以構(gòu)建的消息數(shù)為:4*4*4*2=128條;對(duì)于cb通道，攻擊者可以構(gòu)建的消息數(shù)為8條。攻擊者需要學(xué)會(huì)的知識(shí)項(xiàng)如表2所示。

Table 2 Knowledge that an attacker needs to learn表2 攻擊者需要學(xué)會(huì)的知識(shí)

由表1與表2的第二列求交集得到攻擊者最有價(jià)值的信息，其表示的知識(shí)項(xiàng)為:

{A，B，C}ENCKey;{A2，B2，C2}ENCKey;{D}ENCKey;{D2}ENCKey

(2)攻擊者行為描述。

遵循Dolev-Yao攻擊者建模思想，在以上分析基礎(chǔ)上運(yùn)用Promela語(yǔ)言對(duì)攻擊者具體行為進(jìn)行建模。建模分為三部分:消息的截取、知識(shí)項(xiàng)的表示與學(xué)習(xí)、消息的構(gòu)建與發(fā)送。

①消息的截取:定義語(yǔ)句 ca?_，x1，x2，x3，攻擊者可實(shí)現(xiàn)截獲所有誠(chéng)實(shí)主體發(fā)送的消息。其中，語(yǔ)句中的“_”是指不需要判斷消息來(lái)自哪里，直接接收。

②知識(shí)項(xiàng)的表示與學(xué)習(xí):攻擊者截獲消息后，用已有知識(shí)對(duì)消息進(jìn)行學(xué)習(xí)。定義以k_為前綴，例如 k_A_B_C__Key 表示{A，B，C}ENCKey這個(gè)消息的知識(shí)，初始值為0，表示攻擊者還未學(xué)習(xí)到此知識(shí);若值為1，表示該知識(shí)項(xiàng)已經(jīng)被攻擊者學(xué)會(huì)。實(shí)現(xiàn)代碼如下。

#define k1(x1)if

③消息的構(gòu)建與發(fā)送:攻擊者利用初始知識(shí)和學(xué)習(xí)到的知識(shí)構(gòu)建各種消息發(fā)送給誠(chéng)實(shí)主體。例如發(fā)送語(yǔ)句:

ca!(((kA＆＆kB＆＆kC＆＆k_Key)‖ k_A_B_C__Key)→ Tag:Rt)，A，B，C，Key，1

攻擊者要么分別知道A、B、C和Key，要么在知道整條消息的情況下，才能構(gòu)造{A，B，C}ENCKey并發(fā)送給Tag;否則，會(huì)將整條消息發(fā)給一個(gè)不存在的主體Rt。這就意味著，只有攻擊者充分學(xué)習(xí){A，B，C}ENCKey這個(gè)消息，才會(huì)將此消息構(gòu)建或轉(zhuǎn)發(fā)給合法主體。定義攻擊者進(jìn)程為PI，攻擊者行為描述代碼如下所示:

proctype PI(){

bit k_A_B_C__Key=0;bit k_D__Key=0;

bit k_A2_B2_C2__Key=0;

bit k_D2__Key=0;bit kx=0;bit kA=0;

bit kB=0;bit kC=0;

bit kD=0;bit k_Key=0;bit kA2=0;

bit kB2=0;bit kC2=0;bit kD2=0;

mtype x1=0，x2=0，x3=0，x4=0，x5=0

do

::ca!((kA ＆＆ k_Key)→ Tag:R)，A，A，A，Key，1//

攻擊者向ca、cb通道發(fā)送消息

::ca!((kA ＆＆ kB ＆＆ k_Key)→ Tag:R)，A，A，B，

Key，1

……

::cb!((kA ＆＆ k_Key)→ Reader:R)，A，Key，1

::cb!((kB ＆＆ k_Key)→ Reader:R)，B，Key，1

::d_step{ca?_，x1，x2，x3，x4，x5;… }/* 攻擊者知

識(shí)庫(kù)構(gòu)建*/

::d_step{cb?_，x1，x2，x3;… }/* 攻擊者知識(shí)庫(kù)構(gòu)

建*/

::CheckConsistency()

od

}

3．3 協(xié)議安全屬性刻畫

為了將協(xié)議的安全性質(zhì)描述成SPIN可接受的語(yǔ)言，需要運(yùn)用線性時(shí)態(tài)邏輯LTL(Linear Time Logic)［16，17］刻畫協(xié)議需要滿足的安全性質(zhì)，SPIN自動(dòng)驗(yàn)證協(xié)議模型與安全屬性之間的正確性，若出現(xiàn)性質(zhì)違反，說(shuō)明協(xié)議存在漏洞，SPIN將給出攻擊序列。

作為雙向認(rèn)證協(xié)議，RCIA使Reader和Tag之間完成相互認(rèn)證，完成對(duì)應(yīng)的假名、密鑰更新操作。因此，需要對(duì)協(xié)議認(rèn)證性、一致性進(jìn)行描述。其中，認(rèn)證性指Reader和Tag之間完成相互認(rèn)證;一致性指Reader端和Tag端在會(huì)話完成后，兩端所存儲(chǔ)的密鑰信息版本相同。描述協(xié)議的認(rèn)證性、一致性，可借助原子謂詞表示。在Promela語(yǔ)言中，定義如下全局變量描述協(xié)議的認(rèn)證性、一致性:

bit ConsistencyRT=1;bit IniRunningRT=0;

bit IniCommitRT=0;bit ResRunningRT=0;

bit ResCommitRT=0;

其中，ConsistencyRT表示閱讀器端與標(biāo)簽端密鑰版本信息的一致性;ConsistencyRT值為1即Reader端中存儲(chǔ)的密鑰版本總有一個(gè)與Tag端對(duì)應(yīng)，值為0表示Reader端與Tag端密鑰版本不一致。IniRunningRT表示Reader參與了和Tag的會(huì)話，Ini-CommitRT表示 Reader提交了和 Tag的對(duì)話，ResRunningRT表示Tag參與了和Reader的會(huì)話，ResCommitRT表示Tag提交了和Reader的會(huì)話;其初始值為0表示未參與/提交會(huì)話，為1表示參與/提交會(huì)話。定義全局變量后，需對(duì)原子謂詞值進(jìn)行更新，可通過宏定義方式更新原子謂詞值。宏定義如下:

運(yùn)用已定義好的原子謂詞，RCIA協(xié)議認(rèn)證性描述為:Tag對(duì)Reader的認(rèn)證，即在 IniCommitRT之前，ResRunningRT值必須為真;Reader對(duì)Tag的認(rèn)證，即在ResCommitRT之前，IniRunningRT值必須為真。協(xié)議一致性指ConsistencyRT總是為真。上述安全屬性轉(zhuǎn)化為L(zhǎng)TL公式，如下所示:

4 實(shí)驗(yàn)結(jié)果與分析

定義各進(jìn)程后，在Windows 7 64位系統(tǒng)下使用 Cygwin 2．510．2．2 構(gòu)建的環(huán)境中，使用 SPIN 5．2．0對(duì)RCIA協(xié)議進(jìn)行驗(yàn)證，發(fā)現(xiàn)如圖3所示的攻擊序列。圖3描述了RCIA中的一種去同步攻擊漏洞:

具體攻擊過程如下:

Stage1:

盡管無(wú)相關(guān)密鑰去解密每條信息，攻擊者仍能學(xué)習(xí)會(huì)話中的整體消息，將其存儲(chǔ)和轉(zhuǎn)發(fā)。

Stage1中，攻擊者轉(zhuǎn)發(fā)每條消息使Reader和Tag能正常通信和更新密鑰，同時(shí)攻擊者記錄并存儲(chǔ)消息(1．1)和消息(1．3)。會(huì)話完成后，兩端密鑰版本為{1，2}。

Stage2中，Reader使用新密鑰(即密鑰版本2)與Tag通信，但攻擊者截獲發(fā)送給Tag的消息(2．1)，并重放消息(1．3)給 Reader;Reader收到消息(1．3)后認(rèn)為此“Tag”還未更新密鑰，嘗試使用舊密鑰(即密鑰版本1)與Tag通信，進(jìn)入到Stage3。

Stage3中，Reader使用舊密鑰與Tag通信并正常更新密鑰信息，但攻擊者記錄并存儲(chǔ)消息(3．1)。Stage3階段會(huì)話完成后，Reader端和Tag端的密鑰版本均為{1，3}。隨后，攻擊者在Stage4和Stage5階段均假冒Reader與Tag通信。

Stage4中，攻擊者重放消息(1．1)給Tag。因?yàn)樵撓⑹褂肧tage1的數(shù)據(jù)，Tag端驗(yàn)證消息后更新本端密鑰，密鑰版本回退至{1，2}。

Stage5中，攻擊者重放消息(2．1)給Tag。因?yàn)樵撓⑹且悦荑€版本2加密的，因此重放的消息依舊能通過驗(yàn)證。同時(shí)更新本端密鑰，密鑰版本更新至{2，4}。攻擊結(jié)束后，將導(dǎo)致合法標(biāo)簽再也無(wú)法與閱讀器通信。RCIA協(xié)議中各原子謂詞及變量的值如圖4所示。

圖 4中 ConsistencyRT值為 0，IniRuningRT、ResRuningRT、IniCommitRT及 ResCommitRT值均為1，表示RCIA協(xié)議滿足認(rèn)證性而不滿足一致性，即協(xié)議存在去同步攻擊漏洞。

此外，在RCIA協(xié)議模型檢測(cè)結(jié)果中，還可以查看到更多關(guān)于驗(yàn)證的信息，如:狀態(tài)矢量(statevector)、搜索深度(depth reached)、狀態(tài)存儲(chǔ)數(shù)(state stored)、狀態(tài)匹配數(shù)(state matched)、遷移量(transitions)、原子步個(gè)數(shù)(atomic steps)等，如圖5所示。

從圖5可知，本次驗(yàn)證過程中花費(fèi)76字節(jié)內(nèi)存來(lái)存儲(chǔ)全局系統(tǒng)狀態(tài)，搜索深度達(dá)到93層，驗(yàn)證結(jié)果為not valid。

5 協(xié)議改進(jìn)及形式化分析驗(yàn)證

以上實(shí)驗(yàn)結(jié)果表明，RCIA協(xié)議存在去同步攻擊漏洞，需對(duì)該漏洞進(jìn)行分析，并提出對(duì)RCIA協(xié)議的改進(jìn)方案，從而提高該協(xié)議的安全性。

5．1 去同步攻擊漏洞改進(jìn)方案

Reader與Tag雙方認(rèn)證完成后會(huì)更新各自密鑰信息以保持一致，去同步攻擊目標(biāo)是使兩端密鑰失衡。需要指出的是，攻擊者始終不能竊取到加密密鑰，只能通過重放已有的消息來(lái)實(shí)現(xiàn)攻擊。那么，可引入冗余機(jī)制使所有密鑰更新信息可被檢索，使攻擊者重放消息后，主體更新的密鑰信息還能在可回溯范圍之內(nèi)。基于以上分析，本文提出一種密鑰同步機(jī)制，具體內(nèi)容為:

(1)定義固定長(zhǎng)度的密鑰更新鏈，用以存儲(chǔ)歷史會(huì)話中密鑰更新信息。當(dāng)密鑰更新鏈存儲(chǔ)空間不足時(shí)，回收最久未使用的舊密鑰以釋放存儲(chǔ)空間。

(2)當(dāng)使用舊密鑰進(jìn)行通信時(shí)，Reader端首先需要使用舊密鑰對(duì)Tag端進(jìn)行密鑰信息的強(qiáng)制更新，使Reader和Tag端密鑰信息始終保持同步。

5．2 基于密鑰同步機(jī)制的RCIA協(xié)議改進(jìn)

考慮到Tag端存儲(chǔ)和計(jì)算資源受限，而Reader端不受限制，因此密鑰更新機(jī)制可在Reader端實(shí)現(xiàn)。事實(shí)上，密鑰同步機(jī)制沒有改變RCIA的交互過程，我們假設(shè)當(dāng)標(biāo)簽從Reader收到Hello信息時(shí)，總是回復(fù) IDS。因此，運(yùn)用密鑰同步機(jī)制對(duì)RCIA協(xié)議改進(jìn)的形式化表述如下所示:

由于改進(jìn)后的RCIA協(xié)議的消息結(jié)構(gòu)和交互流程并未發(fā)生改變，因此改進(jìn)后的RCIA中的誠(chéng)實(shí)主體行為描述、攻擊者知識(shí)庫(kù)的構(gòu)建及行為描述都與上述未改進(jìn)的RCIA協(xié)議形式化分析結(jié)果一致。不同的是，改進(jìn)的RCIA協(xié)議需要具體實(shí)現(xiàn)密鑰更新鏈，這是密鑰同步機(jī)制的關(guān)鍵。為此，在Promela中，可用數(shù)組模擬實(shí)現(xiàn)密鑰更新鏈，另外定義一個(gè)宏設(shè)定密鑰更新鏈的固定大小，如代碼所示:

定義好密鑰更新鏈后，上述未改進(jìn)RCIA協(xié)議的主體的密鑰、選擇函數(shù)ChooseKey()和密鑰更新函數(shù) Update(x，y，z，m，n)都需要重構(gòu)。為了便于在readerKeySet［N］中索引，有必要引入for()循環(huán)函數(shù)，但在Promela循環(huán)結(jié)構(gòu)中無(wú)for()循環(huán)定義，為此我們利用do…od實(shí)現(xiàn)for()循環(huán)，具體代碼如下:

實(shí)現(xiàn)for()循環(huán)后，密鑰選擇函數(shù)ChooseKey()只需將收到的Key在密鑰更新鏈readerKeySet［N］中循環(huán)索引并將值返回給curKey_use即可。而對(duì)于密鑰更新函數(shù) Update(x，y，z，m，n)的實(shí)現(xiàn):(1)Reader端，首先判斷當(dāng)前的會(huì)話密鑰curKey_use是否為新密鑰，若是，則在密鑰更新鏈 readerKeySet［N］中追加新密鑰;若為舊密鑰，則不更新密鑰，直至Tag端使用新密鑰進(jìn)行會(huì)話;(2)Tag端，若cur-Key_use是舊密鑰，則更新 tagKeySet［1］;若 curKey_use是新密鑰，首先將tagKeySet［1］賦值給 tagKey-Set［0］，賦值完之后更新 tagKeySet［1］。

5．3 改進(jìn)后的RCIA協(xié)議分析與驗(yàn)證

類似地，定義改進(jìn)的RCIA協(xié)議誠(chéng)實(shí)主體、攻擊者進(jìn)程及需要遵循的安全性質(zhì)后，使用SPIN進(jìn)行驗(yàn)證，并未出現(xiàn)性質(zhì)違反，如圖6所示:

表3描述了RCIA協(xié)議改進(jìn)前和改進(jìn)后的驗(yàn)證結(jié)果，從結(jié)果對(duì)比可看出，改進(jìn)后的協(xié)議在遷移量、搜索算法深度等數(shù)據(jù)上都有比較大的提升。這是因?yàn)镾PIN工具在驗(yàn)證模型性質(zhì)時(shí)，一旦檢測(cè)到某個(gè)性質(zhì)違反時(shí)就會(huì)停止驗(yàn)證，這也從側(cè)面驗(yàn)證了基于密鑰同步機(jī)制的RCIA協(xié)議安全性、可靠性更高。

Table 3 Comparison of verification results between the RCIA and improved RCIA protocol表3 RCIA協(xié)議與改進(jìn)的RCIA協(xié)議驗(yàn)證結(jié)果對(duì)比

6 結(jié)束語(yǔ)

本文基于形式化方法對(duì)RFID標(biāo)簽認(rèn)證協(xié)議RCIA進(jìn)行分析與驗(yàn)證，提出了一種協(xié)議抽象建模方法，降低超輕量級(jí)協(xié)議描述的復(fù)雜度，從而可以采用模型檢測(cè)工具SPIN驗(yàn)證其安全屬性。驗(yàn)證結(jié)果表明，RCIA協(xié)議存在去同步攻擊漏洞。針對(duì)該漏洞，本文提出了一種基于密鑰同步機(jī)制的改進(jìn)方案，對(duì)改進(jìn)RCIA協(xié)議形式化分析與驗(yàn)證的結(jié)果表明改進(jìn)的協(xié)議具有更高的安全性。然而，我們不能保證改進(jìn)的RCIA協(xié)議是絕對(duì)安全的，因?yàn)槟Ｐ蜋z測(cè)方法只能檢測(cè)協(xié)議的缺陷，不能驗(yàn)證其正確性。因此，我們下一步工作將采用定理證明方法證明協(xié)議的正確性。