TY - GEN

T1 - DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code

AU - Bhargavan, Karthikeyan

AU - Bichhawat, Abhishek

AU - Do, Quoc Huy

AU - Hosseyni, Pedram

AU - Küsters, Ralf

AU - Schmitz, Guido

AU - Würtele, Tim

PY - 2021/11/4

Y1 - 2021/11/4

N2 - We present DY∗, a new formal verification framework for the symbolic security analysis of cryptographic protocol code written in the F∗ programming language. Unlike automated symbolic provers, our framework accounts for advanced protocol features like unbounded loops and mutable recursive data structures, as well as low-level implementation details like protocol state machines and message formats, which are often at the root of real-world attacks. Our work extends a long line of research on using dependent type systems for this task, but takes a fundamentally new approach by explicitly modeling the global trace-based semantics within the framework, hence bridging the gap between trace-based and type-based protocol analyses. This approach enables us to uniformly, precisely, and soundly model, for the first time using dependent types, long-lived mutable protocol state, equational theories, fine-grained dynamic corruption, and trace-based security properties like forward secrecy and post-compromise security. DY∗ is built as a library of F∗ modules that includes a model of low-level protocol execution, a Dolev-Yao symbolic attacker, and generic security abstractions and lemmas, all verified using F∗. The library exposes a high-level API that facilitates succinct security proofs for protocol code. We demonstrate the effectiveness of this approach through a detailed symbolic security analysis of the Signal protocol that is based on an interoperable implementation of the protocol from prior work, and is the first mechanized proof of Signal to account for forward and post-compromise security over an unbounded number of protocol rounds.

AB - We present DY∗, a new formal verification framework for the symbolic security analysis of cryptographic protocol code written in the F∗ programming language. Unlike automated symbolic provers, our framework accounts for advanced protocol features like unbounded loops and mutable recursive data structures, as well as low-level implementation details like protocol state machines and message formats, which are often at the root of real-world attacks. Our work extends a long line of research on using dependent type systems for this task, but takes a fundamentally new approach by explicitly modeling the global trace-based semantics within the framework, hence bridging the gap between trace-based and type-based protocol analyses. This approach enables us to uniformly, precisely, and soundly model, for the first time using dependent types, long-lived mutable protocol state, equational theories, fine-grained dynamic corruption, and trace-based security properties like forward secrecy and post-compromise security. DY∗ is built as a library of F∗ modules that includes a model of low-level protocol execution, a Dolev-Yao symbolic attacker, and generic security abstractions and lemmas, all verified using F∗. The library exposes a high-level API that facilitates succinct security proofs for protocol code. We demonstrate the effectiveness of this approach through a detailed symbolic security analysis of the Signal protocol that is based on an interoperable implementation of the protocol from prior work, and is the first mechanized proof of Signal to account for forward and post-compromise security over an unbounded number of protocol rounds.

U2 - 10.1109/eurosp51992.2021.00042

DO - 10.1109/eurosp51992.2021.00042

M3 - Conference contribution/Paper

SN - 9781665430487

SP - 523

EP - 542

BT - 2021 IEEE European Symposium on Security and Privacy, (Euro S & P) 2021

PB - IEEE

ER -