Secrecy in Squirrel and the Post-Compromise Security of a Ratchet

Clément Hérouard; Charlie Jacomme; Adrien Koutsos; Joseph Lallemand

Paper 2026/1912

Secrecy in Squirrel and the Post-Compromise Security of a Ratchet

Clément Hérouard

, Université de Lorraine, National Council for Scientific Research, French Institute for Research in Computer Science and Automation, LORIA

Charlie Jacomme

, Université de Lorraine, National Council for Scientific Research, French Institute for Research in Computer Science and Automation, Loria

Adrien Koutsos

, French Institute for Research in Computer Science and Automation

Joseph Lallemand

, Univ. Rennes, National Council for Scientific Research, Institut de Recherche en Informatique et Systèmes Aléatoires

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: Published elsewhere. Minor revision. CCS'26
Keywords: Protocols Formal Methods Verification Computer-aided Cryptography
Contact author(s): clement herouard @ inria fr
charlie jacomme @ inria fr
adrien koutsos @ inria fr
joseph lallemand @ irisa fr
History: 2026-09-10: approved; 2026-09-07: received; See all versions
Short URL: https://ia.cr/2026/1912
License: CC BY

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}
}