# Formal Analysis of Ratchet Protocols Based on Logic of Events
## 4 Comparison  
[PERSON] et al. [18] proved that the ratchet module of the TextSecure protocol is secure by analyzing the source code of TextSecure v3. However, the composite security of interactions between modules remains unverified. [PERSON] et al. [19] proposed ART (asynchronous ratcheting trees) to achieve stronger security properties, constructing a game-based computational security model to analyze the protocol. Their performance evaluation showed that while ART introduces innovative ratcheting for asynchronous group messaging, it suffers from limitations in computational complexity, synchronization issues, and dynamic group support, which affect the protocol's performance and scalability. [PERSON] et al. [20] demonstrated how to formalize ratchet encryption by defining syntax for ratcheted encryption and key exchange, although their model only captures unidirectional ratcheting (sender-side key updates) and does not extend to bidirectional mechanisms such as Signal's double ratchet algorithm. [PERSON] et al. [21] employed the Tamarin tool for formal modeling and verification of Signal's ratchet protocol, where automated verification relies on explicit security assumptions. However, Tamarin faces limitations in formalizing ratchet processes and integrating them into broader verification procedures. Compared with the prior works [19; 22], this paper introduces several key innovations. In contrast to [19], which proposes the Asynchronous Ratcheting Tree (ART) model focusing on group messaging, our method focuses on formal verification of pairwise ratchet-based protocols, specifically the double ratchet mechanism used in Signal. Rather than employing game-based computational models, we construct a logical model in the Logic of Events (LoET) framework, allowing for deductive proofs of authentication properties. Compared with [22], our work is the first to extend LoET by introducing two new event classes: DH (Diffie-Hellman operations) and _ratchet_ (state update operations). We also add new causal axioms and matching rules (e.g., _AxiomE_, _Rule1-3_), enabling modeling of dynamic key evolution. While our primary demonstration uses the Signal protocol, the extended LoET framework is designed to be protocol-agnostic. It can potentially analyze other ratcheting protocols like MLS, but current limitations include lack of automation and scalability for large protocol families. Unlike Tamarin [21], which supports automated security analysis, it relies on complex user-defined lemmas and does not naturally express bidirectional authentication constraints or temporally structured event matching. In contrast, our approach based on LoET employs explicit causal semantics, enabling clear modeling of the evolution of keys and messages, as well as the logical binding between authentication properties and their cryptographic dependencies. To demonstrate the advantages and necessity of our model, we provide a vulnerability scenario. If _AxiomE_--the rule that links Diffie-Hellman (DH) and ratchet event chains--is disabled or bypassed, an attacker can inject a forged public key into the communication sequence. This breaks the causal continuity between key derivation steps. Under a false assumption, the receiver may derive an incorrect session key, which ultimately results in impersonation. In this case, the protocol loses its strong authentication guarantees. Our model can formally detect such violations through the failure of the _Clean_ predicate. In Appendix A, we provide a simplified attack example to illustrate how the omission of a critical logical rule can directly lead to protocol failure. Meanwhile, we further compare the Tamarin and ART frameworks through a systematic evaluation. The results demonstrate that LoET offers clear advantages in terms of modeling clarity, expressiveness of authentication properties, and verification efficiency. Compared with the above methods, LoET offers distinct advantages in verifying the security of ratchet protocols.