熊 飛，陳 芳，周鴻喜，呂俊峰，黨育軍，谷勇浩，于華東，徐長福，路永玲，王 鵬

（1.國家電網(wǎng)公司信息通信分公司，北京 100761；2.北京郵電大學(xué) 計(jì)算機(jī)學(xué)院 智能通信軟件與多媒體北京市重點(diǎn)實(shí)驗(yàn)室，北京 100876；3.國網(wǎng)信息通信產(chǎn)業(yè)集團(tuán)有限公司研發(fā)中心，北京 102211；4.國網(wǎng)江蘇省電力公司電力科學(xué)研究院，南京 211103；5.中國科學(xué)院計(jì)算技術(shù)研究所，北京 100080）

一種基于靜態(tài)ID機(jī)制可證明安全的RFID協(xié)議

熊 飛1，陳 芳1，周鴻喜1，呂俊峰1，黨育軍1，谷勇浩2，于華東3，徐長福4，路永玲4，王 鵬5

（1.國家電網(wǎng)公司信息通信分公司，北京 100761；2.北京郵電大學(xué) 計(jì)算機(jī)學(xué)院 智能通信軟件與多媒體北京市重點(diǎn)實(shí)驗(yàn)室，北京 100876；3.國網(wǎng)信息通信產(chǎn)業(yè)集團(tuán)有限公司研發(fā)中心，北京 102211；4.國網(wǎng)江蘇省電力公司電力科學(xué)研究院，南京 211103；5.中國科學(xué)院計(jì)算技術(shù)研究所，北京 100080）

電力物聯(lián)網(wǎng)中部分電力設(shè)備可采用 RFID方式接入，RFID需要設(shè)計(jì)一個滿足高效、安全、低成本要求的RFID安全協(xié)議。論文在對現(xiàn)有RFID安全技術(shù)分析的基礎(chǔ)上，提出一種基于靜態(tài)ID機(jī)制可證明安全的RFID協(xié)議,以解決現(xiàn)有靜態(tài)安全協(xié)議的不足，同時對所提協(xié)議與現(xiàn)有協(xié)議在安全性方面做了對比，并對所提協(xié)議進(jìn)行了GNY形式化分析和證明。

電力物聯(lián)網(wǎng)；RFID；空口通信；安全協(xié)議；GNY邏輯分析

0 引言

目前基于 RFID的變電站巡檢系統(tǒng)作為一種先進(jìn)的技術(shù)手段，已經(jīng)成功應(yīng)用于特高壓站點(diǎn)。其系統(tǒng)通過內(nèi)置GPRS及LTE230模塊回傳數(shù)據(jù)，可以將記錄有電力設(shè)備的運(yùn)行狀態(tài)、缺陷信息回傳于接收控制系統(tǒng)，但是空口傳輸?shù)耐该餍约?RFID芯片可靠性，決定了設(shè)備信息在傳輸過程中容易被竊取、仿造、篡改，因此需要對 RFID空口傳輸?shù)陌踩珯C(jī)制進(jìn)行分析，給出有效的空口通信模型，提出保障變電站信息可靠傳輸?shù)募夹g(shù)措施和手段，確保電力系統(tǒng)安全穩(wěn)定運(yùn)行。RFID低成本、低能耗、計(jì)算能力較弱對 RFID安全協(xié)議提出了新的要求，不能使用現(xiàn)有經(jīng)典但比較復(fù)雜的加密算法。因此設(shè)計(jì)一個滿足高效、安全、低成本要求的 RFID安全協(xié)議顯得十分必要。

2 研究現(xiàn)狀

RFID安全機(jī)制主要包括物理方法和密碼學(xué)技術(shù)。物理方法主要保護(hù) RFID標(biāo)簽持有者的隱私，包含設(shè)置休眠機(jī)制，廢棄機(jī)制，阻塞機(jī)制，重新貼標(biāo)和法拉第標(biāo)簽套等；針對標(biāo)簽中的ID是否更新可將基于密碼學(xué)技術(shù)的安全機(jī)制分為：靜態(tài)ID機(jī)制和動態(tài)ID機(jī)制。

動態(tài)ID機(jī)制的安全協(xié)議包括Hash-Chain協(xié)議、基于雜湊 ID變化協(xié)議、LCAP協(xié)議、Ownership Transfer協(xié)議、πRSC協(xié)議等。靜態(tài)ID機(jī)制的安全協(xié)議包括Hash-Lock協(xié)議、隨機(jī)化Hash-Lock協(xié)議、分布式RFID詢問-響應(yīng)認(rèn)證協(xié)議、Hash鏈協(xié)議、數(shù)字圖書館RFID協(xié)議、HASP協(xié)議等。

基于靜態(tài) ID機(jī)制的安全協(xié)議存在以下問題：（1）標(biāo)簽跟蹤，（2）重放攻擊（3）偽裝攻擊（4）成本過高等。因此，本文提出了一種基于靜態(tài)ID機(jī)制可證明安全的RFID協(xié)議，解決上述問題。

3 基于靜態(tài)ID機(jī)制可證明安全的RFID協(xié)議

3.1 協(xié)議描述

基于靜態(tài)ID機(jī)制可證明安全的RFID協(xié)議流程如圖1所示。

各部分?jǐn)?shù)據(jù)存儲情況如下：

1.Back-End BD：分區(qū)儲存Tag的ID，其中Tag所在區(qū)域用XT表示；ID所對應(yīng)的Data；

2.Reader：儲存前i次來自Tag的H(ID//Rrj)（i是可調(diào)數(shù)，當(dāng)重放攻擊多時可調(diào)大i，從而使得重放攻擊效果變差）；

3.Tag：自身的ID；自加數(shù)j；Tag自身ID所在區(qū)域XT；需要在一個工作周期內(nèi)儲存隨機(jī)數(shù)Rr，周期結(jié)束后刪除。

表1 符號說明Table 1 Symbols

協(xié)議描述如下：

Step 1：Challenge

Reader向Tag發(fā)送Query和隨機(jī)數(shù)Rr。

Step 2：T-R Response

Tag接收到后，取隨機(jī)數(shù)的第j部分（Rr總共被分為n+1個部分），進(jìn)行計(jì)算H(ID//Rrj)，將H(ID// Rrj) 和XT傳送給Reader；并且當(dāng) j＜n時進(jìn)行自加1運(yùn)算，當(dāng) j=n時則 j=1。

Step 3：R-B Response

Reader接收到Tag的回饋信息后，會將新接收到的H(ID//Rrj)與之前自身儲存的 H()對比，如果相同則過濾掉（默認(rèn)為重放攻擊）；Reader將正常的H(ID//Rrj)，XT，隨機(jī)數(shù)Rr傳送給Back-End BD。

Step 4：B-R Reply

Back-End BD接收到信息后，選取XT區(qū)內(nèi)的ID，與分段的Rr進(jìn)行 H()運(yùn)算，并與接收到的H(ID//Rrj)對比如果有相同的，則找到匹配的ID；將這一ID與隨機(jī)數(shù)Rr的n+1部分進(jìn)行H()運(yùn)算；然后把H(ID//Rrn+ 1)和Data發(fā)送回Reader。

圖1 基于靜態(tài)ID機(jī)制可證明安全的RFID協(xié)議Fig.1 A provably secure RFID protocol based on static ID mechanism

Step 5：R-T Reply

Reader接收到 Back-End BD的信息后，將H(ID//Rrn +1)發(fā)送回 Tag，Tag會將儲存的隨機(jī)數(shù)Rr的第n+1部分與自身的ID做H()運(yùn)算，然后所得的值與接收到的H(ID//Rrn+1)匹配；匹配通過則停止發(fā)送信號。

3.2 協(xié)議安全性分析

下面是本協(xié)議與相關(guān)靜態(tài)協(xié)議在實(shí)現(xiàn)功能和抗各種攻擊方面的對比：

表2 協(xié)議在各種攻擊上的對比Table 2 Comparison of protocols in various attacks

3.3 協(xié)議的GNY邏輯分析與證明

安全協(xié)議形式化分析技術(shù)可使協(xié)議設(shè)計(jì)者通過系統(tǒng)分析將注意力集中于接口，系統(tǒng)環(huán)境的假設(shè)，在不同條件下系統(tǒng)的狀態(tài)，條件不滿足時出現(xiàn)的情況以及系統(tǒng)不變的屬性；并通過系統(tǒng)驗(yàn)證，提供協(xié)議必要的安全保證，通俗地講，安全協(xié)議的形式化分析是采用一種正規(guī)的，標(biāo)準(zhǔn)的方法對協(xié)議進(jìn)行分析，以檢查協(xié)議是否滿足其安全目標(biāo)。

3.3.1 GNY邏輯符號

下面先介紹GNY邏輯的基本符號：

1.P?X某一主體向P發(fā)送了包含X的信息。

2.P?*X某一主體向 P發(fā)送了包含新鮮的信息X的信息。

3.P?X 主體P擁有X（信息，或算法）。

4.P≡|#(X) P相信X是新鮮的。

5.P|～X P發(fā)送了包含公式X的消息。

6.P|≡φ(X) P可通過X的內(nèi)容和格式識別X。

8.P|≡C P相信命題C為真。

10.P|?CP對X有管轄權(quán)。

3.3.2 對基于分組隨機(jī)數(shù)的安全協(xié)議的 GNY邏輯證明

協(xié)議的GNY邏輯的證明過程，包括：GNY邏輯描述協(xié)議，協(xié)議要證明的邏輯問題，對 RFID各部分所具有功能或儲存的數(shù)據(jù)進(jìn)行邏輯化假設(shè)，用上述GNY邏輯公理結(jié)合邏輯化假設(shè)證明所提問題。

（1）協(xié)議邏輯化

把原始協(xié)議的 5條消息按照傳遞順序轉(zhuǎn)換成GNY的邏輯符號，描述如下：

注：使用S[]命名每一步，取意Step。

（2）要證明的問題

我們把協(xié)議的安全性簡化為兩個邏輯問題，既后臺數(shù)據(jù)庫和標(biāo)簽間是否能夠互相接收到可信的（就是確認(rèn)是來自于對方）且這個消息是新發(fā)送的（非被截取后重發(fā)的消息）。

Q[1]B|≡T|～#(H（ID//Rrj）)后臺數(shù)據(jù)庫確認(rèn)是來自于標(biāo)簽新鮮的信息。

Q[2]T|≡|B～#（H（ID//Rr n+1）） 標(biāo)簽確認(rèn)是來自于后臺數(shù)據(jù)庫新鮮的信息。

注：Q[1]和Q[2]取義Question。

（3）初始假設(shè)

①對Tag的假設(shè)

Tag[1]Tag擁有ID: T?ID

Tag[2]Tag擁有XT: T?XT

Tag[3]Tag 相信隨機(jī)數(shù) Rr是新鮮的: T|≡#（Rr）

Tag[4]Tag擁有算法H(x):T?H（X）

②對Reader的假設(shè)

Re[1]Reader擁有上次傳入的H'(ID//R rj): R?H′（ID//Rrj）

Re[2]Reader相信隨機(jī)數(shù) Rr與接收到的H（ID//Rrj）是新鮮的:R|≡#（Rr ）R|≡#（H（ID//Rrj））

Re[3]Reader與BD間的信道是安全的:R|≡ B|?B|≡*

③對Back-End BD的假設(shè)

BD[1]BD擁有ID:B?ID

BD[2]BD擁有算法H(X):B?H（X） BD[3]BD與 Tag共同擁有安全隨機(jī)數(shù)Rrj和

BD[4]BD擁有XT: B?XT

BD[5]BD 與 Reader間的信道是安全的:B|≡R|?R≡*

BD[6]BD 擁有所有 ID 對應(yīng)的 DATA: B?DATA

注：下面中(A,B) ?C表示由A和B條件推理出條件C。

（4）對Q[1]的證明

（5）對Q[2]的證明

通過 GNY邏輯我們證明了本協(xié)議能夠達(dá)到實(shí)現(xiàn)安全認(rèn)證和數(shù)據(jù)傳輸?shù)墓δ埽俏覀冏⒁獾?，在初始假設(shè)中XT，并沒有在后面證明中用到，也就是說在實(shí)現(xiàn)安全認(rèn)證和數(shù)據(jù)傳輸時并沒有用到這個值，它對于認(rèn)證過程是一個冗余量，但是在前面對XT進(jìn)行解釋時說明了這個量是為了使得后臺數(shù)據(jù)庫運(yùn)算復(fù)雜度降低，也就是說對于安全認(rèn)證這一過程，XT是沒有作用的，但是對于優(yōu)化整個安全認(rèn)證協(xié)議還是有重要作用的。這說明GNY邏輯可以檢測出協(xié)議中存在的冗余。

4 結(jié)語

本文提出了一種基于靜態(tài) ID機(jī)制可證明安全的RFID協(xié)議，將其與其他靜態(tài)ID機(jī)制的RFID安全協(xié)議在抵御攻擊方面進(jìn)行比較，然后通過 GNY形式化驗(yàn)證了本協(xié)議，證明了本協(xié)議能夠?qū)崿F(xiàn)安全認(rèn)證和數(shù)據(jù)傳輸?shù)墓δ堋?/p>

參考文獻(xiàn)

[1]周永彬, 馮登國.RFID安全協(xié)議的設(shè)計(jì)與分析[J].計(jì)算機(jī)軟件學(xué)報(bào), 2006, 29(4): 581-589.

[2]丁振華, 李錦濤, 馮波.基于Hash函數(shù)的RFID安全認(rèn)證協(xié)議研究[J].計(jì)算機(jī)研究與發(fā)展, 2009, 46(4): 583-592.

[3]鄭和喜, 陳湘國, 郭哲榮等.WSN RFID物聯(lián)網(wǎng)原理與應(yīng)用.電子工業(yè)出版社.2010: 1-13.

[4]范紅, 馮登國.安全協(xié)議理論與方法.科學(xué)出版社.2003: 47-62.

[5]Klaus Finkenzeller, “RFID Handbook: Fundamentals and Applications in Contactless SmartCards and Identification”, Second Edition Copyright 2003 John Wiley&Sons, Ltd.ISBN: 0-470-84402-7.

[6]Juels A.RFID Security and Privacy: A Research Survey[J].IEEE Journal on Selected Areas in communication, 2006, 24(2): 381-394.

[7]Sarma S, Weis S, Engels D.RFID systems and security and privacy implications[C]PPProe of the 4th Int Workshop on Cryptographic Hardware and Embedded Systems.Berlin: Springer, 2002: 454-469.

[8]Molnar D., Wagner D..Privacy and security in library RFID: Issues, practices, and architectures[C].In: Proceedings of the 1lth ACM Conference on Computer and Communications Security, Washington DC, 2004: 2 10-2 1 9.

[9]Y.C.Lee, Y.C.Hsieh, P.s.You, T.C.Chen.An Improvement on RFID Authentication Protocol with Privacy Protection[C].In: Proceedings of the 3rd International Conference of Convergence and Hybrid Information Technology, ICCIT, 2008: 569-573.

[10]蔡慶玲, 詹宜巨.一種符合EPC C1G2標(biāo)準(zhǔn)的RFID隨機(jī)化密鑰雙向認(rèn)證協(xié)議[J].電信科學(xué) 2007.第4期: 70-74.

[11]李曉東.射頻識別技術(shù)中的隱私安全問題及策略[J].微電子學(xué)與計(jì)算機(jī) 2005.第22卷 第9期: 137-140.

[12]Gwo-ChingChang.A Feasible Security Mechanism For Low Cost RFID Tags[J].IEEE Computer Security.2005.

[13]于宇, 楊玉慶, 閔昊.RFID標(biāo)簽的安全建模及對EPCC1G2協(xié)議的改進(jìn)[J].小型微型計(jì)算機(jī)系統(tǒng)2007年7月.第28卷第7期: 1339-1344.

[14]GongL, Needham, Yahalom R.Reasoning About Belief in Cryptographic Protocols.InProceedings of the 1990 IEEE Computer Society Symposium on Research in Security and Privacy, IEEE Computer SocietyPress, Los Alamitos, California, 1990, 5: 234-248.

A Provably Secure RFID Protocol Based on Static ID Mechanism

XIONG Fei1, CHEN Fang1, ZHOU Hong-xi1, LV Jun-feng1, DANG Yu-jun1, GU Yong-hao2,YU Hua-dong3, XU Chang-fu4, LU Yong-ling4, WANG Peng5
(1.State Grid Information & Telecommunication Branch Company, Beijing 100761, China; 2 Beijing Key Laboratory of Intelligent Telecommunication Software and Multimedia, School of Computer Science, Beijing University of Posts and Telecommunications, Beijing 100876, China; 3.R&D Center of State Grid Information & Telecommunication Group Co., LTD., Beijing 102211, China; 4.Jiangsu Electric Power Company Research Institute, Nanjing City 211103, China; 5.Institute of computing technology, Chinese Academy of Sciences, Beijing 100080, China)

Radio Frequency Identification (RFID) can be used to access into Internet of things in power systems, which it needs a security protocol to meet the requirements of high efficiency, security and low cost.In this paper, a provably secure RFID protocol based on static ID mechanism is proposed in order to solve the existing problem.Compared with the existing schemes, the proposed scheme is provably secure which is based on GNY analysis and proof.

Internet of things in power systems; RFID; Air interface communication; Security protocol; GNY logic analysis

TN914.33

A

10.3969/j.issn.1003-6970.2017.03.001

本文受國網(wǎng)科技項(xiàng)目(SGTYHT/15-JS-191)，國家自然科學(xué)基金資助項(xiàng)目(61173017)、工信部通信軟科學(xué)基金資助項(xiàng)目(2014-R-42，2015-R-29)、信息網(wǎng)絡(luò)安全公安部重點(diǎn)實(shí)驗(yàn)室開放課題基金資助項(xiàng)目(C14613)、面向傳輸網(wǎng)絡(luò)及業(yè)務(wù)網(wǎng)絡(luò)的智能綜合網(wǎng)絡(luò)管理技術(shù)項(xiàng)目支持

熊飛(1983-)，男，高工，博士，無線通信方向；陳芳(1983-)，女，高工，碩士，通信系統(tǒng)運(yùn)維方向；周鴻喜(1975-)，男，高工，碩士，通信傳輸方向。

本文著錄格式：熊飛，陳芳，周鴻喜，等.一種基于靜態(tài)ID機(jī)制可證明安全的RFID協(xié)議[J].軟件，2017，38（3）：01-05