# Formal Analysis of Ratchet Protocols Based on Logic of Events
## 3 Formal Analysis of the Signal Protocol
### Formal Verification of Strong Authentication Properties
#### 3.3.4 Computational Complexity and Scalability  
LoET has strong expressive power, but its current verification process requires manual reasoning steps. When applied to protocols with high state complexity or multiple participants, it may become operationally burdensome. We estimate that the verification of event sequences during each ratchet update round remains linearly tractable, assuming the number of events per round is bounded.  
**Time Complexity.** A typical ratchet round includes one Diffie-Hellman key exchange (two events), one symmetric key derivation (one event), one encryption (one event), and one send/receive pair (two events), totaling approximately six events. Given \(R\) ratchet rounds and \(M\) messages per round, the number of causal relations to be verified is approximately \(\mathcal{O}(R\times M)\). Since each verification step (based on key and message matching) is a constant-time operation, the overall time complexity is \(\mathcal{O}(R\times M)\).  
**Space Complexity.** The LoET framework must store each event along with its metadata (e.g., position, message content, associated keys). If the total number of events is \(N=R\times M\), and each event occupies constant space, then the overall space complexity is \(\mathcal{O}(N)\). When constructing the flow relation (i.e., the causal graph among events), the worst-case complexity may reach \(\mathcal{O}(N\log N)\), depending on the branching structure of the protocol.  
**Scalability.** The current LoET framework is mainly designed for two-party interaction modeling but can be extended to multi-party protocols (e.g., group messaging). Preliminary analysis suggests that with \(P\) participants and \(R\) rounds of group communication, the total number of events could reach \(\mathcal{O}(P\times R\times M)\), and the size of the causal graph may grow to \(\mathcal{O}(P^{2}\times R\times M)\). In such cases, identity binding and message routing ambiguity significantly increase, placing greater demands on the modeling of the _Clean_ predicate and _AxiomE_ rule.  
These scalability constraints further underscore the importance of understanding how LoET captures core security guarantees such as forward and backward secrecy across diverse communication scenarios.  
**Forward secrecy** is ensured by the unidirectional flow from \(DH\) to _Ratchet_ events, making prior keys irrecoverable even if a later key is compromised. This is formally modeled in LoET by the causal dependency chain \(DH\to Ratchet\to Encrypt\). The _Clean_ predicate ensures that any decryption event is based only on fresh keys derived through legitimate DH and ratchet steps, preventing key reuse or rollback attacks. **Backward secrecy** is achieved through periodic \(DH\) key refresh and use of ephemeral keys. In LoET, this is captured via the _New_ event (nonce/fresh key generation), which is causally linked to each _ratchet_ event. Even if a previous key is compromised, it does not allow the decryption of future messages due to the causal isolation enforced by _AxiomE_ and _Rule3_. Practically, this allows protocol designers to assess the temporal granularity of key update strategies and understand the trade-off between security and performance. Our model thus offers both formal guarantees and actionable design insights for protocol hardening.