A secure and efficient ID-based registration protocol with user anonymity is proposed in this paper for IP-based mobile networks. The protocol minimizes the registration delay through a minimal usage of the identity (ID)-based signature scheme that eliminates expensive pairing operations. User anonymity is achieved via a temporary identity (TID) transmitted by a mobile user, instead of its true identity. Additional replay protection from a Foreign Agent (FA) is included in the registration messages to prevent a possible replay attack. A formal correctness proof of the protocol using Protocol Composition Logic (PCL) is presented. Numerical analysis and computer simulation results demonstrate that the proposed protocol outperforms the existing ones in terms of the registration delay, the registration signaling traffic, and the computational load on a Mobile Node (MN) while improving security. For example, the proposed protocol reduces the registration delay up to 49.3 percent approximately, comparing to Yang's protocol. © 2010 IEEE.