Mechanized Proof of Resistance of Denial of Service Attacks in Voting Protocol with ProVerif

Authors: Bo Meng, Wei Wang

Abstract:

Resistance of denial of service attacks is a key security requirement in voting protocols. Acquisti protocol plays an important role in development of internet voting protocols and claims its security without strong physical assumptions. In this study firstly Acquisti protocol is modeled in extended applied pi calculus, and then resistance of denial of service attacks is proved with ProVerif. The result is that it is not resistance of denial of service attacks because two denial of service attacks are found. Finally we give the method against the denial of service attacks.

Keywords: Applied pi calculus, protocol state, symbolic model, availability.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1329913

References:

[1] A.Acquisti. Receipt-Free Homomorphic Elections and Write-in Voter Verified Ballots. Technical Report 2004/105. International Association for Cryptologic Research, May 2, 2004, and Carnegie Mellon Institute for Software Research International, CMU-ISRI-04-116, 2004.
[2] M.R.Clarkson, S. Chong, and A.C. Myers, "Civitas: Toward a secure voting system," In Proceeding of the 2008 IEEE Symposium on Security and Privacy, Oakland, California, USA, 2008, p.354-368.
[3] B.Meng,"A critical review of receipt-freeness and coercion-resistance". Information Technology Journal, vol.8, vol.8, no. 7, pp. 934-964, 2009.
[4] B.Meng, "A secure non-interactive deniable authentication protocol with strong deniability based on discrete logarithm problem and its application on internet voting protocol," Information Technology Journal, vol.8, no.3, pp. 302-309, 2009.
[5] B.Meng, Z. Li ,and J. Qin, " A receipt-free coercion-resistant remote internet voting protocol without physical assumptions through deniable encryption and trapdoor commitment scheme," Journal of software, vol.5, no.9, pp. 942-949, 2010.
[6] C.Meadows , "A cost-based framework for analysis of denial of service networks," Journal of Computer Security, vol.9, no.1/2, pp. 143-164, 2001.
[7] C.F.Yu ,and V.D. Gligor, 1990. "A formal specification and verification method for the prevention of denial of service," Journalc on communictions, to be published.
[8] B.Meng ,and W.Huang, "Automated Proof of Resistance of Denial of Service Attacks with Theorem Prover," Journalc on communictions, to be published.
[9] E.Bacic, and M. Kuchta, "Considerations in the preparation of a set of availability criteria," In Proceedings of 3rd Annual Canadian Computer Security Symposium, Ottawa, Canada, 1991,p. 283-292.
[10] J.K.Millen, "A Resource Allocation Model for Denial of Service Protection," Journal of Computer Security, vol.2, no.2-3, pp. 89-106, 1993.
[11] V.Ramachandran, Analyzing DoS-resistance of protocols using a costbased framework, Technical Report DCS/TR-1239, Harlow, Yale University, USA, 2002.
[12] J.Smith, J.M. Gonzalez-Nieto, and C. Boyd, "Modelling denial of service attacks on JFK with Meadows-s cost-based framework," In Proceedings of the 2006 Australasian workshops on Grid computing and e-research, Australia, 2006, p.125-134.
[13] S.Tritilanunt, C. Boyd, E. Foo, and J.M.G. Nieto, "Cost-based and timebased analysis of DoS-resistance in HIP," In Proceedings of the thirtieth Australasian conference on Computer science, 2007, p.191-200.
[14] W.Huang ,and B.Meng, "Automated Proof of Resistance of Denial of Service Attacks in Remote Internet Voting Protocol with Extended Applied Pi Calculus,"Information Technology Journal, vol.10, no.8, pp. 1468-1483, 2011.
[15] F.Cuppens ,and C. Saurel, "Towards a formalization of availability and denial of service,". In Proceedings of In Information Systems Technology Panel Symposium on Protecting Nato Information Systems in the 21st Century, Washington, 1999.
[16] A.Gabillon, and L. Gallon, "An Availability Model for Avionic Data Buses," In Proceedings of. Workshop on Issues in Security and Petri Nets. University of Eindhoven, Netherlands, 2003.
[17] B.Meng,W.Huang,and D.J.Wang "Automatic Verification of Remote Internet Voting Protocol in Symbolic Model," Journal of Networks, Vol 6, No. 9 pp. 1262-1271, 2011.