Design and formal security evaluation of NeMHIP: A new secure and efficient network mobility management protocol based on the Host Identity Protocol

NEtwork MObility Basic Support (NEMO BS) is a standardized protocol for managing the mobility of a set of nodes that move together as a whole while having continuous connectivity to the Internet through one or more Mobile Routers (MRs). Because it is based on Mobile IPv6 (MIPv6), it inherits the properties of MIPv6, such as the use of IPsec. However, NEMO BS does not address all the features required by the demanding Intelligent Transportation Systems (ITS) scenario to provide an integrated and global secure mobility management framework. In addition, unlike MIPv6, the routing in NEMO BS is suboptimal, which makes difficult the provision of an adequate service performance. These characteristics make the application of the NEMO BS protocol not optimum in this scenario. An interesting strategy to provide security and good service performance is to consider a protocol that establishes and maintains Security Associations (SAs), such as the Host Identity Protocol (HIP). Different HIP-based approaches have been defined. However, these HIP-based network mobility solutions still present unsolved issues. In this article, we present a secure and efficient network mobility protocol named NeMHIP. NeMHIP provides secure and optimum mobility management and efficient end-to-end confidentiality and integrity protection apart from the basic security properties inherited from HIP. To evaluate the security provisions of NeMHIP, we have conducted a belief-based formal evaluation. The results demonstrate that the defined security goals are achieved by the protocol. Furthermore, we have performed an automated formal evaluation to validate additional security aspects of NeMHIP. Thus, we have modeled NeMHIP using the AVISPA tool and assessed its security when an intruder is present. The results confirm that NeMHIP is a secure protocol that ensures end-to-end confidentiality and integrity without introducing security leaks to the basic HIP. Thus, we have addressed the need found in the literature for providing security and efficiency in the network mobility scenario.