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

(2023) Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations. (Submitted)

Text USENIX23-final.pdf - Accepted Version Download (581kB)

Abstract

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.

Item Type:	Conference or Workshop Item (A Paper) (Paper)
Divisions:	Cas Cremers (CC)
Conference:	USENIX-Security Usenix Security Symposium
Depositing User:	Alexander Dax
Date Deposited:	08 Mar 2023 12:26
Last Modified:	08 Mar 2023 12:26
Primary Research Area:	NRA2: Reliable Security Guarantees
URI:	https://publications.cispa.saarland/id/eprint/3905

Actions

Actions (login required)

View Item