This work explores real-world deniability in messaging. We propose a formal model that considers the entire messaging system to analyze deniability in practice. Applying this model to the Signal application and DKIM-protected email, we demonstrate that these systems do not offer practical deniability guarantees. Additionally, we analyze 140 court cases in Switzerland that use conversations on messaging applications as evidence and find that none consider deniability, providing evidence that this property does not have an impact in the legal setting. Based on these technical and legal findings, we assess whether deniability is a desirable property and the challenges and shortcomings of designing a system that is deniable in practice. We posit that systems should either offer real-world deniability or refrain from claiming to achieve it. We discuss how to choose an appropriate threat model for deniability in a given context and how to design communication systems that are deniable in practice. For Signal, we propose and discuss a simple yet effective solution: the application should enable direct modification of locally stored messages in the user interface. This position paper raises several unanswered questions, aiming to further stimulate discussion and research on real-world deniability in messaging.

The Signal Protocol is a two-party secure messaging protocol used in applications such as Signal, WhatsApp, Google Messages and Facebook Messenger and is used by billions daily. It consists of two core components, one of which is the Double Ratchet protocol that has been the subject of a line of work that aims to understand and formalise exactly what security it provides. Existing models capture strong guarantees including resilience to state exposure in both forward security (protecting past secrets) and post-compromise security (restoring security), adaptive state corruptions, message injections and out-of-order message delivery. Due to this complexity, prior work has failed to provide security guarantees that do not degrade in the number of interactions, even in the single-session setting.

Abstract To mitigate state exposure threats to long-lived instant messaging sessions, ratcheting was introduced, which is used in practice in protocols like Signal. However, existing ratcheting protocols generally come with a high cost. Recently, Caforio et al. proposed pragmatic constructions, which compose a weakly secure ‘light’ protocol and a strongly secure ‘heavy’ protocol, in order to achieve so-called ratcheting on-demand. The light protocol they proposed has still a high complexity. In this paper, we propose the lightest possible protocol we could imagine, which essentially encrypts and then hashes the secret key. We prove it secure in the standard model by introducing a new security notion, which relates symmetric encryption with key updates by hashing. Our protocol composes well with the generic transformation techniques by Caforio et al. to offer high security and performance at the same time. In a second step, we propose another protocol based on a newly defined integrated primitive, extending standard one-time authenticated encryption with an additional output block used as a secret key for the next message. We instantiate this primitive firstly from any authenticated encryption with associated data, and then we propose an efficient instantiation using advanced encryption standard (AES) encryption to update the key and AES-Galois/Counter mode of operation to encrypt and decrypt messages.

We address the problem of online payments, where users can transfer funds among themselves. We introduce Astro, a system solving this problem efficiently in a decentralized, deterministic, and completely asynchronous manner. Astro builds on the insight that consensus is unnecessary to prevent double-spending. Instead of consensus, Astro relies on a weaker primitive---Byzantine reliable broadcast---enabling a simpler and more efficient implementation than consensus-based payment systems. In terms of efficiency, Astro executes a payment by merely broadcasting a message. The distinguishing feature of Astro is that it can maintain performance robustly, i.e., remain unaffected by a fraction of replicas being compromised or slowed down by an adversary. Our experiments on a public cloud network show that Astro can achieve near-linear scalability in a sharded setup, going from 10K payments/sec (2 shards) to 20K payments/sec (4 shards). In a nutshell, Astro can match VISA-level average payment throughput, and achieves a 5× improvement over a state-of-the-art consensus-based solution, while exhibiting sub-second 95^th percentile latency.