Audit reports, security advisories, software releases, research, and essays.
Verifpal 1.4 fixes false positives caused by combining incompatible protocol runs, detects two previously missed attacks, corrects precondition semantics, adds clearer verdict labels, gives AEAD a nonce so that nonce reuse can be modelled, and removes password-specific syntax.
23 min readVerifpal 1.3 adds peer scenarios, which instantiate a principal's counterparty differently across concurrent runs. That is what finally lets Verifpal find Lowe's attack on Needham-Schroeder and tell that protocol apart from its fix. Alongside it, every passing query now prints the envelope it was reached under, --saturate raises the session count until verdicts stop moving, and --auto-queries generates a query set from the model.
13 min readVerifpal 1.0 removes the beta warning the tool has printed with every analysis since 2020, on the strength of a new paper. The language now covers post-quantum key exchange, declared weakening assumptions, witness-based unlinkability, and two concurrent sessions of every principal; the engine behind it comes with a soundness theorem that holds however the solver behaves, unconditional termination, and attack traces measured for readability against ProVerif and Tamarin.
20 min readVerifpal 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 readFive people joined us this summer: two research interns formalizing zkVM soundness bounds in Lean, and three teaching assistants running the Applied Cryptography course. Here they are, in their own words.
4 min readCedarcrypt's first edition has concluded. On what a year of teaching cryptography in and for Lebanon has meant, why the conference met in Cyprus rather than Beirut, and the decades of work ahead.
12 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 readA note on Symbolic Software's technical review of Telegram's MTProto protocol, made public in 2026 through litigation. Covers the auth_key_id tracking vulnerability, the empirical case against Telegram's 'changes regularly' rebuttal, the editorial independence terms of the engagement, and how the document entered the public record.
13 min readFifty students from nine institutions were admitted to the free Summer 2026 Applied Cryptography online course.
2 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 read