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

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