A Constructive Analysis of IPsec Master Thesis in Computer Science

Securing today’s Internet communication is one of the most fundamental application of cryptographic techniques, and one of the prevailing protocol suite used for this purpose is IPsec. It consists, among others, of a sub-protocol for key establishment, the second version of the Internet Key Exchange (IKEv2) protocol, and a sub-protocol for secur-ing the traffic, the Encapsulated Security Payload (ESP) protocol. Whereas the ESP protocol is based on the well established encrypt-then-MAC approach, the design of the IKEv2 protocol is more peculiar: while based on the Diffie-Hellman key exchange, that exchange is initially not authenticated. The authentication is postponed to a second round, which at the same time already makes use of that previously negotiated key. Somewhat surprisingly, and despite its practical importance, no comprehensive analysis of the IKEv2 protocol in a coherent framework has been conducted so far. Even though certain aspects of the IKEv2 protocol have been studied in depth in the literature, all analyses either consider significantly simplified protocol variants or neglect important aspects such as the initial lack of authentication. This might partially be explained b