Heider, T. (2019):Towards a Verifiably Secure Quantum Resistant Key Exchange in IKEv2Recent breakthroughs in the field of quantum computing have sparked fears that the cryptographic methods we rely on every day may be broken in the near future. Even worse, encrypted network communication protocols like the IPsec suite rely on an asymmetric key exchange to derive a set of symmetric keys used to encrypt network traffic. An attacker storing recordings of the key exchange and the following communication can break the key exchange, extract the symmetric keys and compromise the clear text data once a powerful enough quantum computer is available in the future. The goal of this work is to make the IKEv2 protocol and thus the whole IPsec communication quantum-resistant, using novel cryptographic methods collected in the NIST post-quantum standardization project, without introducing new security weaknesses. The challenge lies in the constraints of the new cryptographic schemes, such as enormous key sizes, which the IKEv2 protocol was not designed for. A thorough analysis of the quantum-resistant key exchange methods in regards to their constraints and an analysis of the IKEv2 protocol in terms of its limitations and security properties gives a clear insight of the changes required to support the new methods. Because the security of most methods is unclear, the protocol design should not repeat the mistake to favor a single cryptographic method. Instead, all key exchange schemes should be interchangeable and even combinable in a hybrid key exchange. To ensure the security of the protocol, this work employs a formal analysis driven protocol design approach similar to TLS 1.3. The resulting protocol, named PQ-IKEv2, is the result of a comparison of previous work on the subject and new original ideas. It enables a hybrid key exchange with all NIST post-quantum key exchange contestants. To assert its security properties, it is subjected analysis using the Tamarin prover. A preceding analysis of IKEv2 confirms the results of previous security analysis and is then extended to show that the new PQ-IKEv2 protocol provides the same security against a more powerful quantum computer attacker. A benchmark of a PQ-IKEv2 reference implementation proofs to be usable in real world settings with an added latency of merely 10% for a hybrid ECDH and post-quantum exchange.
|