# Formal Analysis of Ratchet Protocols Based on Logic of Events
## 1 Introduction  
Ratchet protocols are a class of security protocols designed to enhance communication security [1]. The core principle of the ratchet mechanism lies in dynamically updating keys to achieve forward secrecy [2, 3] and backward secrecy [4]. It is widely adopted in instant messaging [5] (for example, Signal protocol, WhatsApp [6]), end-to-end encryption (E2 EE) [7, 8], and key exchange [9], among other domains. For example, Signal [10] provides E2 EE for numerous instant messaging platforms such as WhatsApp, Wire, and Facebook Messenger, serving over 1 billion active users. In the midst of growing concerns about communication privacy breaches [11], the Signal protocol leverages X3 DH (Extended Triple Diffie-Hellman) [12] and the double ratchet encryption technique [13] to provide robust security properties. These mechanisms ensure that even if a key is compromised, past and future messages remain protected. Off-the-Record (OTR) [14] was one of the earliest secure messaging protocols. It employs a Diffie-Hellman ratchet, generating a new ephemeral shared key with each message exchange. Since past messages cannot be decrypted from subsequent states, this technique is referred to as a ratchet mechanism. Ratchet protocols are broadly categorized into unidirectional (single) and bidirectional (double) ratchets [15]. A unidirectional ratchet--such asthe KDF-based ratchet [16]--updates keys in only one direction. In contrast, a bidirectional ratchet combines a KDF ratchet and a Diffie-Hellman ratchet to achieve both forward and backward secrecy, thereby offering stronger security guarantees.The evolution of ratchet structures has been complex. For instance, TextSecure [17], the predecessor of Signal, was the first to formalize the double ratchet mechanism by integrating both a symmetric-key ratchet and an asymmetric Diffie-Hellman ratchet. a In recent years, the security of ratchet protocols and their associated mechanisms has been extensively studied. [PERSON] et al. [18] conducted a security analysis of TextSecure v3, demonstrating that, in their model, the long-term symmetric keys used to initialize the ratchet mechanism form a secure one-round key exchange protocol. However, their analysis did not address the security properties of the ratchet mechanism itself. [PERSON] et al. [19] proposed a formal security analysis framework capable of capturing ratchet structures. Building on this, they introduced the asynchronous ratcheting tree (ART) design method to achieve stronger security guarantees. Meanwhile, [PERSON] et al. [20] formally defined security properties for ratchet mechanisms and presented a provably secure ratcheted key exchange protocol, demonstrating how to model the characteristics of ratchet encryption.Further advancing the field, [PERSON] et al. [21] employed the Tamarin prover to formally model and verify the Signal protocol, including its ratchet-based components. Additionally, [PERSON] et al. [22] developed a formal security analysis of the Signal protocol using Logic of Events theory, providing rigorous proofs for the security of its ratchet mechanism. These studies have provided in-depth analyses and improvements of ratchet protocols and their associated mechanisms from various angles, including key exchange, ratchet operations, and formal verification [23; 24]. Collectively, they have laid a solid theoretical foundation for ensuring the security and robustness of ratchet-based communication protocols. Logic of Events theory (LoET) [25; 26] is a theorem-proving approach frequently employed for analyzing the security of distributed systems. In response to the limitations of Protocol Composition Logic (PCL) [27], [PERSON] et al. made significant theoretical advancements by applying LoET to security protocol analysis. Their work substantially expanded the theoretical framework of LoET, enabling it to support the formal verification of security protocols across multiple domains.