Proving Mutual Authentication Property of RCIA Protocol in RFID Based on Logic of Events

The increasing commercialization and massive deployment of radio frequency identification (RFID) systems has raised many security related issues which in return evokes the need of security protocols. Logic of events theory (LoET) is a formal method for constructing and reasoning about distributed systems and protocols that involve concepts of security. We propose fresh ciphertext and ciphertext release lemmas to extend LoET for analyzing and proving the security of authentication protocols that use symmetric key cryptography more than just digital signature. Based on the extended LoET we formally analyze and prove the authentication property of RCIA protocol, which provides mutual authentication between Tag and Reader in RFID system. Our proof approach based on extended LoET could be applied to the design and analysis of such ultralightweight RFID mutual authentication protocols.