Nadim Kobeissi

I've recently founded Capsule Social, a startup that's building a decentralized discourse platform that's resilient to anti-intellectual, mob-motivated censorship and takedowns by private corporations. See also TechCrunch coverage.

Since 2018, I've run Symbolic Software, a Paris-based software published and applied cryptography consulting office. As its director, I manage a small team that offers security audits, cryptographic protocol design and formal verification services. Since its founding in 2017, Symbolic Software has completed and delivered over 300 software and cryptographic audits for clients all around the world. Symbolic Software also publishes well-known research software for applied cryptographers.

All of my worthwhile software projects are published by Symbolic Software and can be viewed over on its website.

In 2018, I defended my Ph.D. thesis, Formal Verification for Real-World Cryptographic Protocols and Implementations, at Inria Paris, after 3½ years of research with team PROSECCO.

In 2018 and 2019, I also designed and taught the computer security course at New York University's Paris campus, where I served as an adjunct professor.

Publications and Podcast

Publications aside, I also host Cryptography FM, a weekly podcast with news and a featured interview covering the latest developments in theoretical and applied cryptography. Whether it's a new innovative paper on lattice-based cryptography or a novel attack on a secure messaging protocol, we'll get the people behind it on Cryptography FM to talk about it.

• Verifpal: Cryptographic Protocol Analysis for the Real World (with G. Nicolas, M. Tiwari), 21st International Conference on Cryptology in India, 2020
• 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
• Ledger Design Language: Designing and Deploying Formally Verified Public Ledgers (with N. Kulatova), Workshop on Security Protocol Implementations, 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), 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-Beguelin), 11th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security, 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

Blog Posts

• 2021-06-20: Adventures in Writing Othello Software for iOS and macOS
• 2021-06-02: On the Feasibility of Secure Traceability in End-to-End Encrypted Messaging
• 2020-11-26: On the Apple Silicon M1 MacBook Pro
• 2020-09-07: Fear and Loathing in Protocol Analysis
• 2020-05-27: Why StopCOVID Fails as a Privacy-Preserving Design
• 2020-04-25: iPhone SE and the Commodification of the Pocket Computer
• 2020-04-17: An Investigation Into PEPP-PT
• 2020-03-29: Thoughts on 'Half-Life: Alyx' and G-Man
• 2019-04-11: Selfie's Reflections on Formal Verification for TLS 1.3: Largely Opaque
• 2018-10-26: Repairing a ThinkPad with a Corrupt Thunderbolt Firmware Chip
• 2015-11-25: On Encryption and Terrorists

Other Interests

Check out this gallery of my favorite paintings. I'm also a hobbyist photographer.