Bhargavan, KarthikeyanKarthikeyanBhargavanBichhawat, AbhishekAbhishekBichhawatDo, Quoc HuyQuoc HuyDoHosseyni, PedramPedramHosseyniKüsters, RalfRalfKüstersSchmitz, GuidoGuidoSchmitzWürtele, TimTimWürtele2025-08-312025-08-312021-01-0110.1007/978-3-030-91631-2_42-s2.0-85119669759https://d8.irins.org/handle/IITG2025/25649DY^⋆ is a recently proposed formal verification framework for the symbolic security analysis of cryptographic protocol code written in the F^⋆ programming language. Unlike automated symbolic provers, 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 DY^⋆ can be executed, and hence, tested, and they can even interoperate with real-world counterparts. 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. In this paper, we provide a tutorial-style introduction to DY^⋆ : We illustrate how to model and prove the security of the ISO-DH protocol, a simple key exchange protocol based on Diffie-Hellman.falseCryptographic protocols | F⋆ | Formal methods | Mechanized proofs | Protocol analysisBook Chapter1611334977-9720212chBook Series3