Beyond the Quantum Promise: A Security Analysis of Classical Control in Quantum Key Distribution

Abstract

Quantum Key Distribution (QKD) protocols provide information-theoretic security by using quantum mechanical principles. Yet QKD is fundamentally a hybrid protocol: its security depends on the correct integration of the quantum phase with classical post-processing. While ETSI and ITU-T specifications standardize QKD architectures and interfaces, they evaluate protocol security in isolation, leaving cross-layer interactions as an underexplored attack surface. This paper introduces a formal verification framework that holistically models QKD protocols based on ETSI and ITU-T QKD specifications. Our model is the first hybrid QKD protocol model that supports automated analysis of protocol-level security focusing on how classical operations influence the security guarantees provided by the quantum layer.