nadim.computer Open in urlscan Pro
2606:4700:3036::ac43:d6cf  Public Scan

Form analysis
0 forms found in the DOM

Text Content

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 (2019—): 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 (2018—): 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 (2022—): 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 (2024—): 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 (2021—): 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.


GAME BOY COLOR GAME REVIEWS

I have a small independent website that reviews Game Boy Color games called
Color Cart Critic.

--------------------------------------------------------------------------------


BLOG POSTS

 * 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-08-16: My Work Desk in 2023
 * 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-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

RSS feed

--------------------------------------------------------------------------------


OTHER INTERESTS

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

Contact information: Email • X • Mastodon

© 2024 Nadim Kobeissi. All Rights Reserved.