# Formal Analysis of Ratchet Protocols Based on Logic of Events
## 2 Logic of Events Theory
### Fundamental Concepts
#### 2.3.2 Related Axiomatic Extension  
In the Logic of Events, the causal axioms include the Receive Axiom (_AxiomR_), the Verify Axiom (_AxiomV_), and the Decrypt Axiom (_AxiomD_). These three axioms associate the event classes _Rcv_, _Verify_, and _Decrypt_ with their causally related counterparts _Send_, _Sign_, and _Encrypt_, respectively. Among them, _AxiomR_ and _AxiomV_ are structurally similar, both describing the matchability of protocol behaviors--that is, any receive event or signature verification event must be preceded by a corresponding send or signing event, with identical message content. _AxiomD_ introduces the element of the key, asserting that the decryption event corresponds to an encryption event with both matching content and matching key. The formal definitions are as follows:  
\[\left\{\begin{array}{c}\mathit{AxiomR}:\forall e:E(\mathit{Rcv})\;\exists e^ {\prime}:E(\mathit{Send}).(e^{\prime}<e)\wedge\mathit{Rcv}(e)=\mathit{Send}(e ^{\prime})\\ \mathit{AxiomV}:\forall e:E(\mathit{Verify})\;\exists e^{\prime}:E(\mathit{ Sign}).(e^{\prime}<e)\wedge\mathit{Verify}(e)=\mathit{Sign}(e^{\prime})\\ \mathit{AxiomD}:\forall e:E(\mathit{Decrypt})\;\exists e^{\prime}:E( \mathit{Encrypt}).e^{\prime}<e\wedge\mathit{DEMatch}(e,e^{\prime})\\ \mathit{DEMatch}(e,e^{\prime})\equiv_{\mathit{dof}}\mathit{ plaintext}(e)=\mathit{ plaintext}(e^{\prime})\wedge\\ \mathit{ciphertext}(e)=\mathit{ciphertext}(e^{\prime})\wedge\mathit{ MatchingKeys}(\mathit{key}(e),\mathit{key}(e^{\prime}))\end{array}\right\} \tag{10}\]  
To introduce \(\mathit{DH}\) and _ratchet_ events, the causal axiom needs to be extended. The extended axiom is denoted as _AxiomE_. It stipulates that, in the sequence of these two types of events, a corresponding \(\mathit{DH}\) event must occur before the _ratchet_ event. The two events are causally related and share relevant information content. In addition, the keys involved must also be match-associated. The formal definition of _AxiomE_ is given as follows:  
\[\left\{\begin{array}{c}\mathit{AxiomE}:\forall e:E(\mathit{Ratchet})\;\exists e ^{\prime}:E(\mathit{DH}).(e^{\prime}<e)\wedge\mathit{Ratchet}(e)=\mathit{DH}(e ^{\prime})\wedge\\ \mathit{RDMatch}(e,e^{\prime})\equiv_{\mathit{dof}}\mathit{ plaintext}(e)=\mathit{ plaintext}(e^{\prime})\wedge\\ \mathit{ciphertext}(e)=\mathit{ciphertext}(e^{\prime})\wedge\mathit{ MatchingKeys}(\mathit{key}(e),\mathit{key}(e^{\prime}))\end{array}\right\} \tag{11}\]  
To ensure the soundness of _AxiomE_, we clarify that the relation _RDMatch(e, e')_--which links a _ratchet_ event to a prior \(\mathit{DH}\) event--is assumed to be injective. That is, for every ratchet event, there exists at most one \(\mathit{DH}\) event such that _RDMatch_ holds. This uniqueness is guaranteed by the local causal ordering in LoET and the protocol design of Signal, where each \(DH\) operation generates a fresh ephemeral key used exactly once. Therefore, ambiguity is avoided even in long sessions.  
In asynchronous environments such as message delay, loss, or replay, _RDMatch_ remains valid based on symbolic causality. A _ratchet_ event must be causally linked to a verifiable prior \(DH\) event. Messages that lack this linkage are considered invalid and excluded from the protocol trace, thus ensuring the correctness of _AxiomE_ even under adversarial or unreliable conditions.