RFID超輕量級認證協(xié)議RCIA形式化分析與改進*

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

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

1 引言

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

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

超輕量級雙向認證協(xié)議UMAP(Ultra-lightweight Mutual Authentication Protocols)是輕量級安全協(xié)議中的一個重要分支［4］。UMAP在標簽端使用簡單逐位(bitwise)操作(比如 XOR、AND、OR、循環(huán)移位和模加等運算)以加密通信數(shù)據(jù)。輕量級雙向認證協(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中提出的超輕量級雙向認證協(xié)議。該協(xié)議采用一種新的加密原語:遞歸哈希(recursive hash)，聲稱遞歸哈希原語將給RCIA協(xié)議帶來高安全性。然而，2016年Safkhani等人［12］描述了在超輕量級相互認證協(xié)議中存在去同步攻擊漏洞，并指出該漏洞同樣存在最近提出的RCIA協(xié)議中。2017年，Yasear等人［13］發(fā)現(xiàn)RCIA中存在惡意跟蹤攻擊，并且提出基于逐位操作的隨機數(shù)生成器(RNG)技術(shù)以克服該攻擊。

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

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

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

2．1 RCIA 協(xié)議

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

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

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

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

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

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

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

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

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

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

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

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

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

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

3 RCIA協(xié)議Promela建模

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

3．1 誠實主體建模

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

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

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

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ā)送語句

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

收語句*/

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

(2)誠實主體行為描述。

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

RCIA協(xié)議運行之初，Reader和Tag首先協(xié)商密鑰信息，確定初始會話所使用的密鑰版本。定義函數(shù)ChooseKey()協(xié)商密鑰信息，協(xié)商出的密鑰信息用curKey_use表示。協(xié)商好密鑰信息后，誠實主體借助ca，cb通道發(fā)送和接收消息。協(xié)議交互過程中需要更新密鑰信息，定義函數(shù)Update(x，y，z，m，n)以更新密鑰信息。函數(shù)ChooseKey()基本思想是依次將Tag中密鑰信息與Reader中存儲的密鑰信息進行比對，若匹配成功將當前密鑰賦值給curKey_use;函數(shù) Update(x，y，z，m，n)中 x 為 IDS，y為Key，z為Reader或者Tag，m和n是接收到消息項內(nèi)容。Reader端更新規(guī)則:若curKey_use是舊密鑰，則更新 readerKeySet［1］;若 curKey_use是新密鑰，則將 readerKeySet［1］賦值給 readerKeySet［0］，賦值后更新 readerKeySet［1］。Tag端更新規(guī)則同Reader端，不作詳述。進程Reader和Tag具體實現(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()將各個操作語句定義在atomic塊中，有效縮減了狀態(tài)空間遷移數(shù)，以緩解狀態(tài)爆炸問題。

3．2 攻擊者建模

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

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

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

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

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

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

Table 1 Knowledge that an attacker can learn表1 攻擊者可學會的知識

分析攻擊者需要學會的知識，通過分析Reader端和Tag端接收語句:

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

Table 2 Knowledge that an attacker needs to learn表2 攻擊者需要學會的知識

由表1與表2的第二列求交集得到攻擊者最有價值的信息，其表示的知識項為:

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

(2)攻擊者行為描述。

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

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

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

#define k1(x1)if

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

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;否則，會將整條消息發(fā)給一個不存在的主體Rt。這就意味著，只有攻擊者充分學習{A，B，C}ENCKey這個消息，才會將此消息構(gòu)建或轉(zhuǎn)發(fā)給合法主體。定義攻擊者進程為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;… }/* 攻擊者知

識庫構(gòu)建*/

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

建*/

::CheckConsistency()

od

}

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

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

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

bit ConsistencyRT=1;bit IniRunningRT=0;

bit IniCommitRT=0;bit ResRunningRT=0;

bit ResCommitRT=0;

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

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

4 實驗結(jié)果與分析

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

具體攻擊過程如下:

Stage1:

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

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

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

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

Stage4中，攻擊者重放消息(1．1)給Tag。因為該消息使用Stage1的數(shù)據(jù)，Tag端驗證消息后更新本端密鑰，密鑰版本回退至{1，2}。

Stage5中，攻擊者重放消息(2．1)給Tag。因為該消息是以密鑰版本2加密的，因此重放的消息依舊能通過驗證。同時更新本端密鑰，密鑰版本更新至{2，4}。攻擊結(jié)束后，將導致合法標簽再也無法與閱讀器通信。RCIA協(xié)議中各原子謂詞及變量的值如圖4所示。

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

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

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

5 協(xié)議改進及形式化分析驗證

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

5．1 去同步攻擊漏洞改進方案

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

(1)定義固定長度的密鑰更新鏈，用以存儲歷史會話中密鑰更新信息。當密鑰更新鏈存儲空間不足時，回收最久未使用的舊密鑰以釋放存儲空間。

(2)當使用舊密鑰進行通信時，Reader端首先需要使用舊密鑰對Tag端進行密鑰信息的強制更新，使Reader和Tag端密鑰信息始終保持同步。

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

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

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

定義好密鑰更新鏈后，上述未改進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)中無for()循環(huán)定義，為此我們利用do…od實現(xiàn)for()循環(huán)，具體代碼如下:

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

5．3 改進后的RCIA協(xié)議分析與驗證

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

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

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

6 結(jié)束語

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