Conclusions and Future Work
In this work we provided the first formal security analysis of the cryptographic core of the Signal protocol.
While any first analysis for such a complex object will be necessarily incomplete, our analysis leads to several
observations
First, our analysis shows that the cryptographic core of Signal provides useful security properties. These
properties, while complex, are encoded in our security model, and which we prove that Signal satisfies under
standard cryptographic assumptions. Practically speaking, they imply secrecy and authentication of the message
keys which Signal derives, even under a variety of adversarial compromise scenarios such as forward security
(and thus “future secrecy”). If used correctly, Signal could achieve a form of post-compromise security, which
has substantial advantages over forward secrecy as described in [12].
Our analysis has also revealed many subtleties of Signal’s security properties. For example, we identified six
different security properties for message keys (triple, triple+DHE, asym-ir, asym-ri, sym-ir and sym-ri).
One can imagine strengthening the protocol further. For example, if the random number generator becomes
fully predictable, it may be possible to compromise communications with future peers. We have pointed out to
the developers that this can be solved at negligible cost by using constructions in the spirit of the NAXOS
protocol [35] or including a static-static DH shared secret in the key derivation.
We have described some of the limitations of our approach in Section 6. Furthermore, the complexity and
tendency to add “extra features” makes it hard to make statements about the protocol as it is used. Examples
include the ability to reset the state [12], encrypt headers, or support out-of-order decryption.
As with many real-world security protocols, there are no detailed security goals specified for the protocol,
so it is ultimately impossible to say if Signal achieves its goals. However, our analysis proves that several
standard security properties are satisfied by the protocol, and we have found no major flaws in its design, which
is very encouraging.