Verifpal 1.5: Auditing the Verifier with Frontier AI Models
Verifpal 1.5 is out: an audit with frontier AI models fixes false reports, missed attacks, and a crash. We also explain how Verifpal compares with ProVerif and Tamarin.
17 min readSoftware.
20 posts in category “Software”.
Verifpal Takes on TLS 1.3
An overnight analysis, nineteen security queries, and three expected counterexamples: modeling TLS 1.3 with concurrent sessions, malicious certified peers, completion preconditions, and staged key compromise.
10 min readHow Verifpal Finds a 3-of-5 Threshold-Signature Forgery
A walkthrough of Verifpal 1.4.4's FROST-shaped model: two signing oracles and one leaked share cross a 3-of-5 threshold, producing a valid signature without disclosing the group key.
8 min readVerifpal 1.4: More Accurate Protocol Analysis
Verifpal 1.4 fixes false positives caused by combining incompatible protocol runs, detects two previously missed attacks, corrects precondition semantics, adds clearer verdict labels, gives AEAD a nonce so that nonce reuse can be modelled, and removes password-specific syntax.
23 min readVerifpal 1.3: Who Alice Thinks She's Talking To
Verifpal 1.3 adds peer scenarios, which instantiate a principal's counterparty differently across concurrent runs. That is what finally lets Verifpal find Lowe's attack on Needham-Schroeder and tell that protocol apart from its fix. Alongside it, every passing query now prints the envelope it was reached under, --saturate raises the session count until verdicts stop moving, and --auto-queries generates a query set from the model.
13 min readVerifpal Reaches 1.0: A Toy Becomes an Instrument
Verifpal 1.0 removes the beta warning the tool has printed with every analysis since 2020, on the strength of a new paper. The language now covers post-quantum key exchange, declared weakening assumptions, witness-based unlinkability, and two concurrent sessions of every principal; the engine behind it comes with a soundness theorem that holds however the solver behaves, unconditional termination, and attack traces measured for readability against ProVerif and Tamarin.
20 min readVerifpal 0.80.0: Nuancing Weak Cryptography Modeling and Witness-Based Unlinkability
Verifpal 0.80.0 lets a model declare that a particular piece of cryptography is broken (weak, forgeable, and from a chosen phase onward) instead of approximating the break with a list of leaked values, and decides unlinkability queries by searching for a concrete link witness that it then reports back to you.
19 min readVerifpal 0.70.0: Post-Quantum Key Exchange, and an Attacker That Works Backwards
Verifpal 0.70.0 removes Diffie-Hellman equations from the modelling language, adds a generic KEM for post-quantum and hybrid key exchange, rebuilds the active attacker around a search that works backwards from each query, and narrates every attack it finds as numbered causal steps.
20 min readHow Jevil works
A playground-first, interactive explainer for Jevil, a post-quantum, transparent few-time signature scheme whose key-recovery threshold is a single sharp cliff rather than a slow slope.
11 min readhpke-ng: Faster, Smaller, Harder HPKE for Rust
126 head-to-head benchmarks against hpke-rs and rust-hpke. hpke-ng wins 103, ties 19, loses 4. ML-KEM-1024 decap −55%, X25519 decap −41%, export −72% to −76%, end-to-end roundtrip −30%, plus a type system that catches four classes of bug at compile time.
26 min readVerifpal 0.51.0: Sharper Semantics for Passwords, Assertions, and AEAD
Verifpal 0.51.0 tightens the analysis engine's treatment of password-qualified values, checked ASSERT? assertions, and AEAD associated data, all on the back of excellent bug reports from the community.
7 min readCrucible: Forging Post-Quantum Implementations in the Fire of Real Audit Findings
We tested 15 ML-KEM and ML-DSA implementations across 5 languages, and found two conformance gaps and no security vulnerabilities.
4 min readMaking Verifpal Easier to Reason About
Verifpal's analysis engine has been redesigned with a unified equational theory, provenance-tagged values, a formally grounded deduction loop, and a bounded-depth search that runs 3x faster, plus updated tooling across the board.
11 min readVerifpal Workbench: Protocol Analysis in Your Browser
Verifpal now runs entirely in the browser via WebAssembly. The new Workbench at verifpal.com/workbench lets anyone write, verify, and visualize cryptographic protocol models with zero installation.
3 min readVerifpal, Rewritten in Rust
After seven years in Go, Verifpal has been completely rewritten in Rust, gaining a new analysis engine, massive performance improvements, a rich terminal interface, and a novel attack strategy that finds more attacks.
9 min readVerifpal Verifies Signal Across Three Messages
Verifpal 0.31.2 ships a major overhaul to active attacker analysis. Verifpal can now fully verify a model of Signal's three-message protocol, a result other tools reached years ago and that is new only for Verifpal.
7 min readKyber-K2SO 1.0: Now Implementing ML-KEM
Kyber-K2SO version 1.0 upgrades from Kyber v3 to ML-KEM, the NIST-standardized post-quantum key encapsulation mechanism.
4 min readOne Year of Verifpal
Understanding Verifpal's relationship with cryptographic protocol security.
5 min readBetter Queries for Verifpal
Towards new queries, automated model translation and formalized semantics in Verifpal.
6 min readModeling DP-3T With Verifpal
How Verifpal sped up the formal modeling efforts for a new pandemic-tracing Protocol.
8 min read