We present a unilateral authentication protocol for protecting IPv6 networks against abuse of mobile IPv6 primitives. The proposed protocol imposes minimal computational requirements on mobile nodes, uses as few messages as possible. It is also easy to implement, economic to deploy and lightweight in use. We formally verifies the correctness of the protocol using the finite-state analysis tool mur
, which has been used previously to analyze hardware designs and security properties of several protocols.