Formal Methods and Real-World Cryptographic Protocols: Advancing the Verification and Testing Frontiers for Specifications and Implementations

Cryptographic protocols are the backbone of secure digital communication and a key technological pillar of our information society. Yet a long history of attacks exploiting both design flaws and implementation bugs has repeatedly exposed their fragility. This manuscript addresses a central challenge in computer security: how can we achieve higher assurance for cryptographic protocols?

First, we present foundational advances in formal methods, introducing new modeling techniques, verification algorithms, and proof methodologies within the Dolev-Yao model that aim to provide formal security guarantees for cryptographic protocols against a powerful network attacker. Second, we put these methods into practice through large-scale security analyses of widely deployed protocols. In particular, we detail the discovery and remediation of critical vulnerabilities—since fixed—in major protocols, including mobile telephony standards (4G and 5G), industrial control system standards (OPC UA), and the French electronic voting system (FLEP) deployed for national elections. Finally, we address the gap between the formal verification of protocol specifications and the security of their real-world implementations by introducing a novel Dolev-Yao model-guided fuzzing approach. This new software testing paradigm enables the automatic discovery of logical attacks caused by implementation bugs in complex cryptographic protocols. We demonstrate its effectiveness through the detection of several previously unknown vulnerabilities and dozens of bugs in implementations of TLS and SSH—some of the most extensively tested protocols.