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

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

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

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

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

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

電力物聯網；RFID；空口通信；安全協議；GNY邏輯分析

0 引言

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

2 研究現狀

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

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

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

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

3.1 協議描述

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

各部分數據存儲情況如下：

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

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

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

表1 符號說明Table 1 Symbols

協議描述如下：

Step 1：Challenge

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

Step 2：T-R Response

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

Step 3：R-B Response

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

Step 4：B-R Reply

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

圖1 基于靜態(tài)ID機制可證明安全的RFID協議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會將儲存的隨機數Rr的第n+1部分與自身的ID做H()運算，然后所得的值與接收到的H(ID//Rrn+1)匹配；匹配通過則停止發(fā)送信號。

3.2 協議安全性分析

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

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

3.3 協議的GNY邏輯分析與證明

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

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的內容和格式識別X。

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

10.P|?CP對X有管轄權。

3.3.2 對基于分組隨機數的安全協議的 GNY邏輯證明

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

（1）協議邏輯化

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

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

（2）要證明的問題

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

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

Q[2]T|≡|B～#（H（ID//Rr n+1）） 標簽確認是來自于后臺數據庫新鮮的信息。

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

（3）初始假設

①對Tag的假設

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

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

Tag[3]Tag 相信隨機數 Rr是新鮮的: T|≡#（Rr）

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

②對Reader的假設

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

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

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

③對Back-End BD的假設

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

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

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

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

BD[6]BD 擁有所有 ID 對應的 DATA: B?DATA

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

（4）對Q[1]的證明

（5）對Q[2]的證明

通過 GNY邏輯我們證明了本協議能夠達到實現安全認證和數據傳輸的功能，但是我們注意到，在初始假設中XT，并沒有在后面證明中用到，也就是說在實現安全認證和數據傳輸時并沒有用到這個值，它對于認證過程是一個冗余量，但是在前面對XT進行解釋時說明了這個量是為了使得后臺數據庫運算復雜度降低，也就是說對于安全認證這一過程，XT是沒有作用的，但是對于優(yōu)化整個安全認證協議還是有重要作用的。這說明GNY邏輯可以檢測出協議中存在的冗余。

4 結語

本文提出了一種基于靜態(tài) ID機制可證明安全的RFID協議，將其與其他靜態(tài)ID機制的RFID安全協議在抵御攻擊方面進行比較，然后通過 GNY形式化驗證了本協議，證明了本協議能夠實現安全認證和數據傳輸的功能。

參考文獻

[1]周永彬, 馮登國.RFID安全協議的設計與分析[J].計算機軟件學報, 2006, 29(4): 581-589.

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

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

[4]范紅, 馮登國.安全協議理論與方法.科學出版社.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標準的RFID隨機化密鑰雙向認證協議[J].電信科學 2007.第4期: 70-74.

[11]李曉東.射頻識別技術中的隱私安全問題及策略[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標簽的安全建模及對EPCC1G2協議的改進[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

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

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

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