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 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 2018, Symbolic Software has completed and delivered over 250 software and cryptographic audits for clients all around the world.

I also write research software: Verifpal, an automated cryptographic protocol modeling, analysis and verification framework and a project that I am very passionate about.

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.


Blog Posts

RSS RSS feed

Software Projects

I've written dozens of software projects over the years. Here, I'm listing only the ones that I think are genuinely meaningful to me personally, organized purely according to how much I like them.

VerifpalWebsiteCode

Verifpal is 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. Verifpal is really cool!

PiccoloApp StoreWebsite

Piccolo started off as a pet project to develop a strong AI for the Japanese Othello board game, but then matured into a full software application for iPhone, iPad and Mac. It comes with a strong AI opponent (written in Go), a nice native user interface (written in SwiftUI), over eight beautiful themes (designed by myself), an online play service, and more. Despite it just being a “board game app”, a lot of thinking and design effort went into Piccolo, and it's one of my favorite software projects. Featured in Apple's “Games We Love” on the iPhone, iPad and Mac App Stores!

Noise ExplorerWebsiteCode

Noise Explorer is an 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.

Kyber-K2SOCode

Kyber-K2SO is a clean implementation of the Kyber IND-CCA2-secure key encapsulation mechanism (KEM), whose security is based on the hardness of solving the learning-with-errors (LWE) problem over module lattices. Kyber is one of the candidate algorithms submitted to the NIST post-quantum cryptography project.


Other Interests

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