Applied cryptography
2017 · Paris, France
Audit reports, security advisories, software releases, research, and essays.
An examination of CE Labs' TLS implementations reveals 75% of valid ECDSA signatures rejected, authentication tags silently dropped, no certificate validation, and remote denial-of-service vectors.
11 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 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 read