[liberationtech] 'Trust it': Results of Signal's first formal crypto analysis are in

[Greg Walton]

'Trust it': Results of Signal's first formal crypto analysis are in

Crypto connoisseurs finds favourite chat app protocol up to scratch

8 Nov 2016 at 08:02, Darren Pauli

Source: http://www.theregister.co.uk/2016/11/08/trust_it_results_of_signals_first_formal_crypto_analysis_are_in/

Encrypted SMS and voice app Signal has passed a security audit with
flying colours.

As explained in a paper titled A Formal Security Analysis of the
Signal Messaging Protocol (PDF) from the International Association for
Cryptologic Research, Signal has no discernible flaws and offers a
well-designed and compromise-resistant architecture.

Signal uses a double rachet algorithm that employs ephemeral key
exchanges continually during each session, minimising the amount of
text that can be decrypted at any point should a key be compromised.

Signal was examined by a team of five researchers from the UK,
Australia, and Canada, namely Oxford University information security
Professor Cas Cremers and his PhDs Katriel Cohn-Gordon and Luke
Garratt, Queensland University of Technology PhD Benjamin Dowling, and
McMaster University Assistant Professor Douglas Stebila.

The team examines Signal threat models in the context of a fully
adversarially-controlled network to examine how it stands up, proving
that the cryptographic core of Signal is secure. As the authors write,
Signal's security is such that even testing it is hard:

Providing a security analysis for the Signal protocol is challenging
for several reasons. First, Signal employs a novel and unstudied
design, involving over ten different types of keys and a complex
update process which leads to various chains of related keys. It
therefore does not directly fit into existing analysis models. Second,
some of its claimed properties have only recently been formalised.
Finally, as a more mundane obstacle, the protocol is not substantially
documented beyond its source code.

They conclude that it is impossible to say if Signal meets its goals,
as there are none stated, but say their analysis proves it satisfies
security standards adding "we have found no major flaws in its design,
which is very encouraging".

The team finds some room for improvement which they passed on to the
app's developers, namely that the protocol can be further strengthened
with negligible cost by using "constructions in the spirit of the
NAXOS (authenticated key exchange) protocol" [PDF]" by or including a
static-static Diffie-Hellman shared secret in the key derivation. This
would solve the risk of attackers compromising communications should
the random number generator become fully predictable.

The paper does, however, cover only a subsection of Signal's efforts,
as it ignores non-Signal library components, plus application and
implementation variations. It should therefore be considered a
substantial starting point for future analysis, the authors say,
rather than the final world on Signal. ®




The paper is here: https://eprint.iacr.org/2016/1013


Cryptology ePrint Archive: Report 2016/1013


A Formal Security Analysis of the Signal Messaging Protocol


Katriel Cohn-Gordon and Cas Cremers and Benjamin Dowling and Luke
Garratt and Douglas Stebila


Abstract: Signal is a new security protocol and accompanying app that
provides end-to-end encryption for instant messaging. The core
protocol has recently been adopted by WhatsApp, Facebook Messenger,
and Google Allo among many others; the first two of these have at
least 1 billion active users. Signal includes several uncommon
security properties (such as "future secrecy" or "post-compromise
security"), enabled by a novel technique called *ratcheting* in which
session keys are updated with every message sent. Despite its
importance and novelty, there has been little to no academic  analysis
of the Signal protocol.


We conduct the first security analysis of Signal's Key Agreement and
Double Ratchet as a multi-stage key exchange protocol. We extract from
the implementation a formal description of the abstract protocol, and
define a security model which can capture the "ratcheting" key update
structure. We then prove the security of Signal's core in our model,
demonstrating several standard security properties. We have found no
major flaws in the design, and hope that our presentation and results
can serve as a starting point for other analyses of this widely
adopted protocol.



Lead Author: cas.cremers at cs.ox.ac.uk