Design and Formal Analysis of a Lightweight MIPv6 Authentication Scheme

Document Type


Publication Title

IEEE Internet of Things Journal


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. IEEE

First Page


Last Page




Publication Date



Authentication, Complex networks, Computer circuits, Formal methods, Manganese, Mobile security, Network security, Security systems, Authentication scheme, Formal analysis, Mobile authentication, Mobile-IPv6, Models checking, Routings, Security, Security analysis, SVO logic, SVO logic, Model checking


IR Deposit conditions:

OA version (pathway a): Accepted version

No embargo

When accepted for publication, set statement to accompany deposit (see policy)

Must link to publisher version with DOI

Publisher copyright and source must be acknowledged