Tamarin Prover

1. Contract

1. RECORD roles, messages, sessions/state, trust anchors, channels, compromise/reveal/erasure timing, and claims.
2. ASSUME Dolev-Yao network control for In/Out unless explicitly modeled otherwise.
3. CLASSIFY trace | observational equivalence | accountability. LIST symbolic abstractions, equations, omitted implementation behavior, and bounds.
4. ROUTE computational reductions, primitive security, implementation correctness, and side channels to separate analyses.

Gate: explicit threat model, property class, and symbolic-to-protocol boundary.

2. Toolchain

READ references/installation.md for installation/upgrade, dependency discovery, WSL, or remote access. SELECT a supported pinned release; source build only for development/required unreleased features.