RWC 2017 - A Formal Security Analysis of the Signal Messaging Protocol

Real World Crypto 2017 kicked off yesterday in New York City. This afternoon, Luke Garratt presented his and his colleagues' work, A Formal Security Analysis of the Signal Messaging Protocol. The signal protocol is used by the Facebook messenger app, WhatsApp and the Signal app (to name but a few). It is therefore surprising that there had been no formal security analysis, and their work addresses this issue. The paper is motivated by the questions

What should Signal achieve?

and

Does it?

Or, put in more modern language (spoiler alert),

Why what does is 

Let's first look at what kind of security we can hope for. We speak of Forward Secrecy, which ensures that past messages are not compromised even if the communication is at some point in the future. This is to prevent an adversary storing all the conversations and waiting until an attack is successful to then recover all the communication. 

Post-compromise security pushes this even further. If we have post-compromise security, not only past conversations are not compromised, but also future ones. The Signal protocol achieves this using a technique called ratcheting, which involves session keys being updated with each message sent. Why is this useful? Well, it makes the adversary's life much harder. In order to attack a system with post-compromise security, an adversary must obtain long-term keys and immediately attack and continue attacking if they want to compromise future sessions. As opposed to forward security, where an adversary would obtain a long-term key and wait for an interesting target to launch a man-in-the-middle attack (e.g. TLS-DHE) or to no forward security, where they would just store all ciphertext traffic until they obtain a long-term key and decrypt everything (e.g. TLS-RSA). Times are hard. 

Their security model captures: 

• Full network control by the adversary;
• Perfect forward secrecy;
• Post-compromise security;
• Key compromise impersonation attacks;
• Some (but not all) random numbers compromise.

Their proof is too long to be featured in this blog post, but Luke promises it is tedious rather than complex. Their conclusion? So far, so good. 

In terms of limitations, they note that they have not analysed any implementation of the protocol, so this is a theoretical analysis only. They also assume an honest key distribution and have not (yet) considered multiple devices.