Events

Salle W,

École Normale Supérieure

45, rue d’Ulm, 75005 — ParisTowards the Automated Verification of Cryptographic Protocol Implementations

Karthikeyan Bhargavan

INRIA — Paris Rocquencourt

Abstract: In recent years, the emergence of effective protocol analyzers and expressive cryptographic models have enabled the proof of large cryptographic protocols, such as Transport Layer Security (TLS) and Kerberos, in abstract but increasingly precise models. A criticism of such proofs is that they provide a false sense of security, since their models do not cover low-level implementation details and may miss entire classes of attacks that rely, for example, on message formats or error handling. Indeed, attacks on mainstream protocol implementations, such as the OpenSSL implementation of TLS, continue to be found despite years of expert review and formal proofs.

We present a line of research that aims to address this gap between formal models and implementations of cryptographic protocols. Our goal is to prove the security of running code, accounting for their concrete details, under precise cryptographic assumptions, and against realistic attackers. The challenge is that protocol implementations are large programs that do far more than simply use cryptographic constructions: they implement complex state machines, they process flexible message formats, and they provide an abstract API to application code.

We identify and formalize a subset of the programming language F# that is well-suited for programming and specifying protocols. Programs (and adversaries) written in this subset can be interpreted both concretely (for execution) and symbolically (for verification). We describe two verification techniques, one relying on model extraction and a specialized cryptographic protocol analyzer, and another on a type system and an general-purpose first-order logic prover. We evaluate these techniques by verifying a series of protocol implementations, including TLS and Web Services Security. We thus present the first security verification results for interoperable implementations of mainstream cryptographic protocols.