Verifpal Takes on TLS 1.3
An overnight analysis, nineteen security queries, and three expected counterexamples: modeling TLS 1.3 with concurrent sessions, malicious certified peers, completion preconditions, and staged key compromise.
10 min readWriting.
Audit reports, security advisories, software releases, research, and essays.
How Verifpal Finds a 3-of-5 Threshold-Signature Forgery
A walkthrough of Verifpal 1.4.4's FROST-shaped model: two signing oracles and one leaked share cross a 3-of-5 threshold, producing a valid signature without disclosing the group key.
8 min readVerifpal 1.4: More Accurate Protocol Analysis
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: Who Alice Thinks She's Talking To
Verifpal 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 Reaches 1.0: A Toy Becomes an Instrument
Verifpal 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: Nuancing Weak Cryptography Modeling and Witness-Based Unlinkability
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: Post-Quantum Key Exchange, and an Attacker That Works Backwards
Verifpal 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 readMeet the Symbolic Software Summer 2026 Team
Five 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 readWhy I Teach Cryptography in Lebanon
Cedarcrypt'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 readHow Jevil works
A 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 readOn Our Telegram MTProto Review
A 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 readApplied Cryptography: Summer 2026 Cohort
Fifty students from nine institutions were admitted to the free Summer 2026 Applied Cryptography online course.
2 min read