Nadim Kobeissi

I'm a computer scientist and a software developer with a focus on applied cryptography and software security. I'm also a hobbyist puzzle game developer and runner. I'm based in Paris, France. Professionally, I am:

Senior Applied Cryptography Auditor at Cure53, where I've worked on auditing over 150 real-world cryptographic systems.
Director at Symbolic Software, a software publisher and boutique applied cryptography consultancy based in Paris which has participated in over 250 software security audits and has published research software for applied cryptographers. Also publishes small indie puzzle game projects.

Previously, I wrote and 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. I also designed and taught the computer security course at New York University's Paris campus, where I served as an adjunct professor.

My Curriculum Vitae (PDF)

Software

My software is published by my small Paris-based company, Symbolic Software. Over the years, I've worked on probably over a dozen projects; here are the ones that matter and that are actively maintained:

Applied Cryptography

Verifpal: New software for verifying the security of cryptographic protocols. Building upon contemporary research in symbolic formal verification, Verifpal's main aim is to appeal more to real-world practitioners, students and engineers without sacrificing comprehensive formal verification features. Used by Google, Zoom, Bosch and others.
Noise Explorer: Online engine for designing, reasoning about, formally verifying and implementing arbitrary Noise Handshake Patterns. Based on our formal treatment of the Noise Protocol Framework, Noise Explorer can validate any Noise Handshake Pattern and then translate it into a model ready for automated verification and also into a production-ready software implementation written in Go or in Rust.

Puzzle Games

Dr. Kobushi's Labyrinthine Laboratory: Ambitious indie puzzle adventure game! Features over 100 levels, story, dialog, and innovative gameplay. Only the third ever commercial video game to be written in the Go programming language. It's a really nice game, check it out!
Runes of Ardun: Reimagining of the ancient Japanese strategy game Mini Shogi, transforming it into a strategic duel of wits and cunning on iPhone, iPad, Mac and Android. Includes original Shogi AI written from scratch in Rust, which plays at a competitive 2200 Elo rating. Featured in Apple's New Games We Love. Top 10 Board Game in the Japan, United States, United Kingdom, France, Switzerland and a dozen more countries' App Stores in 2024.
Piccolo: Othello: Othello software for macOS and iOS written in Rust and Swift. Featured in Apple's What We're Playing, Games We Love, and Best Games Made in France. #1 top overall game in the Japan Mac App Store from April to July 2021.

Selected Publications

DuckyZip: Provably Honest Global Linking Service, Cryptology ePrint Archive, 2023
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

Selected Presentations

The Broader Implications of Apple’s Content Scanning Push, Swiss Cyber Storm, 2021
Verifpal: Cryptographic Protocol Analysis for the Real World, IACR Real World Cryptography Symposium, 2021
Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols, IACR Real World Cryptography Symposium, 2019

Cryptography Podcast

I host Cryptography FM, a 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.

Blog Posts

2024-11-26: Getting a Driver's License in France
2024-11-18: An Internet of Desperate Protagonists
2024-08-27: Meredith Whittaker at Le Bourget
2024-05-16: Critique of the TechCrunch Article on Google's Call-Scanning AI
2024-04-18: We Need to Talk About the State of Calendar Software on Desktop
2023-07-22: Using the Apple Studio Display on a Windows Computer
2022-02-11: Rust on iOS and Mac Catalyst: A Simple, Updated Guide
2021-12-12: On Paying Open Source Maintainers
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-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

RSS feed