sorryfreeLast reviewed 2026-09-13
Index › Glossary › Symbolic vs computational model

Symbolic vs computational model

Direct answerThe symbolic (Dolev-Yao) model treats cryptographic primitives as perfect black boxes and searches for logical attacks automatically; the computational model reasons about probabilistic polynomial-time adversaries and concrete security bounds, matching cryptographers' proofs.

In more detail

Symbolic tools (Tamarin, ProVerif, Verifpal) are fast and find protocol-logic flaws over unbounded sessions but cannot see weaknesses inside primitives. Computational tools (EasyCrypt, CryptoVerif, SSProve) give the guarantee a cryptographer expects at far higher effort. Squirrel attempts to combine them. Most serious protocol analyses use one of each.

Frameworks that address it

Tamarin, ProVerif, EasyCrypt, CryptoVerif.

Circuit soundness, Circuit completeness, Underconstrained circuit, Overconstrained circuit, Specification gap, Trusted computing base and verification boundary, Proof assistant vs SMT-based verifier, Bounded model checking, Equivalence checking, Refinement, Constant-time verification, Arithmetization (R1CS, PLONKish, AIR), Extraction (code to model), Witness generation vs constraints

Getting help

Firms on this index that handle this in practice: zkSecurity, Galois, Veridise, Nethermind (Formal Verification team).

Last reviewed 2026-09-13 by the sorryfree editors. Machine-readable: data.json · summary.txt