
Quantum Key Distribution (QKD) protocols achieve information-theoretic security, but their security proofs assume authenticated classical channels. All current ETSI QKD 014-compliant deployments authenticate these channels using classical TLS with RSA or ECDSA certificates — primitives vulnerable to quantum attack via Shor's algorithm. We prove (Theorem 2) that any production QKD deployment using RSA/ECDSA authentication will be retroactively compromised once quantum computers become available. This affects all major QKD vendors (Nokia, ID Quantique, Toshiba, QuantumCTek) and national quantum testbeds worldwide. We present the Post-Quantum Transport Gateway (PQTG), an open-source software gateway that replaces classical TLS on QKD control channels with NIST-standardized post-quantum cryptography (ML-KEM-768, Falcon-512, SPHINCS+-256f). PQTG requires no vendor firmware modifications. Security properties are formally verified with 549 machine-checked theorems in Lean 4. Open source: https://github.com/Paraxiom/pq-transport-gateway (MIT license)
ETSI QKD 014, TLS vulnerability, Quantum Key Distribution, TLS, Post-Quantum Cryptography, Lean 4, harvest-now-decrypt-later, formal verification, Falcon, ML-KEM, SPHINCS+
ETSI QKD 014, TLS vulnerability, Quantum Key Distribution, TLS, Post-Quantum Cryptography, Lean 4, harvest-now-decrypt-later, formal verification, Falcon, ML-KEM, SPHINCS+
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
