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.
AI Summary
Video chapters
0:00A challenge-response protocol example2:24Limits of academic verification tools5:03Verifpal's accessible modeling language7:19Workbench, attack traces and error messages11:14Forward secrecy, quantum attacks and compromised peers15:08WalletConnect signature verification flaw17:51Iterative design and analysis trade-offs24:14Readable models in the age of AI26:59Questions and answers
Key facts
- In WalletConnect, a failed signature validation called a reject function that showed an error but did not halt the protocol; the flaw had been present since 2024, was found using Verifpal, and has been acknowledged by the maintainers, who are fixing it.
- Verifpal cannot perform unbounded session analysis, so its absence-of-attack results are weaker guarantees than those from ProVerif or Tamarin.
- Verifpal Workbench runs Verifpal entirely in the browser without installation, alongside extensions for Visual Studio Code, Zed and Neovim.
- According to the speaker, more than 200 bugs were fixed in Verifpal this year, largely thanks to AI-assisted testing, fuzzing and bug finding.
Ideas
- Building cryptographic primitives such as signing, verification and authenticated encryption into the modeling language removes a common source of user error, since tools like ProVerif require users to define those primitives themselves.
- Attack traces are rendered in plain English using the model's own variable names. Combined with guarded values that represent keys authenticated out of band, this supports a fast cycle of modeling a protocol, finding an attack and repairing it.
- Phases add temporal logic to a model: long-term keys can leak in a later phase to test forward secrecy and post-compromise security, and primitives can be declared weak, forgeable or malleable from a given phase to simulate the arrival of quantum computers.
- Symbolic analyzers cannot tell apart primitives with very different real-world failure modes, such as AES-GCM (Advanced Encryption Standard in Galois/Counter Mode) versus AES-GCM-SIV under nonce reuse, so none of these tools should be treated as delivering complete proofs.
- As AI generates huge volumes of formally verified code that no one can read, a human-readable modeling language becomes more important for keeping engineers able to reason about, and remain accountable for, their systems.
Keywords
- Verifpal
- cryptography
- cryptographic protocol analysis
- symbolic formal verification
- WalletConnect
- post-quantum
Quotes
- “I have never claimed that verifpal gives you proofs. I have claimed that verifpal allows you to reason about your protocol better and to find attacks.”
- “Verifpal is the bridge between the formal methods experts and the rest of the team.”
- “But there's so much formally verified code now that no one is able to read it. There's too much of it.”
Recommendations
- Start with Verifpal models to give the whole team a common, readable description of how a protocol works, then use them as the foundation for more complete ProVerif or Tamarin models maintained by formal-methods experts for higher assurance.
- Check that failed verifications actually stop protocol execution: in Verifpal, a question mark after a check such as signature verification makes the principal abort on failure, which is exactly what WalletConnect's implementation lacked.
- Inferred from the closing answer: treat a protocol model as evidence about the design only, and pair it with sound software engineering, because no analysis tool covers how the protocol is deployed, such as how keys are handled in practice.
Resources
- Verifpal — Tool — Lets security practitioners model protocols, query confidentiality and authentication, and read clear attack traces without formal-methods expertise.
- Verifpal Workbench — Tool — Lowest-friction way to try protocol modeling, as nothing has to be installed.
- ProVerif — Tool — Next step after Verifpal when stronger guarantees of the absence of attacks are needed.
- Tamarin Prover — Tool — Alternative or complement to ProVerif after Verifpal when stronger guarantees are needed, especially for stateful protocols or properties that require manual proof guidance.
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 …