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.

The recent advances in the development of quantum computers pose a threat to the cryptography used today. While symmetric algorithms can adapt to those challenges, no prevalent key exchange method can protect against quantum computer based attacks. There already exist several new, quantum-resistant approaches. Yet, all of them either lack in confidence regarding their security or require large data to be transmitted. Due to the lack of confidence in these algorithms, researchers tend towards hybrid key exchange methods which combine at least two different algorithms. As long as one of them prevails, the shared secret remains secure. Yet, these hybrid key exchanges together with algorithms which transmit large payloads require significant changes to the design of security protocols. IKEv2 is willing to introduce radical changes in order to support as many different algorithms as possible. This was expected to impact the protocol's operational feasibility, but remained to be tested due to the lack of a working reference implementation of the newly proposed internet drafts. To address this issue, we implemented these drafts using a modified version of the OpenIKED as basis that already comprised the first steps towards the concept's integration. During the implementation we found that several design choices severely hinder a clean and maintainable structure. With the resulting implementation, we tested the adjusted protocol under real-world conditions. The results show that the result generally works but struggles to cope with slow, lossy networks. Based on these insights, we drafted an improved protocol design which also supports the full range of quantum-resistant key exchange methods. In contrast to the current drafts, it promises a cheaper and more maintainable implementation.