Tool-Assisted Verification of Security Protocols with a Combined Type- and Trace-Based Approach

• Applicant: Professor Dr. Ralf Küsters
• Subject Area: Security and Dependability, Operating-, Communication- and Distributed Systems
• Term: since 2025
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 557128350

Security protocols are essential for securing communication, ensuring privacy, maintaining data integrity as well as for authentication and authorization tasks, and as such, are at the heart of almost all security-critical tasks in our modern society. Such protocols are typically complex and subtle. Informal reasoning about their security can easily overlook attacks and vulnerabilities, as has often been demonstrated in the past. The analysis of security protocols therefore necessitates a rigorous formal approach. The planned project will focus on so-called symbolic analysis, which has been instrumental in formally analyzing various widely-used real-world protocols, including TLS, EMV, FIDO, 5G, and Signal. These analyses have uncovered attacks, leading to protocol improvements and subsequent security proofs of these protocols. Despite these successes, mechanized tools for symbolic analysis still face many challenges along the dimensions of scalability, automation, and expressiveness, and make different trade-offs. Traditionally, symbolic protocol analysis tools are divided into trace- and type-based approaches. In general, trace-based tools balance more towards automation, at the expense of the other challenges, working with fairly abstract modeling languages and examining large portions of protocols all-at-once, while type-based tools require more manual work, but can model protocols in a more fine-grained way, and, by analyzing each protocol step independently, can scale well. Recently, the applicant along with colleagues proposed a new approach for the mechanized analysis of security protocols, called DY*. DY* combines trace- and type-based approaches and aims to benefit from both worlds. In DY*, protocols can be written and analyzed in the full-fledged programming language F*, yielding precise and executable protocol models. Moreover, DY* leverages F*'s rich type system for the modular verification of individual protocol steps, enhancing scalability, while unlike other type-based approaches, it comes with a clear trace-based semantics similar to trace-based approaches. This project aims to further advance the DY* framework and its novel approach along all three dimensions: scalability, automation, and expressivity, establishing DY* as a powerful and versatile new tool for security protocol verification, which combines benefits of so far separate analysis approaches. Using the enhancements developed in this project, we will also perform several case studies on important widely-used protocols and standards of independent interest.

• DFG Programme: Research Grants