A formal analysis of IKEv2's post-quantum extension

Many security protocols used for daily Internet traffic have been used for decades and standardization bodies like the IETF often provide extensions for legacy protocols to deal with new requirements. Even though the security aspects for extensions are carefully discussed, automated reasoning has proven to be a valuable tool to uncover security holes that would otherwise have gone unnoticed. Therefore, Automated Theorem Proving (ATP) is already a customary procedure for the development of some new protocols, e.g., TLS 1.3 and MLS. IKEv2, the key exchange for the IPsec protocol suite, is expected to undergo significant changes to facilitate the integration of Post-Quantum Cryptography. We present the first formal security model for the IKEv2-handshake in a quantum setting together with an automated proof using the Tamarin Prover. Our model focuses on the core state machine, is therefore easily extendable, and aims to promote the use of ATP in IPsec-standardization. The security model captures gaps in the protocol, but treats the specific implementation (like fragmentation mechanisms, for example) as a black box. With IKE_INTERMEDIATE we showcase this approach on a recently proposed extension that significantly changes the protocol's state machine.