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

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

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

1 引言

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

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

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

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

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

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

2 RCIA協議及協議抽象建模

2．1 RCIA 協議

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

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

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

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

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

2．2 協議抽象建模方法

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

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

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

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

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

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

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

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

3 RCIA協議Promela建模

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

3．1 誠實主體建模

(1)消息通道構建。

為了便于在模型中表示協議交互過程，構建一個數據項的有限集合，定義如下:

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

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;//消息發送語句

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

收語句*/

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

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

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

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

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);/* 執行密鑰更新

操作*/

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);/* 執行密鑰更新操

作*/

ResCommit(party，self);

}

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

3．2 攻擊者建模

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

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

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

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

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

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

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

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

其中，接收語句 g1、g2、g3 取值范圍{(A，B，C，D)，(A2，B2，C2，D2)}。對于 ca 通道，攻擊者可以構建的消息數為:4*4*4*2=128條;對于cb通道，攻擊者可以構建的消息數為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攻擊者建模思想，在以上分析基礎上運用Promela語言對攻擊者具體行為進行建模。建模分為三部分:消息的截取、知識項的表示與學習、消息的構建與發送。

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

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

#define k1(x1)if

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

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

攻擊者要么分別知道A、B、C和Key，要么在知道整條消息的情況下，才能構造{A，B，C}ENCKey并發送給Tag;否則，會將整條消息發給一個不存在的主體Rt。這就意味著，只有攻擊者充分學習{A，B，C}ENCKey這個消息，才會將此消息構建或轉發給合法主體。定義攻擊者進程為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通道發送消息

::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;… }/* 攻擊者知

識庫構建*/

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

建*/

::CheckConsistency()

od

}

3．3 協議安全屬性刻畫

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

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

bit ConsistencyRT=1;bit IniRunningRT=0;

bit IniCommitRT=0;bit ResRunningRT=0;

bit ResCommitRT=0;

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

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

4 實驗結果與分析

定義各進程后，在Windows 7 64位系統下使用 Cygwin 2．510．2．2 構建的環境中，使用 SPIN 5．2．0對RCIA協議進行驗證，發現如圖3所示的攻擊序列。圖3描述了RCIA中的一種去同步攻擊漏洞:

具體攻擊過程如下:

Stage1:

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

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

Stage2中，Reader使用新密鑰(即密鑰版本2)與Tag通信，但攻擊者截獲發送給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的數據，Tag端驗證消息后更新本端密鑰，密鑰版本回退至{1，2}。

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

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

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

從圖5可知，本次驗證過程中花費76字節內存來存儲全局系統狀態，搜索深度達到93層，驗證結果為not valid。

5 協議改進及形式化分析驗證

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

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

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

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

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

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

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

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

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

實現for()循環后，密鑰選擇函數ChooseKey()只需將收到的Key在密鑰更新鏈readerKeySet［N］中循環索引并將值返回給curKey_use即可。而對于密鑰更新函數 Update(x，y，z，m，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協議分析與驗證

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

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

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

6 結束語

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