Mechanized Proof of Resistance of Denial of Service Attacks in Voting Protocol with ProVerif
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.
[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.
[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.
@article{"International Journal of Information, Control and Computer Sciences:50613", author = "Bo Meng and Wei Wang", title = "Mechanized Proof of Resistance of Denial of Service Attacks in Voting Protocol with ProVerif", 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.", volume = "5", number = "12", pages = "1514-6", }
