Formal Verification of Cryptographic Protocol for Secure RFID System

RFID technology has become one of the most hotly debated ubiquitous computing technologies, and public fears of its alleged capability for comprehensive surveillance have prompted a flurry of research trying to alleviate such concerns. Security mechanisms for RFID systems are therefore of utmost important. In this paper, we describe problems of previous work on RFID security protocols and specify several known attacks with Casper (A Compiler of Security Protocol Analyzer), then verify their security properties such as secrecy and authentication using the FDR (Failure Divergence Refinement) model checking tool. Finally, we discuss practical issue of the hash authentication RFID security protocol, which guarantee data privacy and authentication between a tag and a reader using Casper and FDR.