Dolev-Yao

• Formal Verification of Cryptographic Protocols: ProVerif, Tamarin, and the TLS 1.3 Verification Story · 2023-04-06

  An exploration of the Dolev-Yao model, ProVerif and Tamarin provers, computational soundness results, and how formal methods proved TLS 1.3 secure before deployment.