Formal analysis of ECC-based RFID authentication protocol in logic of events theory

Today, the rapid development of the Internet of Things (IoT) has greatly affected human life, and the security analysis of authentication protocols in IoT is increasingly important. Radio Frequency Identification (RFID) is a crucial component of IoT, and RFID using Elliptic Curve Cryptography (ECC) is a public key cryptosystem authentication approach that tackles the problem of electronic tag data encryption in RFID systems. The formal method is one of the most powerful ways for verifying protocol security, and the Logic of Events Theory (LoET) is a theorem-proving formal logic for analyzing distributed system security. This paper proposes three event classes, Compute, Retrieve, and Generate, and related axioms and inference rules to formally abstract the ECC session key generation function, formally statute the authentication process of both parties, and the extended LoET is used to analyze the security properties of ECC-based RFID security protocols. Under reasonable assumptions, an ECC-based RFID two-way authentication scheme is shown to satisfy the two-way strong authentication feature. It is shown that the extended logic of event theory may be used to prove the security properties of this class of ECC-based RFID protocols.