# Formal Analysis of Ratchet Protocols Based on Logic of Events
## 5 Conclusions  
This paper proposes a formal analysis framework for ratchet protocols based on LoET, introducing dedicated axioms and rules tailored to the characteristics of ratchet protocols. It addresses the modeling limitations of traditional formal methods in capturing ratchet encryption mechanisms. Using the Signal protocol as a case study, we construct a bidirectional authentication model for ratchet encryption that precisely captures the security properties required for mutual authentication. We also complete a formal verification of Signal's strong authentication properties, thereby extending the applicability of LoET to the analysis of ratchet protocols. This work not only provides a theoretical security guarantee for the Signal protocol at a foundational level but also establishes a reusable methodology for the formal verification of similar secure communication protocols. Building upon the formal security guarantees established in our current model, future work will focus on bridging the gap between theoretical verification and real-world deployment, aiming to promote the practical adoption of formal protocol models in engineering contexts. To further enhance protocol security under real operational conditions, we plan to conduct in-depth research on implementation-level formal verification, including security property validation at the code level, consistency checking between implementations and formal specifications, and security evaluation within execution environments. These efforts aim to establish a complete verification chain spanning from theoretical modeling to engineering practice. Specifically, our planned directions include: (1) developing a prototype tool capable of parsing protocol communication logs and automatically generating corresponding LoET event models; (2) extending the LoET framework to support group communication and dynamic participant management, while exploring integration with the ART model for hybrid verification; (3) enhancing the framework's ability to capture asynchronous communication scenarios, such as message loss and reordering; and (4) extracting event traces from real-world protocol logs (e.g., Wire, WhatsApp) and validating their conformance to the formal model's causal dependencies and authentication semantics. Collectively, these efforts will further advance the applicability of the LoET framework in diverse communication protocols and provide systematic support for the verifiable design and implementation of secure protocols. \begin{table}
\begin{tabular}{c c c c} \hline \hline
**Reference** & **Research Method** & **Analysis of Ratchet** & **Verification Efficiency** \\ \hline \multirow{3}{*}{Ref. [20]} & \multirow{3}{*}{Syntax for ratcheted encryption} & \multirow{3}{*}{Models unidirectional ratchet; does not capture Signal’s double ratchet logic.} & \(\times\) & \(\big{\}}\) \\  & & & & \\  & & & & \\  & & & & \\ \hline \multirow{3}{*}{Ref. [21]} & \multirow{3}{*}{Tamarin} & \multirow{3}{*}{Automates partial proofs; lacks native support for causality or bidirectional authentication semantics.} & \(\times\) & \(\big{\}}\) \\  & & & & \\ \cline{1-1}  & & & & \\ \cline{1-1}  & & & & \\ \hline \multirow{3}{*}{Ref. [22]} & \multirow{3}{*}{Original LoET} & \multirow{3}{*}{Early LoET use; no AxiomE/Clean support; only basic match rules used.} & \(\times\) & Coarse-grained modeling; fewer verification steps and weak completeness; lacks Clean and AxiomE support; incomplete reasoning paths \\ \hline \hline \end{tabular}
\end{table} 
Table 3: _Cont._  
**Author Contributions:** Conceptualization, M.X. and Z.L. ; methodology, H.W. ; formal analysis, H.W. ; Investigation, H.F. and H.S. ; writing--original draft preparation, H.W. ; writing--review and editing, M.X. and Z.L. ; visualization, H.W. ; supervision, Z.L. and K.Y. ; All authors have read and agreed to the published version of the manuscript. **Funding:** This research was funded by the National Natural Science Foundation of China (No. 62362033, 61962020), Double Thousand Talent Plan of Jiangxi Province (No.