Formal Verification of an RFID Authentication Protocol Based on Hash Function and Secret Code

Radio frequency identification (RFID) systems have recently been in wide use across industries. RFID systems are characterized by the wireless data communication between readers and tags. Accordingly, the very wireless communication is vulnerable to security issues and likely to become a target of intrusion (Khor in Wirel Pers Commun 59(1): 17–26, 2011, Habibi and Aref in Wirel Pers Commun 69(4): 1583–1596, 2013). Regarding RFID security issues, many studies have dealt with a range of protocols. A range of security protocols including hash-locking and that suggested by Kenji et al. have been proposed in the form of theorem proving, but found over time by many scholars to have security vulnerabilities. The present study experimentally applied formal specification techniques to hash-locking and Kenji et al.’s protocols and verified their vulnerabilities. The security vulnerabilities of the proposed protocols can hardly be found with theorem proving. Protocols proposed based on theorem proving are often found to have unexpected vulnerabilities by other investigators. Also, many of those protocols are applied to real systems without precise understanding of what their investigators suggest and often implemented after many trials and errors. Hence, it is a very important issue to develop some techniques capable of analyzing vulnerabilities at earlier stages of initial design via automated verification methods. As a means of solving the security issues relevant to RFID systems, the present study verifies the protocols using formalization tools and proposes an RFID security protocol based on hash locks, public keys and secret keys. The proposed protocol designed to have no security vulnerabilities does not require unnecessary calculations and meets the formal verification, i.e. safety verification, deadlock verification and livelock verification. To develop and verify a secure protocol, the present study uses Casper and Failure Divergence Refinements (FDR) tools and confirms the proposed protocol is safe and secure. With the verification of security, \(\hbox {P}\,\sqsubseteq \,\hbox {TQ}\,\triangleq \) traces(Q) \(\subseteq \) traces(P) was found to be met. Similarly, with the verification of deadlock, \(\hbox {P}\,\sqsubseteq \,\hbox {FQ}\,\triangleq \) failures(Q) \(\subseteq \) failures(P) was confirmed. Finally, with the verification of live-lock, the fail/branch model of the process proved to be in deadlock and live-lock. Also, P \(\sqsubseteq \) FDQ \(\triangleq \) failures(Q) \(\subseteq \) failures(P) \(\wedge \)divergences(Q) \(\subseteq \) divergences(P) was confirmed and found secure based on the FDR verification results. These findings indicate that the proposed protocol is applicable to RFID wireless security systems, meets the security requirements, facilitates implementation of secure systems and is usable for a range of application techniques.