Colloquium V. Cortier – Tuesday, September 20, 2016

Electronic voting: logic to the rescue

Abstract : The electronic vote must open the same guarantees as the traditional vote at the ballot box. In this purpose, the electronic voting protocols use cryptographic primitives, as in the more traditional case of authentication or key exchange protocols. It is now recognized that all these protocols are difficult to design and verify. Thus, attacks can be discovered years later. Formal models, such as process algebras, Horn clauses or constraint systems, have been successfully used to automatically analyze many protocols. However, electronic voting protocols significantly complicate the task of verification tools. Indeed, they call upon often new and complex primitives (such as homomorphic encryption), new execution schemes and ensure new security properties.