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.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.
Read →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 →