What is Symbolic vs computational model? Definition and why it matters
======================================================================

The 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.

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.

Source page: https://sorryfree.com/glossary/symbolic-vs-computational/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13