A formal analysis of IKEv2’s post-quantum extension
Stefan-Lukas Gazdag, Sophia Grundner-Culemann, Tobias Guggemos, Tobias Heider, Daniel Loebenberger · Annual Computer Security Applications Conference · 2021
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.