A polite standard makes cryptography safer to use in the real world. It anticipates edge cases and security problems, provides interfaces that reduce misuse, explains implementation and usage, and supplies test vectors for checking correctness. section 16.2
A well-behaved standard should:
- Leave little room for implementers to make dangerous mistakes. section 16.2
- Cover edge cases and potential security issues instead of assuming ideal inputs. section 16.2
- Include matching input-output test vectors for implementation testing. section 16.2
- Balance cryptographic agility against added complexity and downgrade risks. 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.
Formal verification can model a cryptographic protocol and search for attacks, complementing careful standard design. section 16.2
