Electronic Voting: How Logic Can Help

Electronic Voting: How Logic Can Help. Véronique Cortier. In Proceegings of the 12th International Joint Conference on Automated Reasoning (IJCAR 2014), pp. 16–26, LNAI 8562, Vienna, Austria, 2014.

Download

[PDF] [HTML]

Abstract

Electronic voting should offer at least the same guarantees than traditional paper-based voting systems. In order to achieve this, electronic voting protocols make use of cryptographic primitives, as in the more traditional case of authentication or key exchange protocols. All these protocols are notoriously difficult to design and flaws may be found years after their first release. Formal models, such as process algebra, Horn clauses, or constraint systems, have been successfully applied to automatically analyze traditional protocols and discover flaws. Electronic voting protocols however significantly increase the difficulty of the analysis task. Indeed, they involve for example new and sophisticated cryptographic primitives, new dedicated security properties, and new execution structures.
After an introduction to electronic voting, we describe the current techniques for e-voting protocols analysis and review the key challenges towards a fully automated verification.

BibTeX

    @InProceedings{SurveyVote-IJCAR14,
  author = 	 {V\'eronique Cortier},
  title = 	 {Electronic Voting: How Logic Can Help},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {{P}roceegings of the 12th {I}nternational {J}oint
                   {C}onference on {A}utomated {R}easoning (IJCAR 2014)},
  pages = 	 {16-26},
  year = 	 {2014},
  OPTeditor = 	 {},
  volume = 	 {8562},
  OPTnumber = 	 {},
  series = 	 {LNAI},
  address = 	 {Vienna, Austria},
  OPTmonth = 	 {},
  OPTorganization = {},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {},
abstract = {Electronic voting should offer at least the same guarantees than traditional paper-based voting systems. In order to achieve this, electronic voting protocols make use of cryptographic primitives, as in the more traditional case of authentication or key exchange protocols. All these protocols are notoriously difficult to design and flaws may be found years after their first release. Formal models, such as process algebra, Horn clauses, or constraint systems, have been successfully applied to automatically analyze traditional protocols and discover flaws. Electronic voting protocols however significantly increase the difficulty of the analysis task. Indeed, they involve for example new and sophisticated cryptographic primitives, new dedicated security properties, and new execution structures.
\par
After an introduction to electronic voting, we describe the current techniques for e-voting protocols analysis and review the key challenges towards a fully automated verification.
},
    DOI = {10.1007/978-3-319-08587-6_2},
}