Abstract: Secure remote internet voting protocols play an important role in electronic government. Owning to the huge damage and hard to prevention of denial of service attacks in security protocols, resistance of denial of service attacks occupy a tiny space and is intricate security requirements for remote voting protocols. Meng protocol is one of the most important remote internet voting protocols that claims to satisfy formal definitions of key properties. In this study firstly the review of the formal model of resistance of denial of service attacks in security protocol are introduced. Then extended applied pi calculus, the mechanized proof tool ProVerif and Huang’s formal model are examined. After that Meng protocol is modeled in extended applied pi calculus. Finally resistance of denial of service attacks is analyzed with ProVerif. The results we obtain are that Meng protocol is not resistance of denial of service attack because one denial of service attacks is found by us. At the same time we give the method against the denial of service attack. To our best knowledge we are conducting the first mechanized proof of resistance of denial of service attacks in Meng protocol for an unbounded number of honest and corrupted voters.