Symbolic Software is an independent applied-cryptography consultancy. We review protocols, cryptographic designs, threat models, formal models, and implementations.
We review the threat model, protocol, primitive choices, formal models, and implementation. More than 250 engagements since 2017 have followed that approach.
Protocol design, cryptographic implementations, threat models, and formal analysis.
Verifpal, Crucible, hpke-ng, Kyber-K2SO, PQ Migration Playbook.
Applied Cryptography, an 18-topic university course with open materials.
Audit reports, security advisories, software releases, papers, and essays.
Crucible runs 129 conformance tests across 12 categories. Each test cites the relevant FIPS section and, where applicable, the audit finding that prompted it.
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.
Read →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.
Read →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.
Read →