Paper 2022/1710

Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations

Cas Cremers, CISPA Helmholtz Center for Information Security
Charlie Jacomme, Inria Paris
Aurora Naska, CISPA Helmholtz Center for Information Security

The building blocks for secure messaging apps, such as Signal’s X3DH and Double Ratchet (DR) protocols, have received a lot of attention from the research community. They have notably been proved to meet strong security properties even in the case of compromise such as Forward Secrecy (FS) and Post-Compromise Security (PCS). However, there is a lack of formal study of these properties at the application level. Whereas the research works have studied such properties in the context of a single ratcheting chain, a conversation between two persons in a messaging application can in fact be the result of merging multiple ratcheting chains. In this work, we initiate the formal analysis of secure messaging taking the session-handling layer into account, and apply our approach to Sesame, Signal’s session management. We first experimentally show practical scenarios in which PCS can be violated in Signal by a clone attacker, despite its use of the Double Ratchet. We identify how this is enabled by Signal’s session-handling layer. We then design a formal model of the session-handling layer of Signal that is tractable for automated verification with the Tamarin prover, and use this model to rediscover the PCS violation and propose two provably secure mechanisms to offer stronger guarantees.

Available format(s)
Cryptographic protocols
Publication info
Formal analysisTamarinPCSPost-Compromise SecuritySignalSesame
Contact author(s)
cremers @ cispa de
charlie jacomme @ inria fr
aurora naska @ cispa de
2023-02-20: last of 2 revisions
2022-12-09: received
See all versions
Short URL
Creative Commons Attribution


      author = {Cas Cremers and Charlie Jacomme and Aurora Naska},
      title = {Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations},
      howpublished = {Cryptology ePrint Archive, Paper 2022/1710},
      year = {2022},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.