More Web Proxy on the site http://driver.im/

research-article

Formal verification of e-voting: solutions and challenges

Author:

Véronique CortierAuthors Info & Claims

ACM SIGLOG News, Volume 2, Issue 1

Pages 25 - 34

https://doi.org/10.1145/2728816.2728823

Published: 28 January 2015 Publication History

Abstract

In the last ten years, electronic voting has been used in an ever growing number of elections. There are many reasons for this development. First, some election modes require a mechanized way for counting since the number of questions or the number of choices is too large for a manual counting. Electronic voting also allows one to vote from home, possibly avoiding long travels. Sometimes, it simply follows the trend of using Internet in our daily life.

References

[1]

M. Abadi and A. D. Gordon. 1997. A Calculus for Cryptographic Protocols: The Spi Calculus. In Proc. of the 4th ACM Conference on Computer and Communications Security (CCS'97). ACM Press, 36--47.

Digital Library

[2]

Ben Adida. 2008. Helios: Web-based Open-Audit Voting. In USENIX Security'08: 17th USENIX Security Symposium. USENIX Association, 335--348.

Digital Library

[3]

Ben Adida, Olivier de Marneffe, Oliver Pereira, and Jean-Jacques Quisquater. 2009. Electing a university president using open-audit voting: Analysis of real-world use of Helios. In Proceedings of the 2009 conference on Electronic voting technology/workshop on trustworthy elections.

Digital Library

[4]

M. Arapinis, L. Mancini, E. Ritter, and M. Ryan. 2014. Privacy through pseudonymity in mobile telephony systems. In 21st Annual Network and Distributed System Security Symposium (NDSS'14).

[5]

A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.-C. Héam, O. Kouchnarenko, J. Mantovani, S. Mödersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganò, and L. Vigneron. 2005. The AVISPA Tool for the automated validation of internet security protocols and applications. In 17th International Conference on Computer Aided Verification, CAV'2005 (Lecture Notes in Computer Science), Vol. 3576. Springer, 281--285.

Digital Library

[6]

Alessandro Armando, Roberto Carbone, Luca Compagna, Jorge Cuellar, and Llanos Tobarra Abad. 2008. Formal Analysis of SAML 2.0 Web Browser Single Sign-On: Breaking the SAML-based Single Sign-On for Google Apps. In Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering (FMSE 2008). 1--10.

Digital Library

[7]

Michael Backes, Catalin Hritcu, and Matteo Maffei. 2008. Automated Verification of Electronic Voting Protocols in the Applied Pi-calculus. In Proceedings of 21st IEEE Symposium on Computer Security Foundations (CSF 2008),. IEEE, 195--209.

Digital Library

[8]

Jordi Barrat, Esteve, Ben Goldsmith, and John Turner. 2012. International Experience with E-Voting. Technical Report. Norwegian E-Vote Project.

[9]

Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella Béguelin. 2014. Probabilistic Relational Verification for Cryptographic Implementations. In 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'14). 193--206.

Digital Library

[10]

Josh Cohen Benaloh and Moti Yung. 1986. Distributing the Power of a Government to Enhance the Privacy of Voters (Extended Abstract). In Proc. 5th Annual ACM Symposium on Principles of Distributed Computing (PODC'86). ACM, 52--62.

Digital Library

[11]

David Bernhard, Véronique Cortier, Olivier Pereira, Ben Smyth, and Bogdan Warinschi. 2011. Adapting Helios for provable ballot secrecy. In Proceedings of the 16th European Symposium on Research in Computer Security (ESORICS'11) (Lecture Notes in Computer Science), Vol. 6879.

Digital Library

[12]

David Bernhard, Véronique Cortier, Olivier Pereira, and Bogdan Warinschi. 2012. Measuring Vote Privacy, Revisited. In 19th ACM Conference on Computer and Communications Security (CCS'12). ACM.

Digital Library

[13]

David Bernhard, Olivier Pereira, and Bogdan Warinschi. 2012. How Not to Prove Yourself: Pitfalls of the Fiat-Shamir Heuristic and Applications to Helios. In Advances in Cryptology - (ASIACRYPT 2012). 626--643.

Digital Library

[14]

David Bernhard and Ben Smyth. 2013. Ballot privacy and ballot independence coincide. In Proceedings of the 18th European Symposium on Research in Computer Security (ESORICS'13) (Lecture Notes in Computer Science), Springer (Ed.).

[15]

Karthikeyan Bhargavan, Ricardo Corin, Cédric Fournet, and Eugen Zalinescu. 2008. Cryptographically Verified Implementations for TLS. In Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS'08). 459--468.

Digital Library

[16]

Bruno Blanchet. 2005. An Automatic Security Protocol Verifier based on Resolution Theorem Proving (invited tutorial). In 20th International Conference on Automated Deduction (CADE-20).

[17]

Bruno Blanchet, Martín Abadi, and Cédric Fournet. 2005. Automated Verification of Selected Equivalences for Security Protocols. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005). IEEE Computer Society, 331--340.

Digital Library

[18]

Mayla Brusó, Konstantinos Chatzikokolakis, and Jerry den Hartog. 2010. Formal verification of privacy for RFID systems. In CSF'10: 23rd Computer Security Foundations Symposium. IEEE Computer Society, 75--88.

Digital Library

[19]

Rohit Chadha, Ştefan Ciobâcă, and Steve Kremer. 2012. Automated verification of equivalence properties of cryptographic protocols. In 21th European Symposium on Programming (ESOP'12) (LNCS). Springer. To appear.

Digital Library

[20]

Melissa Chase, Markulf Kohlweiss, Anna Lysyanskaya, and Sarah Meiklejohn. 2013. Verifiable Elections That Scale for Free. In 16th International Conference on Practice and Theory in Public-Key Cryptography (PKC 2013) (Lecture Notes in Computer Science), Vol. 7778. Springer, 479--496.

[21]

David Chaum. 2001. Sure vote: Technical overview. In Proceedings of the Workshop on Trustworthy Elections (WOTE 01).

[22]

David Chaum, Aleks Essex, Richard Carback, Jeremy Clark, Stefan Popoveniuc, Alan Sherman, and Poorvi Vora. 2008. Scantegrity: End-to-End Voter-Verifiable Optical-Scan Voting. IEEE Security and Privacy 6, 3 (2008), 40--46.

Digital Library

[23]

Vincent Cheval. 2014. APTE: an Algorithm for Proving Trace Equivalence. In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14) (Lecture Notes in Computer Science). Springer.

[24]

Vincent Cheval, Véronique Cortier, and Antoine Plet. 2013. Lengths may break privacy -- or how to check for equivalences with length. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV'13) (Lecture Notes in Computer Science), Vol. 8043. Springer, 708--723.

[25]

Michael R. Clarkson, Stephen Chong, and Andrew C. Myers. 2008. Civitas: Toward a Secure Voting System. In Proc. IEEE Symposium on Security and Privacy. 354--368.

Digital Library

[26]

Lillie Coney, Joseph L. Hall, Poorvi L. Vora, and David Wagner. 2005. Towards a Privacy Measurement Criterion for Voting Systems. In In National Conference on Digital Government Research.

Digital Library

[27]

Véronique Cortier, David Galindo, Stephane Glondu, and Malika Izabachene. 2013. A generic construction for voting correctness at minimum cost - Application to Helios. Cryptology ePrint Archive, Report 2013/177. (2013).

[28]

Véronique Cortier and Ben Smyth. 2011. Attacking and fixing Helios: An analysis of ballot secrecy. In 24th Computer Security Foundations Symposium (CSF'11). IEEE Computer Society.

Digital Library

[29]

Véronique Cortier and Ben Smyth. 2013. Attacking and fixing Helios: An analysis of ballot secrecy. Journal of Computer Security 21, 1 (2013), 89--148.

Digital Library

[30]

Véronique Cortier and Cyrille Wiedling. 2012. A formal analysis of the Norwegian E-voting protocol. In Proceedings of the 1st International Conference on Principles of Security and Trust (POST'12) (Lecture Notes in Computer Science), Vol. 7215. Springer, 109--128.

Digital Library

[31]

Ronald Cramer, Rosario Gennaro, and Berry Schoenmakers. 1997. A Secure and Optimally Efficient Multi-Authority Election Scheme. In International Conference on the Theory and Application of Cryptographic Techniques (EUROCRYPT'97). 103--118.

Digital Library

[32]

Cas Cremers. 2008. The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. In Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, USA, Proc. (Lecture Notes in Computer Science), Vol. 5123/2008. Springer, 414--418.

Digital Library

[33]

Edouard Cuvelier, Olivier Pereira, and Thomas Peters. 2013. Election Verifiability or Ballot Privacy: Do We Need to Choose?. In Proceedings of the 18th European Symposium on Research in Computer Security (ESORICS'13) (Lecture Notes in Computer Science).

[34]

Jeremy Dawson and Alwen Tiu. 2010. Automating open bisimulation checking for the spi-calculus. In proceedings of IEEE Computer Security Foundations Symposium (CSF 2010).

Digital Library

[35]

Stéphanie Delaune, Steve Kremer, and Mark D. Ryan. 2009. Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security 17, 4 (2009), 435--487.

[36]

doc 2013. Documentations of the code used for the 2013 Parliamentary election in Norway. https://brukerveiledning.valg.no/Dokumentasjon/Dokumentasjon/Forms/AllItems.aspx. (2013).

[37]

Atsushi Fujioka, Tatsuaki Okamoto, and Kazuo Ohta. 1992. A Practical Secret Voting Scheme for Large Scale Elections. In AUSCRYPT'92: Workshop on the Theory and Application of Cryptographic Techniques (LNCS). Springer.

Digital Library

[38]

Kristian Gjøsteen. 2010. Analysis of an internet voting protocol. Cryptology ePrint Archive, Report 2010/380. (2010). http://eprint.iacr.org/.

[39]

Jens Groth. 2004. Evaluating Security of Voting Schemes in the Universal Composability Framework. In 2nd Int. Conference in Applied Cryptography and Network Security (ACNS 2004) (Lecture Notes in Computer Science), Vol. 3089. Springer, 46--60.

[40]

IACR. International association for cryptologic research. Elections page at http://www.iacr.org/elections/.

[41]

Ari Juels, Dario Catalano, and Markus Jakobsson. 2010. Coercion-Resistant Electronic Elections. In Towards Trustworthy Elections: New Directions in Electronic Voting. LNCS, Vol. 6000. Springer, 37--63.

Digital Library

[42]

Steve Kremer, Mark D. Ryan, and Ben Smyth. 2010. Election verifiability in electronic voting protocols. In 15th European Symposium on Research in Computer Security (ESORICS'10) (LNCS). Springer.

Digital Library

[43]

Ralf Küsters, Tomasz Truderung, and Andreas Vogt. 2010. A Game-Based Definition of Coercion-Resistance and its Applications. In CSF'10: 23rd IEEE Computer Security Foundations Symposium. IEEE Computer Society, 122--136.

Digital Library

[44]

R. Küsters, T. Truderung, and A. Vogt. 2012. Clash Attacks on the Verifiability of E-Voting Systems. In 33rd IEEE Symposium on Security and Privacy (S&P 2012). IEEE Computer Society, 395--409.

Digital Library

[45]

Helger Lipmaa. 2014. A Simple Cast-as-Intended E-Voting Protocol by Using Secure Smart Cards. Cryptology ePrint Archive, Report 2014/348. (2014). http://eprint.iacr.org/.

[46]

P. Y. A. Ryan, D. Bismark, J. Heather, S. Schneider, and Z. Xia. 2009. The Pret a Voter Verifiable Election System. IEEE Transactions on Information Forensics and Security (2009).

Digital Library

[47]

Ben Smyth. ProSwapper. http://www.bensmyth.com/proswapper.php.

[48]

Drew Springall, Travis Finkenauer, Zakir Durumeric, Jason Kitcat, Harri Hursti, Margaret MacAlpine, and J. Alex Halderman. 2014. Security Analysis of the Estonian Internet Voting System. In Proc. 21st ACM Conference on Computer and Communications Security (CCS'14).

Digital Library

Cited By

Martínek TMalý M(2024)Evaluation of the I-Voting System for Remote Primary Elections of the Czech Pirate PartyActa Informatica Pragensia10.18267/j.aip.24913:3(395-417)Online publication date: 22-Aug-2024
https://doi.org/10.18267/j.aip.249
Singh HSingh LTiwari S(2022)A Systematic Literature Review on Test Case Prioritization TechniquesInternational Journal of Software Innovation10.4018/IJSI.31226310:1(1-36)Online publication date: 21-Oct-2022
https://dl.acm.org/doi/10.4018/IJSI.312263
Yamamoto KFuruta STsujino Y(2022)A Support System for Collecting/Selecting Topics in Chat Using Context/Physiological InformationInternational Journal of Software Innovation10.4018/IJSI.31150610:1(1-15)Online publication date: 21-Oct-2022
https://dl.acm.org/doi/10.4018/IJSI.311506
Show More Cited By

Recommendations

Frugal bribery in voting

Bribery in elections is an important problem in computational social choice theory. We introduce and study two important special cases of the classical $Bribery problem, namely, Frugal-bribery and Frugal-$bribery where the briber is frugal in nature. By ...
Voting: the perils of polling

It's unusual and more than a bit surprising that in the short term, technologists want to slow down the move to electronic systems while many election officials are ready to speed ahead. If the officials started down the electronic voting path by ...
An Experiment in Approval Voting

The first major experimental comparison of approval voting with regular plurality voting occurred in the 1985 annual election of The Institute of Management Sciences TIMS. In approval voting a person votes for approves of as many candidates as desired, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGLOG News

ACM SIGLOG News Volume 2, Issue 1

January 2015

42 pages

EISSN:2372-3491

DOI:10.1145/2728816

Editor:
Andrzej Murawski
University of Warwick

Issue’s Table of Contents

Copyright © 2015 Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 January 2015

Published in SIGLOG Volume 2, Issue 1

Check for updates

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
465
Total Downloads

Downloads (Last 12 months)10
Downloads (Last 6 weeks)0

Reflects downloads up to 19 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Martínek TMalý M(2024)Evaluation of the I-Voting System for Remote Primary Elections of the Czech Pirate PartyActa Informatica Pragensia10.18267/j.aip.24913:3(395-417)Online publication date: 22-Aug-2024
https://doi.org/10.18267/j.aip.249
Singh HSingh LTiwari S(2022)A Systematic Literature Review on Test Case Prioritization TechniquesInternational Journal of Software Innovation10.4018/IJSI.31226310:1(1-36)Online publication date: 21-Oct-2022
https://dl.acm.org/doi/10.4018/IJSI.312263
Yamamoto KFuruta STsujino Y(2022)A Support System for Collecting/Selecting Topics in Chat Using Context/Physiological InformationInternational Journal of Software Innovation10.4018/IJSI.31150610:1(1-15)Online publication date: 21-Oct-2022
https://dl.acm.org/doi/10.4018/IJSI.311506
Bossard A(2022)The SOF Programming ParadigmInternational Journal of Software Innovation10.4018/IJSI.30996510:1(1-14)Online publication date: 23-Sep-2022
https://dl.acm.org/doi/10.4018/IJSI.309965
Ofori HKang J(2022)Impact of SNS Behavior on Social Commerce Purchase IntentionInternational Journal of Software Innovation10.4018/IJSI.30995910:1(1-12)Online publication date: 30-Sep-2022
https://dl.acm.org/doi/10.4018/IJSI.309959
Kamble KShirgave S(2022)Hybrid Method for Semantic Similarity Computation Using Weighted Components in OntologyInternational Journal of Software Innovation10.4018/IJSI.30973410:1(1-12)Online publication date: 7-Oct-2022
https://dl.acm.org/doi/10.4018/IJSI.309734
Meghzili SChaoui AElmansouri RAlloui BBouabsa A(2022)Formal Verification and Implementation of an E-Voting SystemInternational Journal of Software Innovation10.4018/IJSI.30973110:1(1-22)Online publication date: 30-Sep-2022
https://dl.acm.org/doi/10.4018/IJSI.309731
PANIZO ALONSO LGasco MMARCOS del BLANCO DHermida Alonso JBarrat JAlaiz Moreton H(2021)E-Voting System Evaluation Based on The Council of Europe Recommendations: Helios VotingIEEE Transactions on Emerging Topics in Computing10.1109/TETC.2018.28818919:1(161-173)Online publication date: 1-Jan-2021
https://doi.org/10.1109/TETC.2018.2881891
Belardinelli FCondurache RDima CJamroga WKnapik M(2020)Bisimulations for Verifying Strategic Abilities with an Application to the ThreeBallot Voting ProtocolInformation and Computation10.1016/j.ic.2020.104552(104552)Online publication date: Mar-2020
https://doi.org/10.1016/j.ic.2020.104552
Marcos del Blanco DDuenas-Cid DAláiz Moretón H(2020)E-Voting System Evaluation Based on the Council of Europe Recommendations: nVotesElectronic Voting10.1007/978-3-030-60347-2_10(147-166)Online publication date: 6-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-60347-2_10
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents