Formal Analysis of Ratchet Protocols Based on Logic of Events

Authors:
Open Access
Publisher website
Google Scholar
Abstract
Ratchet protocols are a class of secure protocols based on ratcheting encryption mechanisms, widely employed in instant messaging. Against the backdrop of frequent incidents of communication privacy breaches, ratchet protocols have become a vital technology for ensuring secure end-to-end communication. This paper presents a formal analysis framework for ratchet protocols grounded in Logic of Events theory (LoET). We further extend LoET by introducing dedicated Diffie–Hellman (DH) and ratchet event classes, along with tailored axioms and inference rules, to support precise modeling of ratcheted encryption. Using the Signal protocol as a case study, we construct a bidirectional authentication model and rigorously prove that both its symmetric and asymmetric ratchet phases satisfy strong authentication properties. Compared with existing formal approaches, our method enables more expressive modeling of key update sequences and supports structured reasoning over causality and authentication flows. The proposed framework lays a theoretical foundation for analyzing the security of modern ratcheted protocols and holds potential for future automated verification.
Funding Information
  • National Natural Science Foundation of China (62362033, 61962020, jxsq2023201009, 20224ACB202006, 20244BCE52146)
  • Double Thousand Talent Plan of Jiangxi Province (62362033, 61962020, jxsq2023201009, 20224ACB202006, 20244BCE52146)
  • Natural Science Foundation of Jiangxi Province (62362033, 61962020, jxsq2023201009, 20224ACB202006, 20244BCE52146)
  • Jiangxi Province Early Career Youth Science and Technology Talent Training Special Project (62362033, 61962020, jxsq2023201009, 20224ACB202006, 20244BCE52146)

This publication has 23 references indexed in Scilit: