From provable models to provable implementations: translating Alice & Bob security protocols to F*

Deploying secure communication protocols remains a challenging task. To ensure that intended security properties hold, formal verification has become increasingly important. In this work, we present a translation from the design-oriented Alice & Bob language to the implementation-level language F*, leveraging the DY* library’s verification capabilities. Our approach addresses the expressiveness gap between abstract specifications and concrete implementations by generating verifiable DY* code that benefits from its dependent-type system. This integration of model-driven development with dependent types enables the specification and proof of security properties directly at the implementation level. As a result, users, even those without expertise in formal methods, can start from an intuitive Alice & Bob notation and obtain a formally backed implementation that can be enriched with features not expressible in Alice & Bob, while preserving correctness through re-verification. We demonstrate the effectiveness of this workflow through the generation and verification of several real-world security protocols, showcasing an end-to-end approach to verified protocol implementation.