Abstract: Existing anonymous routing protocols have only had unsatisfactory anonymity analysis in MANETs, because adversarial models have not been given exactly，the security definition of cryptographic primitives have not been described, and rigorous proofs are lacking. To address this problem a typical anonymous dynamic source routing protocol is improved, and the formal treatment of this protocol is then proposed in this paper. The static attack power is defined for adversarial models to clarify the capacity of adversaries, and the anonymity of a routing protocol is to be achieved if the identities of end users are unlikable to data packets. According to this definition, a UC-style ideal functionality for route discovery process and the one for data transmission process are defined respectively. The route discovery process is modified to get private paths by generating UC-secure session-keys, which realizes the ideal functionality for route discovery. Then, verifiable lightweight route onions are constructed to realize the ideal functionality for data transmission, i.e., the route onions can verify that upstream nodes shuffle data packets correctly and downstream paths are intact. Finally, the anonymity of the improved protocol is proved in the universal composition framework. The methodology used is also suitable for designing and analyzing other anonymous routing protocols in wireless networks.