'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.crem...@cs.ox.ac.uk -- Liberationtech is public & archives are searchable on Google. Violations of list guidelines will get you moderated: https://mailman.stanford.edu/mailman/listinfo/liberationtech. Unsubscribe, change to digest, or change password by emailing moderator at compa...@stanford.edu.
