Secure routing protocols for mobile ad hoc networks have been developed recently yet, it has been unclear what are the properties they achieve, as a formal analysis of these protocols is mostly lacking. In this paper we are concerned with this problem, how to specify and how to prove the correctness of a secure routing protocol. We provide a definition of what a protocol is expected to achieve independently of its functionality, as well as a communication and adversary models. This way, we enablefornial reasoning on the correctness of secure routing protocols. We demonstrate this by analyzing two protocols from the literature.