Cryptographic Protocol Analysis for the Rest of Us
Virtually all privacy depends on well-designed cryptographic protocols, yet a person working in security should be able to examine a protocol without having to become a formal-methods specialist first. Existing tools offer considerable power — but should mastering that machinery be the price of admission?
Verifpal gives you an easy way to define the model. Use its language to describe who knows what, what they compute, and what they send. Built-in cryptographic operations, a browser-based workbench, live editor feedback and protocol diagrams guide you to an iterative model-attack-repair cycle that allows to you examine or enhance the protocol in terms of robustness. Close to the release of Verifpal 1.0 in August 2026, Verifpal was used to discover three new authentication flaws in WalletConnect, one reproduced against an unmodified SDK, and novel weaknesses in SimpleX Chat. Verifpal performs bounded attack search, not unbounded proofs.
About the speaker
Nadim Kobeissi
Nadim Kobeissi is the founder of the Paris-based Symbolic Software, an independent applied cryptography lab with 300+ engagements for clients including Coinbase, Mozilla, and the Ethereum Foundation. He created the protocol modeling and verification engine Verifpal, teaches an Applied Cryptography course first offered at the American University of Beirut, and chairs Cedarcrypt, the Levant’s applied cryptography summer school and conference.
Nadim earned his Ph.D. at Inria Paris on formal verification of real-world cryptographic protocols, where he worked on some of the first formal verification efforts for smart contracts, Signal, TLS, and the Noise Protocol Framework. He is also an active advocate for digital privacy rights and is recognized as a leading expert on end-to-end encrypted secure messaging.
Read more …