I am a Ph.D. student at INRIA's PROSECCO lab, where I focus on applied cryptography and formal verification. I also operate Symbolic Software, a small software and applied cryptography consulting company.

Software

Noise Explorer, Cryptocat

Teaching Material

Cours de Cryptographie

Papers

• new! 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.
• ProScript-TLS: Verifiable Models and Systematic Testing for TLS 1.3 (with K. Bhargavan, B. Beurdouche), NDSS TRON, 2016.
• FLEXTLS: A Tool for Testing TLS Implementations (with B. Beurdouche, A. Delignat-Lavaud, A. Pironti, K. Bhargavan), USENIX WOOT, 2015.