Paper 2023/1753

Formal verification of the post-quantum security properties of IKEv2 PPK (RFC 8784) using the Tamarin Prover

Abstract

The Internet Key Exchange version 2 (IKEv2) (RFC 7296) is a component of IPsec used to authenticate two parties (the initiator and responder) to each other and to establish a set of security parameters for the communications. The security parameters include secret keys to encrypt and authenticate data as well as the negotiation of a set of cryptographic algorithms. The core documentation uses exclusively Diffie-Hellman exchanges to agree the security information. However, this is not a quantum-secure option due to the ability of Shor's algorithm to break the security assumption underlying the Diffie-Hellman. A post-quantum solution is to include a preshared key in the exchange, as proposed by the extension RFC 8784; assuming that this preshared key has sufficient entropy, the keys created in the IKEv2 exchange will be resistant to a quantum computer. In this paper, we investigate the security claims of RFC 8784 using formal verification methods. We find that keys created using the preshared key are secret from an adversary. However, certain authentication properties of the protocol that are weakened under the assumption that Diffie-Hellman is insecure are not recovered using the preshared key.

Note: 12 pages. Github repository available here: https://github.com/sophie-arqit/ikev2-rfc8784-tamarin-analysis