计算机工程与科学2018，Vol.40Issue(12)：2183-2192,10.DOI:10.3969/j.issn.1007-130X.2018.12.012
RFID超轻量级认证协议RCIA形式化分析与改进
Formal analysis and improvement of RCIA:An ultra-lightweight RFID mutual authentication protocol
摘要
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.关键词
RFID/RCIA协议/形式化方法/模型检测/去同步攻击Key words
RFID/RCIA protocol/formal method/model checking/desynchronization attack分类
信息技术与安全科学引用本文复制引用
钟小妹,肖美华,李伟,谌佳,李娅楠..RFID超轻量级认证协议RCIA形式化分析与改进[J].计算机工程与科学,2018,40(12):2183-2192,10.基金项目
国家自然科学基金(61163005,61562026) （61163005,61562026）
江西省主要学科学术与技术带头人项目(2017XSDTR0105) （2017XSDTR0105）
江西省自然科学基金(20161BAB202063) （20161BAB202063）
江西省教育厅科技项目(GJJ170384) （GJJ170384）
