Abstract: Authentication protocols are often adopted to reduce the security threats in mobile ad hoc network(MANET). However, a vulnerable protocol might bring more serious threats to MANET. As a result, formal verifications of security protocols become more important. An approach based on the communicating sequential process (CSP) and Model Checking tool FDR was proposed to model and verify a typical authentication protocol of MANET, callced TAM. First, the communication behaviors of all participants in TAM and its security (authentication and confidentiality) specifications were formally modeled using CSP. Second, based on these models, the participants’ behaviors were verified by FDR and the verification result indicates that the original TAM could not guarantee authentication and confidentiality. Finally, an improvement was proposed and the experiment result shows that the improved TAM satisfies security goals and increases an acceptable consumption in the case of a reasonable size of clusters compared with the original TAM.