I do research in applied cryptography more specifically and computer security more generally. I am a professor at NYU Paris and direct Symbolic Software.

Ph.D. Thesis

Formal Verification for Real-World Cryptographic Protocols and Implementations — defended December 10, 2018 at INRIA Paris after 3½ years of research with Team PROSECCO.

Company

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.

Teaching

• CSCI-UA.9480: Computer Security at NYU Paris.
• new CSCI.UA-9102: Data Structures at NYU Paris.

Software

• Noise Explorer: online engine for reasoning about, formally verifying and generating implementations for arbitrary Noise-based cryptographic protocols.
• Resilience: ad blocker without compromises.
• DiskGem: command-line secure file transfer (SFTP) client written in Go.
• Maze Café, Nadimtris, CNNCTFR: fun toys.

Posts

• 11 Apr. 2019: Selfie's Reflections on TLS 1.3: Largely Opaque
• 26 Oct. 2018: Repairing a ThinkPad with a Corrupt Thunderbolt Firmware Chip
• 23 Nov. 2015: On Encryption and Terrorists

Selected Publications

• new EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats (with A. Delignat-Lavaud, C. Fournet, T. Ramananandro, N. Swamy, T. Chahed), 28th USENIX Security Symposium, 2019.
• Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols (with G. Nicolas, K. Bhargavan), 4th IEEE European Symposium on Security and Privacy, 2019.
• 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.
• FlexTLS: A Tool for Testing TLS Implementations (with B. Beurdouche, A. Delignat-Lavaud, A. Pironti, K. Bhargavan), 9th USENIX Workshop on Offensive Technologies, 2015.

Invited Talks

• 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.
• Bringing Formal Verification to the Real Web: Three Years of Interconnected Work Formal Methods Meets JavaScript Workshop, Imperial College London, 2018.