The return routability protocol (RRP) is commonly used in route optimization to secure and authenticate mobile IPv6 signals between the mobile node and its correspondent node. In this paper, the correctness and the security of RRP were verified using a Murphi model checker. The results show that RRP has no failure and is correct. However, it is not secure, because an intruder may impersonate a mobile node. Therefore, the design of RRP needs to be revised to overcome these obstacles.

Key words: Return routability protocol, Murphi model checker, binding update message, route optimization.