Summary, cont’d
Inductive proofs
- Can prove correctness
- Require substantial effort
- Can be done manually, but preferably with verification tools
Protocol security verification is still a research area
- But experts can do it fairly routinely
“Real” protocols are difficult to analyze for practical reasons
- Specifications are not precise
- They use operators with more complex properties than simple abstract encryption
- Flow of control is more complex - protocols negotiate alternative encryption algorithms and other parameters
- Messages have many fields not relevant to provable security