Formal Verification for Real-World Cryptographic Protocols and Implementations — defended December 10, 2018 at INRIA Paris after 3½ years of research with Team PROSECCO.
Symbolic Software is a company focused on modern insight into cryptographic systems. As its director, I manage a small team that offers security audits, cryptographic protocol design and formal verification services. We recently released Noise Explorer, an online engine for reasoning about and formally verifying Noise-based cryptographic protocols.
- CSCI-UA.9480: Computer Security at NYU Paris.
- DiskGem, a command-line secure file transfer (SFTP) client written in Go.
- Cryptocat, the first web-based secure messenger with end-to-end encryption. Infamous for security bugs during its early days, it eventually became the first secure messenger implementing a formally verified protocol (see EuroS&P 2017 paper below.)
- An Analysis of the ProtonMail Cryptographic Architecture, IACR Cryptology ePrint Archive, 2018.
- Ledger Design Language: Towards Formal Reasoning and Implementation for Public Ledgers (with N. Kulatova), Workshop on Security Protocol Implementations: Development and Analysis, 2018.
- Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate (with K. Bhargavan, B. Blanchet), 38th IEEE Symposium on Security and Privacy, 2017.
- Formal Modeling and Verification for Domain Validation and ACME (with K. Bhargavan, A. Delignat-Lavaud), 21st International Conference on Financial Cryptography and Data Security, 2017.
- Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach (with K. Bhargavan, B. Blanchet), 2nd IEEE European Symposium on Security and Privacy, 2017.
- Formal Verification of Smart Contracts (with K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, A. Rastogi, T. Sibut-Pinote, N. Swamy, S. Zanella-Béguelin), PLAS, 2016.
- new! Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols IACR Real World Cryptography Symposium, 2019.
- Capsule: A Protocol for Secure Collaborative Document Editing (draft) École Polytechnique Fédérale de Lausanne, 2018.
- Formal Verification for Cryptographic Systems in Web Applications OWASP Gothenburg, 2018.