We propose a novel methodology that allows protocol designers, implementers, and security analysts to collaboratively verify a protocol using automated tools. The protocol is implemented in ProScript, a new domain-specific language that is designed for writing cryptographic protocol code that can both be executed within JavaScript programs and automatically translated to a readable model in the applied pi calculus. This model can then be analyzed symbolically using ProVerif to find attacks in a variety of threat models. The model can also be used as the basis of a computational proof using CryptoVerif, which reduces the security of the protocol to standard cryptographic assumptions. If ProVerif finds an attack, or if the CryptoVerif proof reveals a weakness, the protocol designer modifies the ProScript protocol code and regenerates the model to enable a new analysis. We demonstrate our methodology by implementing and analyzing a variant of the popular Signal Protocol with only minor differences. We use ProVerif and CryptoVerif to find new and previously-known weaknesses in the protocol and suggest practical countermeasures. Our ProScript protocol code is incorporated within the current release of Cryptocat, a desktop secure messenger application written in JavaScript. Our results indicate that, with disciplined programming and some verification expertise, the systematic analysis of complex cryptographic web applications is now becoming practical.
@INPROCEEDINGS{KobeissiBhargavanBlanchetEuroSP17, AUTHOR = {Nadim Kobeissi and Karthikeyan Bhargavan and Bruno Blanchet}, TITLE = {Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach}, BOOKTITLE = {2nd IEEE European Symposium on Security and Privacy (EuroS\&P'17)}, YEAR = {2017}, PAGES = {435--450}, MONTH = APR, ADDRESS = {Paris, France}, PUBLISHER = {IEEE} }