Abstract: Soundness and coercion resistance are the important and intricate security requirements for remote voting protocols. In this study firstly the review of the formal methods of security protocols is introduced, then applied pi calculus and the automatic tool ProVerif are examined. Thirdly Meng et al. protocol recently proposed is modeled in applied pi calculus. Finally soundness and coercion resistance are verified with automatic tool ProVerif. The result we obtain is that Meng et al. protocol has coercion resistance. But it has not soundness because ProVerif found an attack on soundness. Finally the improvement of Meng et al. protocol is proposed and also modeled in applied pi calculus and automatically analyzed in ProVerif. The result we get is that the improvement of protocol has soundness. To our best knowledge, the first automated analysis of Meng et al. protocol for an unbounded number of honest and corrupted voters is finished.