Introduction
Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes. However, the convenience of electronic elections comes with a risk of large-scale fraud and their security has seriously been questioned. In this project we propose to use formal methods to analyze electronic voting protocols.
Objectives
Formalising protocols and security properties. Electronic voting protocols have to satisfy a variety of security properties that are specific to electronic elections, such as eligibility, verifiability and different kind of anonymity properties. In literature these properties are generally stated intuitively and in natural language. Such informal definitions are at the origin of many security flaws. As a first step we therefore propose to give a formalisation of the different security properties in a well-established language for protocol analysis.
Automated techniques for formal analysis. We propose to design algorithms to perform abstract analysis of a voting system against formally-stated security properties. From preliminary work it has already become clear that privacy preserving properties can be expressed as equivalences. Therefore, we will give a particular attention to automatic techniques for deciding equivalences, such as static and observational equivalence in cryptographic pi-calculi. Static equivalence relies on an underlying equational theory axiomatizing the properties of the cryptographic functions (encryption, exclusive or, ...). Results exist for several interesting equational theories such as exclusive or, blind signature and other associative and commutative functions. However, many interesting equational theories useful for electronic voting are still lacking. We also foresee to investigate a more modular approach based on combination results. More importantly we also plan to develop algorithms for deciding observational equivalence. In particular we aim at symbolic decision procedures for deciding observational equivalence in the case of a bounded number of sessions and we will concentrate on equational theories with applications to electronic voting. We will implement these algorithms in prototypes which are to be included in the AVISPA platform.
Computational aspects. There are two competing approaches to the verification of cryptographic protocols : the formal (also called Dolev-Yao) model and the complexity-theoretic model, also called the computational model, the adversary can be any polynomial time probabilistic algorithm. While the complexity-theoretic framework is more realistic and gives stronger security guarantees, the symbolic framework allows for a higher level of automation. Because of this, e ort has been spent during the last years in relating both frameworks with the goal of getting the best of both worlds. We plan to continue this effort and investigate soundness results for cryptographic primitives related to electronic voting. Moreover, most of the existing results only hold for trace properties, which do not cover most properties in electronic elections. We plan to establish soundness results for these properties.
Case studies. We will validate our results on several case studies from the literature. We also foresee to analyse a real-life case study on an electronic voting protocol recently designed by the Crypto Group of the « Université Catholique de Louvain » (UCL). This protocol will be used in 2009 for the election of the university’s rectorwith more than 5000 voters. However, even if the fundamental needs of security are satisfied, no formal analysis of this protocol has been performed. Another possible case study is an electronic voting protocol designed by France Télécom R&D. This protocol was trialled during the French referendum on the European Constitution in May 2005.
