Abstract: RFID technology, as the core technology of the Internet of Things, has been widely used in various fields. Currently, RFID systems frequently face security threats, mainly due to the wireless communication used by the readers and tags in RFID systems. RFID security authentication protocols, as an important means to ensure communication security in RFID systems, are crucial for their inherent security. Formal methods have become a major technical approach for enhancing the inherent security of protocols.A general modeling method is proposed for the typical ultralightweight mutual authentication RCIA protocol. Using this method, an SMV (symbolic model verification) model is established for the RCIA protocol, and security property verification is conducted on this model using NuSMV. Experimental results confirm the existence of security flaws in the consistency aspect of the RCIA protocol. Further analysis of the verification results is provided, along with corresponding attack paths for the flaws. A general solution is proposed for this flaw, and its feasibility is evaluated.

Key words: RFID, authentication protocol, model checking, NuSMV, formal verification

摘要： RFID技术作为物联网的核心技术,在各个领域中已被广泛应用.目前RFID系统频繁遭受安全威胁,主要原因在于RFID系统中的读取器和标签使用的是无线通信方式.RFID安全认证协议作为RFID系统通信安全保障的一种重要手段,其内在安全至关重要,同时形式化方法已成为当前提高协议内在安全的一种主要方法.针对典型的超轻量级双向认证RCIA协议,提出了一种通用的建模方法,并采用此方法为RCIA协议建立了SMV模型,通过NuSMV对该模型进行了安全性验证.实验结果确认了RCIA协议在一致性方面存在安全缺陷,进一步分析验证结果,并提供了缺陷相应的攻击路径.针对该缺陷,提出了一个通用的解决方案,并评估了其可行性.

关键词: RFID, 认证协议, 模型检测, NuSMV, 形式化验证