• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

计算机工程与科学

• 计算机网络与信息安全 • 上一篇    下一篇

RFID超轻量级认证协议RCIA形式化分析与改进

钟小妹,肖美华,李伟,谌佳,李娅楠   

  1. (华东交通大学软件学院,江西 南昌 330013)
  • 收稿日期:2018-06-15 修回日期:2018-08-24 出版日期:2018-12-25 发布日期:2018-12-25
  • 基金资助:

    国家自然科学基金(61163005,61562026);江西省主要学科学术与技术带头人项目(2017XSDTR0105);江西省自然科学基金(20161BAB202063);江西省教育厅科技项目(GJJ170384)

Formal analysis and improvement of RCIA:
An ultra-lightweight RFID- mutual authentication protocol

ZHONG Xiaomei,XIAO Meihua,LI Wei,CHEN Jia,LI Yanan   

  1. (School of Software,East China Jiaotong University,Nanchang 330013,China)
  • Received:2018-06-15 Revised:2018-08-24 Online:2018-12-25 Published:2018-12-25

摘要:

无线射频识别(RFID)是物联网中的一种非接触式的自动识别技术,被广泛运用于构建物物互联的RFID系统。RCIA是一种超轻量级RFID双向认证协议,提供高安全性并声称能抵御去同步攻击。形式化方法是安全协议分析的有力手段。运用模型检测工具SPIN对RCIA协议的认证性及一致性进行验证,结果表明RCIA协议存在去同步攻击漏洞。针对此漏洞,提出基于密钥同步机制的修补方案,对RCIA协议进行了改进。对改进后的协议进行形式化分析与验证,结果表明改进后的RCIA协议具有更高的安全性。提出的协议抽象建模方法对此类超轻量级RFID双向认证协议形式化分析具有重要借鉴意义;提出的基于密钥同步机制的漏洞修补方案,被证明能有效抵御去同步漏洞,可适用于此类超轻量级RFID双向认证协议的设计和分析。
 

关键词: RFID, RCIA协议, 形式化方法, 模型检测, 去同步攻击

Abstract:

Radio frequency identification (RFID) is a noncontact automatic identification technology in the Internet of things. It is widely used in the construction of RFID system for the interconnection of things. RCIA is an ultralightweight RFID mutual authentication protocol (UMAP), which provides high security and claims to be resistant to desynchronization attack. Formal method is a powerful tool to analyze the security of cryptographic protocols. We analyze the RFID tag authentication protocol RCIA based on formal method. Model checker SPIN is used to verify the authenticity and consistency of the RCIA protocol. The results show that the RCIA protocol is vulnerable to synchronization attack, for which we propose a patching scheme based on the key synchronization mechanism to improve the protocol. Formal analysis and verification results of the improved protocol show that the improved RCIA protocol has higher security. An abstract protocol modeling method we proposed in this paper is used to build an abstract protocol model of RCIA protocol formally, which has important reference for the formal analysis of such ultralightweight RFID mutual authentication protocol. The proposed vulnerability patching scheme based on key synchronization is proved to be effective against desynchronization attack, and it can be applied to the design and analysis of such ultralightweight RFID mutual authentication protocol.
 

Key words: RFID, RCIA protocol, formal method, model checking, desynchronization attack