# Formal Analysis of Ratchet Protocols Based on Logic of Events
## 1 Introduction
These innovations have reinforced LoET's influence in formal methods research while providing a powerful analytical tool for verifying the security of complex systems. LoET employs events to characterize system behaviors and security properties. By formally modeling protocol executions or specifying desired security goals, LoET enables rigorous verification of whether these properties hold within the protocol model. This approach offers unique advantages in detecting subtle vulnerabilities that may be overlooked by other analysis methods. In this study, we conduct a formal analysis of the ratchet mechanism in the Signal protocol to identify potential vulnerabilities and ensure the security of Signal message exchanges. Our principal contributions are as follows:  
1. A formal analysis framework for ratchet protocols based on LoET. We extend the LoET event class system by introducing DH (Diffie-Hellman) and ratchet event classes and by developing dedicated axioms and inference rules tailored to the characteristics of ratchet protocols. This framework addresses the limitations of conventional formal methods in accurately modeling ratchet-based encryption mechanisms. 2. Construction of a bidirectional authentication formal model for the Signal protocol. To capture the dynamic nature of ratchet encryption, we abstract its key negotiation and update processes. By integrating LoET, we formally define the security propertiesof protocol interactions, precisely characterizing the requirements for bidirectional authentication. 3. Formal verification of strong authentication properties in the Signal protocol. Leveraging our extended LoET rules, we rigorously prove the strong authentication properties of the ratchet mechanism in message exchange scenarios. This work also extends the applicability of LoET to the analysis of ratchet protocols. The remainder of this paper is organized as follows: Section 2 introduces the Logic of Events theory (LoET) and its extensions developed for the formal analysis of ratchet protocols. Section 3 presents a formal analysis of the Signal protocol, including an overview of the protocol and its formal verification framework, followed by a detailed exposition and proof of its strong authentication properties based on LoET. Section 4 presents a comparison between our approach and existing methods. Section 5 summarizes the main conclusions of this study and offers suggestions for future research directions. In addition, several studies have conducted formal verification of the Signal protocol in depth. Tools such as CryptoVerif [28] and Verifpal [29], provide automated protocol analysis capabilities, enabling the modeling of complex cryptographic mechanisms and potential attack vectors. These tools are particularly well-suited for evaluating the security of ratchet-based protocols like Signal. Furthermore, closely related to our work, OSM [30] proposes a model-checking framework based on structured event tracing, which allows for dynamic observation of protocol behavior in aspect-oriented programming systems. This approach aligns well with the event-driven modeling strategy employed by LoET. Additionally, BlockASP [31] extends model-checking techniques for security protocols by emphasizing semantic cleanliness, which plays a critical role in verifying the security of key materials and the integrity of protocol state transitions. These frameworks complement our approach and highlight the broader applicability of event-based formal verification.