by Bhargavan, Karthikeyan and Bichhawat, Abhishek and Do, Quoc Huy and Hosseyni, Pedram and Küsters, Ralf and Schmitz, Guido and Würtele, Tim
Abstract:
$}{\$\backslashtextsf \DY\^\backslashstar $}{\$DY⋆is a recently proposed formal verification framework for the symbolic security analysis of cryptographic protocol code written in the $}{\$\backslashtextsf \F\^\backslashstar $}{\$F⋆programming language. Unlike automated symbolic provers, $}{\$\backslashtextsf \DY\^\backslashstar $}{\$DY⋆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. Protocols modeled in $}{\$\backslashtextsf \DY\^\backslashstar $}{\$DY⋆can be executed, and hence, tested, and they can even interoperate with real-world counterparts. $}{\$\backslashtextsf \DY\^\backslashstar $}{\$DY⋆extends a long line of research on using dependent type systems 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. With this, one can 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.
Reference:
A Tutorial-Style Introduction to $}{\$\backslashtextsf \DY\^\backslashstar $}{\$ (Bhargavan, Karthikeyan and Bichhawat, Abhishek and Do, Quoc Huy and Hosseyni, Pedram and Küsters, Ralf and Schmitz, Guido and Würtele, Tim), Chapter in (Dougherty, Daniel, Meseguer, José, Mödersheim, Sebastian Alexander, Rowe, Paul, eds.), Springer International Publishing, 2021.
Bibtex Entry:
@Inbook{Bhargavan2021,
author="Bhargavan, Karthikeyan
and Bichhawat, Abhishek
and Do, Quoc Huy
and Hosseyni, Pedram
and K{\"u}sters, Ralf
and Schmitz, Guido
and W{\"u}rtele, Tim",
editor="Dougherty, Daniel
and Meseguer, Jos{\'e}
and M{\"o}dersheim, Sebastian Alexander
and Rowe, Paul",
title="A Tutorial-Style Introduction to {\$}{\$}{\backslash}textsf {\{}DY{\}}^{\backslash}star {\$}{\$}",
bookTitle="Protocols, Strands, and Logic: Essays Dedicated to Joshua Guttman on the Occasion of his 66.66th Birthday",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="77--97",
abstract="{\$}{\$}{\backslash}textsf {\{}DY{\}}^{\backslash}star {\$}{\$}DY⋆is a recently proposed formal verification framework for the symbolic security analysis of cryptographic protocol code written in the {\$}{\$}{\backslash}textsf {\{}F{\}}^{\backslash}star {\$}{\$}F⋆programming language. Unlike automated symbolic provers, {\$}{\$}{\backslash}textsf {\{}DY{\}}^{\backslash}star {\$}{\$}DY⋆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. Protocols modeled in {\$}{\$}{\backslash}textsf {\{}DY{\}}^{\backslash}star {\$}{\$}DY⋆can be executed, and hence, tested, and they can even interoperate with real-world counterparts. {\$}{\$}{\backslash}textsf {\{}DY{\}}^{\backslash}star {\$}{\$}DY⋆extends a long line of research on using dependent type systems 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. With this, one can 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.",
isbn="978-3-030-91631-2",
doi="10.1007/978-3-030-91631-2_4",
url="https://doi.org/10.1007/978-3-030-91631-2_4"
}