11 posts tagged “Post-Quantum”.
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 readA 52-page practitioner guide for engineers and architects working on post-quantum migration, alongside an interactive scorecard and TLS scanner at pq-migration.symbolic.software.
1 min readWhy Symbolic Software agrees with Soatok's position on hybrid post-quantum constructions: hybrids are compelling for KEMs, far less necessary for signatures, and the real risk is migration friction.
6 min readSymbolic Software is recommending post-quantum native design for all new cryptographic systems. This post examines the evidence behind that recommendation, its limitations, and the epistemic questions the industry should be confronting.
11 min readWe tested 15 ML-KEM and ML-DSA implementations across 5 languages, and found two conformance gaps and no security vulnerabilities.
4 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 readKyber-K2SO version 1.0 upgrades from Kyber v3 to ML-KEM, the NIST-standardized post-quantum key encapsulation mechanism.
4 min readWe've updated Kyber-K2SO to address a variable timing logic issue.
3 min read