Our Audit of the 4Mica Payment Network
We audited 4Mica's collateral-backed payment network. Its BLS signatures and netting were correct; the serious risks were in settlement and key management.
2 min readBlog
Audit reports, security advisories, software releases, research, and essays.
The Electronic Passport, Modeled in Verifpal
Exploring passport security with Verifpal: why a page scan matters, what stops a copied chip, and how an identity check can reach the wrong service.
17 min readVerifpal 1.5: Auditing the Verifier with Frontier AI Models
Verifpal 1.5 is out: an audit with frontier AI models fixes false reports, missed attacks, and a crash. We also explain how Verifpal compares with ProVerif and Tamarin.
17 min readVerifpal 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 readHow 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 read