Full Program »
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. With IKE_INTERMEDIATE
we showcase this approach on a recently proposed extension that significantly
changes the protocol’s state machine.