Electronic voting : How logic can help

Véronique Cortier is CNRS research director at Loria (Nancy, France). In 2003, she received her Ph.D. degree in Computer Science from the École Normale Supérieure de Cachan, from which she graduated. She served as Program Chair of CSF 2012 and CSF 2013 and she is editorial member of TISSEC/TOPS, JCS, and Information and Computation. Her research focuses on formal verification of security systems, in particular e-voting. She has co-authored more than 80 publications on these topics. In 2010, she was awarded an ERC starting grant and in 2015, she received the INRIA - Académie des Sciences young researcher award.

Résumé :

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 will describe the current techniques for e-voting protocols analysis and review the key challenges towards a fully automated verification.