Audit reports, security advisories, software releases, research, and essays.
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 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 readWe've updated Noise Explorer to address two bugs in generated Rust and WebAssembly implementations of Noise Protocol Framework handshake patterns.
2 min readThree findings in libcrux's ML-DSA implementation: a verifier norm check that is dead code due to a wrong constant, a missing bounds check in hint deserialization, and a wrong multiplication specification that renders AVX2 proofs unsound.
12 min readCE Labs said they'd be 'very interested' if someone found a bug in their verified code. We found three.
13 min readVerifpal 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 readA case study on CE Labs' libcrux exposing the gap between formal verification marketing and engineering reality.
10 min readAnnouncing Cedarcrypt, a new applied cryptography summer school and conference.
2 min readKyber-K2SO version 1.0 upgrades from Kyber v3 to ML-KEM, the NIST-standardized post-quantum key encapsulation mechanism.
4 min readThe public report from our audit, with 3MI Labs, of dWallet Labs' 2PC-MPC Rust implementation.
1 min readWe've updated Kyber-K2SO to address a variable timing logic issue.
3 min readSymbolic Software is sponsoring the IACR Real World Cryptography Symposium for the sixth consecutive year.
1 min read