CISPA
Browse
cispa_all_3905.pdf (567.9 kB)

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

Download (567.9 kB)
Version 2 2023-12-11, 20:09
Version 1 2023-11-29, 18:23
conference contribution
posted on 2023-12-11, 20:09 authored by Cas CremersCas Cremers, Charlie Jacomme, Aurora NaskaAurora Naska
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 mes- saging 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.

History

Preferred Citation

Cas Cremers, Charlie Jacomme and Aurora Naska. Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations. In: Usenix Security Symposium (USENIX-Security). 2023.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Usenix Security Symposium (USENIX-Security)

Legacy Posted Date

2023-03-08

Open Access Type

  • Gold

BibTeX

@inproceedings{cispa_all_3905, title = "Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations", author = "Cremers, Cas and Jacomme, Charlie and Naska, Aurora", booktitle="{Usenix Security Symposium (USENIX-Security)}", year="2023", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC