Formal Analysis of the Munilla Authentication Protocol Using ProVerif

RFID (Radio Frequency Identification) technology is widely used in various sectors such as logistics, transportation, and digital payment systems. However, due to its wireless nature, this technology is vulnerable to various security threats, including eavesdropping, message modification, and multiplexing attacks. To address these challenges, Munilla et al. (2020) proposed a 5G-Compliant Authentication Protocol for RFID, which is claimed to be able to withstand passive, active, and replay attacks. However, this claim is based only on informal analysis without formal proof. In this study, a formal analysis of Munilla's protocol was conducted using ProVerif, a symbolic verification tool based on applied pi-calculus used for security protocol analysis. The verification results indicate potential key leaks, message modification, and failure of certain property authentication. To address these weaknesses, an improved scheme is proposed by adding an HMAC function and refining the KSEAF derivation process. The results of the reanalysis using ProVerif indicate that the improved scheme can improve the level of security and resilience to attacks.