14 posts in category “Software”.
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 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 readA 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 read126 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 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 readWe tested 15 ML-KEM and ML-DSA implementations across 5 languages, and found two conformance gaps and no security vulnerabilities.
4 min readVerifpal'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 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 readAfter 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 0.31.2 ships a major overhaul to active attacker analysis, finally enabling full verification of Signal's three-message protocol.
7 min readKyber-K2SO version 1.0 upgrades from Kyber v3 to ML-KEM, the NIST-standardized post-quantum key encapsulation mechanism.
4 min readUnderstanding Verifpal's relationship with cryptographic protocol security.
5 min readTowards new queries, automated model translation and formalized semantics in Verifpal.
6 min readHow Verifpal sped up the formal modeling efforts for a new pandemic-tracing Protocol.
8 min read