A Tutorial-Style Introduction to $$\textsf {DY}^\star $$

\(\textsf {DY}^\star \) is a recently proposed formal verification framework for the symbolic security analysis of cryptographic protocol code written in the \(\textsf {F}^\star \) programming language. Unlike automated symbolic provers, \(\textsf {DY}^\star \) 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 \(\textsf {DY}^\star \) can be executed, and hence, tested, and they can even interoperate with real-world counterparts. \(\textsf {DY}^\star \) 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.