Formal specification and security verification of the IDKE protocol using FDR model checking

The IDKE protocol is a mechanism aiming to provide authentication and session-key establishment for mobile nodes after an inter domain handover. Credentials are forwarded from a previous access router to the new access router whereas initially no trust relationship exists. The IDKE protocol utilizes an IP based infrastructure to transfer a session-key due an initiated handover. In this paper, we give a formal specification of the IDKE protocol, its properties, pre- and post-conditions. Verification of security properties such as secrecy and authentication is performed by utilizing the model checker FDR. We optimize the specification, prove security properties, and figure out the limits of our optimized specification. We show that the IDKE protocol is capable to provide authenticated and secured key establishment. Furthermore we prove that the IDKE protocol also provides forward secrecy for the session-key and for a secured tunnel between two access routers.