Formal security verification of key delivery protocols in quantum key distribution networks : an overview of the security and soundness of the ETSI GS QKD 014 key delivery protocol standard

Abstract

This project presents a formal symbolic analysis of the ETSI GS QKD 014 quantum key delivery protocol using the Tamarin Prover. After situating the protocol within the context of classical cryptography and emerging quantum threats, the work models key agent interactions and message exchanges. The specification captures fundamental entities and communication flows to verify critical security properties, including key integrity, confidentiality, and authenticity. Analysis is performed under the Dolev-Yao adversary model, which characterizes an active eavesdropper with full network control. The Tamarin Prover is utilized to automatically verify these properties. Results demonstrate that the protocol remains secure within this model, assuming no practical quantum attacks currently threaten TLS. The study discusses these findings in light of ongoing advances in quantum computing and cryptography, emphasizing the necessity of hybrid solutions that integrate quantum key distribution with post-quantum cryptographic schemes to guarantee long-term security.