Summary

Using formal methods and the Tamarin prover for mathematically proving security properties of communication protocols. Provides strong guarantees, can be automated/tool-assisted, and gives early guidance during design before implementation.