Security Protocol Verification: Symbolic and Computational Models

Bruno Blanchet (1)

1 PROSECCO - Programming securely with cryptography

Security protocol verification has been a very active research area since the 1990s. This paper surveys various approaches in this area, considering the verification in the symbolic model, as well as the more recent approaches that rely on the computational model or that verify protocol implementations rather than specifications. Additionally, we briefly describe our symbolic security protocol verifier ProVerif and situate it among these approaches.

Domaines: Cryptographie et sécurité [cs.CR]

Bruno Blanchet. Security Protocol Verification: Symbolic and Computational Models. First Conference on Principles of Security and Trust (POST'12), 2012, Tallinn, Estonia. pp.3--29. ⟨hal-00863388⟩