Paper 2026/1912 Original: eprint.iacr.org/2026/1912 ↗
Secrecy in Squirrel and the Post-Compromise Security of a Ratchet
Abstract
Ratchets are critical cryptographic protocols deployed in many secure messaging applications such as Signal Messenger, WhatsApp, and Apple's iMessage PQ3, which aim for strong guarantees such as Post-Compromise Security (PCS). Computer-aided cryptography can be used to increase confidence in security protocols but, until now, has been unable to prove PCS in the computational model for a ratchet due to the complexity of the cryptographic arguments involved. Existing mechanized PCS analyses have been limited to the symbolic model. We tackle this problem with Squirrel, which is well-suited to study such stateful protocols. The task is still a challenge, due to the intricate reasoning required, and because Sqirrel's indirect modeling of secrecy has difficulties in scaling to such a complex proof. To address these issues, we develop a novel logical framework in Squirrel that allows to reason on secrecy as a first-class notion, and we validate our approach by verifying the PCS of an asymmetric ratchet. This provides the first mechanized computational proof of PCS to date for a ratchet, and possibly for any protocol.
Metadata
- Available format(s)
PDF- Category
- Cryptographic protocols
- Publication info
- Preprint.
- History
- 2026-09-07: last updated
- 2026-09-07: published
- Short URL
- https://ia.cr/2026/1912
- License
- https://creativecommons.org/licenses/by/4.0/
BibTeX
@misc{cryptoeprint:2026/1912,
author = {Clément Hérouard and Charlie Jacomme and Adrien Koutsos and Joseph Lallemand},
title = {Secrecy in Squirrel and the Post-Compromise Security of a Ratchet},
howpublished = {Cryptology {ePrint} Archive, Paper 2026/1912},
year = {2026},
url = {https://eprint.iacr.org/2026/1912}
}