A mini-protocol is a small, custom protocol built for an application when existing standardized protocols do not fit. That flexibility can become dangerous: incorrect assumptions about a primitive’s threat model or composability can create vulnerabilities. section 16.2
Treat a mini-protocol as a security design problem:
- Identify the threat model: determine what each cryptographic primitive protects against. section 16.2
- Check composability: examine how primitives behave when combined with one another or embedded in a larger protocol. section 16.2
- Model the protocol and test its security properties with formal verification rather than relying only on intuition. section 16.2
Figure 16.1 The Tamarin protocol prover is a free formal verification tool that you can use to model a cryptographic protocol and find attacks on it.
Use the Tamarin protocol prover to model a cryptographic protocol and search for attacks. section 16.2
