Palak Jain

We model and analyse the Signal end-to-end messaging protocol within the UC framework. In particular:

• We formulate an ideal functionality that captures end-to-end secure messaging, in a setting with PKI and an untrusted server, against an adversary that has full control over the network and can adaptively and momentarily compromise parties at any time and obtain their entire internal states. In particular our analysis captures the forward secrecy and recovery-of-security properties of Signal and the conditions under which they break.
• We model the main components of the Signal architecture (PKI and long-term keys, the backbone continuous-key-exchange or “asymmetric ratchet”, epoch-level symmetric ratchets, authenticated encryption) as individual ideal functionalities that are realised and analysed separately and then composed using the UC and Global-State UC theorems.
• We show how the ideal functionalities representing these components can be realised using standard cryptographic primitives under minimal hardness assumptions.

Our modelling introduces additional innovations that enable arguing about the security of Signal irrespective of the underlying communication medium, as well as secure composition of dynamically generated modules that share state. These features, together with the basic modularity of the UC framework, will hopefully facilitate the use of both Signal-as-a-whole and its individual components within cryptographic applications.

Two other features of our modelling are the treatment of fully adaptive corruptions, and making minimal use of random oracle abstractions. In particular, we show how to realise continuous key exchange in the plain model, while preserving security against adaptive corruptions.