The Signal is an end-to-end encrypted communication protocol composed of a double ratchet (DR) protocol and an extended triple Diffie-Hellman (X3DH) protocol. Its complex ratchet structure and the characteristics of protocol composition make it challenging to realize formal analysis. A formal analysis method based on logic of events theory (LoET) is proposed to conduct a security analysis of the Signal protocol. The method includes inference rules with key relation and key chain as the core to realize the formal analysis of ratchet structure, and the inference relation between sub-protocols is established by putting forward the composition theorem. The proposed method achieves a formal analysis of Signal, revealing that it does not satisfy a strong authentication property during the X3DH phase. The results show that the LoET-based method can be effectively applied in the formal analysis of Signal protocols, thus promoting the application and development of these protocols with ratchet structure and composition properties.

The development of smart contracts remains in its early stages, with significant differences in underlying programming languages and application platforms resulting in a lack of standardization. This lack of standardization increases the susceptibility to vulnerabilities and associated financial losses. To address security vulnerabilities in smart contracts on the Ethereum blockchain platform, this paper proposes a security audit method based on formal verification. The method integrates an input module, static analysis module, formal verification module, analog execution module, and report and recommendation module, which can accurately discover the security vulnerabilities and logical flaws of smart contracts through formal verification and other analysis techniques, thus realizing correctness detection. During the experiment, the method detects 8 types of common vulnerabilities in 148 smart contracts and marks 21 smart contracts with vulnerabilities. After manual review and analysis, it is found that 17 of these 21 marked smart contracts do have security vulnerabilities. The experimental results show that the proposed method can accurately detect security vulnerabilities and logic flaws in smart contracts through formal verification and other analysis techniques before smart contracts are deployed, thus significantly improving the security of smart contracts and reducing the economic losses that may be caused by code defects.

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.

Security analysis of composite protocols is a critical issue in the field of network security. In complex network environments, the traditional approach of analyzing a single protocol becomes inadequate when dealing with scenarios involving multiple interactions and combinations of protocols. To address this challenge, this paper extends the Logic of Events Theory (LoET) and proposes a method for proving the security of composite protocols. Building upon the Logic of Events Theory, we introduce sequential composition rules, ordering rules, and relevant axioms. We incorporate the concept of invariants and formally abstract the DTLS-SRTP protocol, thereby verifying the mutual authentication and confidentiality of the two sub-protocols. In conclusion, our study demonstrates that the extended Logic of Events Theory offers an effective means of verifying the security of composite protocols.