An automated formal analysis of the security of the internet key exchange (IKE) protocol in the presence of compromising adversaries
Adrian Kyburz · Repository for Publications and Research Data (ETH Zurich) · 2010
Our dependence on sophisticated security services has largely increased in recent years.To address this trend, a lot of research effort has been put into the development and usage of methods for proving security properties of network protocols.To date, many security protocols have already been analyzed by formal methods, using either symbolic computation or complexity theory.One important family of protocols which has only been analyzed in a very limited way is the IKE protocol family.IKE stands for Internet Key Exchange and is the default protocol suite for key management in the IPSec standard.Due to the sheer complexity of the IKE protocol specification, only simplified versions have been subject to formal analysis to date.Previously conducted analyses on IKE are limited to the individual analysis of some of the (many) subprotocols and many of them do not investigate more advanced security properties such as Perfect Forward Secrecy, Key Compromise Impersonation, or the loss of old session keys.This thesis provides the first automatic security analysis of IKEv1 and IKEv2 in the presence of compromising adversaries.We scrutinize the protocols with respect to the loss of session keys, forward secrecy and Key Compromise Impersonation.We describe new attacks against the protocol suites and establish a security hierarchy among the various variants of the protocol.Moreover, our results demonstrate that a tool-supported formal analysis of large-scale security protocols is feasible. This Master's thesis is the culmination of my studies at the Swiss Federal Institute ofTechnology.During the last several years I was given the great opportunity to not only learn about all the fascinating topics the area of Computer Science has to offer, but also to meet a myriad of interesting, and open-minded people who greatly enhanced my horizon.It is thus a pleasure to thank the many people who made this thesis possible.First of all, I would like to thank Dr. Cas Cremers, my supervisor, for being a vibrant source of inspiration and guidance.Without his support and great experience in the area of security protocols and their analysis, this thesis would be very different.