Formal Analysis of Ratchet Protocols Based on Logic of Events
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 communicati...
Salvato in:
| Autori principali: | , , , , , |
|---|---|
| Natura: | Articolo |
| Lingua: | inglese |
| Pubblicazione: |
MDPI AG
2025-06-01
|
| Serie: | Applied Sciences |
| Soggetti: | |
| Accesso online: | https://www.mdpi.com/2076-3417/15/13/6964 |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| Riassunto: | 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. |
|---|---|
| ISSN: | 2076-3417 |