Design and Formal Analysis of a Lightweight MIPv6 Authentication Scheme

The emergence of mobile IPv6 (MIPv6) significantly affected how we live and work, while it still faces more security threats than traditional wireless networks. On the other hand, most mobile devices have constrained computing and storage resources. The network environment is complex, and the network topology also changes very frequently. Although various security protocols have been proposed for authentication in MIPv6, there are still some challenges. First, most of the subsisting authentication schemes can not work in resource-constrained environments. Second, each of these authentication protocols has some defects, which may lead to serious consequences. So it is valuable and crucial to conduct security analysis at the design stage of protocols. At present, most researchers attempts adopt informal methods, which are not as effective and suitable as formal methods. Some researchers have been conscious of the advantages of using formal methods to verify protocols. However, the approaches are too complex to understand for those who are not familiar with formal methods. In light of these challenges, we propose a lightweight MIPv6 authentication scheme for environments with low resource. We conduct the security analysis and performance comparison of the proposed authentication scheme. In particular, we use the SVO logic to formally analyze its security. We also explain how to use this formal method, which can be regarded as an example to better illustrate the application of formal analysis in MIPv6 authentication schemes.