Verification of Resistance of Denial of Service Attacks in Extended Applied Pi Calculus with ProVerif

Owning to the damage of denial of service attacks in security protocols, resistance of denial of service attacks plays an important role in remote voting protocols. Recently Meng et al. proposed a secure remote internet voting protocol that claims to satisfy formal definitions of key properties without physical constrains. In this study firstly the review of the formal model of resistance of denial of service attacks in security protocols is introduced, then extended applied pi calculus and Huang et al. formal model are reviewed, after that Meng et al. protocol is modeled in extended applied pi calculus, finally resistance of denial of service attacks is proved with ProVerif. The result we obtain is that Meng et al. protocol is not resistance of denial of service attacks because one denial of service attack is found. At the same time we also propose a method to prevent it from 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 et al. protocol for an unbounded number of honest and corrupted voters.