Security protocols are the basis of modern network communication, proving that the security problem of protocols is one of the hot research topics today. The data in industrial IoT are usually transmitted through insecure channels, which brings certain security risks. The Logic of Events is a formal method for proving the security properties of protocols based on event systems. The new theoretical extension is based on the Logic of Events theory, which proposes new event classes Compurte, TimeGap, Construct, and Reconstruct and an axiom AxiomRe and related inference rules for malicious attacks and security privacy issues in emerging protocols, as well as extending the matching descriptions of protocol behaviours in complex cryptographic algorithms and information sharing techniques for applications for the formal analysis of authentication protocols for the Industrial Internet of Things. Finally, formal analysis is carried out using the example of a secure multi-factor authentication protocol for the industrial IoT, which proves the security of the protocol.
Radio frequency identification (RFID) is a crucial component of the Internet of Things (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 commercialisation and large-scale deployment of RFID systems has raised a number of security-related issues that suggest the need for security protocols. Logic of events theory (LoET) is a formal method for constructing and reasoning about distributed systems and protocols involving security concepts. 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 and formally institute the authentication process of both parties, and the ex-tended LoET is used to analyse the security properties of ECC-based RFID security protocols. Under reasonable assumptions, an ECC-based RFID mutual authentication scheme is shown to satisfy the strong mutual authentication feature. It is shown that extended logic of events theory may be used to prove the security properties of this class of ECC-based RFID protocols.
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.