Insights from our audit practice, software releases, and applied cryptography research.
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 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 readOur initial audit of the Rust implementation of dWallet Labs' 2PC-MPC protocol.
2 min readWe've updated Kyber-K2SO to address a variable timing logic issue.
3 min readSymbolic Software continues its support for the IACR Real World Cryptography Symposium.
1 min readAn address to France's law enforcement officials on Internet surveillance policy in France.
11 min readOur extensive audit for the Native Labs smart contracts.
2 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