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. More precisely, we structure the project around four work-packages.

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.

More details are available in the full text of the proposal.

Reports

Web site. January 2008.

D1.1: Specificities of voting protocols. January 2009.
D2.1: Algorithms for static equivalence. September 2009.
D3.1: Soundness of static equivalence. March 2010.
D1.2: Formalising security properties in electronic voting protocols. April 2010.

Meetings

Workshop VETO'09
Kick-off meeting (Cachan, 18 January 2008).
Meeting (Cachan, 12 September 2008).
Meeting (Cachan, 9 September 2009).

Publications

— 2008 —
[DRS08]	S. Delaune, M. Ryan and B. Smyth. Automatic verification of privacy properties in the applied pi-calculus. In IFIPTM'08, IFIP Conference Proceedings. Springer, 2008.
[DKR08a]	S. Delaune, S. Kremer and M. Ryan. Composition of Password-based Protocols. In CSF'08, IEEE Comp. Soc. Press, 2008.
[CLC08a]	V. Cortier and H. Comon-Lundh. Computational soundness of observational equivalence. In FCC'08, 4th Workshop on Formal and Computational Cryptography, 2008.
[CLC08b]	V. Cortier and H.Comon-Lundh. Computational soundness of observational equivalence. In CCS'08, 15th ACM Conference on Computer and Communications Security, 2008.
[Laf08a]	P. Lafourcade. Relation between Unification Problem and Intruder Deduction Problem. In Secret'08, 3rd Workshop on Security and Rewriting Techniques, 2008.
[CDELL08a]	J. Courant, M. Daubignard, C. Ene, P. Lafourcade and Y. Lakhnech. Automated Proofs for Asymmetric Encryption. In FCC'08, 4th Workshop on Formal and Computational Cryptography, 2008.
[CDELL08b]	J. Courant, M. Daubignard, C. Ene, P. Lafourcade and Y. Lakhnech. Automated Proofs for Asymmetric Encryption. In FCS-ARSPA-WITS'08, Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, 2008.
[CDELL08c]	J. Courant, M. Daubignard, C. Ene, P. Lafourcade and Y. Lakhnech. Towards Automated Proofs for Asymmetric Encryption Schemes in the Random Oracle Model. In CCS'08, 15th ACM Conference on Computer and Communications Security, 2008.
[KV08]	F. Klay and L. Vigneron. Automatic Methods for Analyzing Non-Repudiation Protocols with an Active Intruder. In FAST'08, 5th International Workshop on Formal Aspects in Security and Trust, 2008.
[CFPST08]	B. Chevalier, P-A. Fouquez, D. Pointcheval, J. Stern and J. Traoré. On Some Incompatible Properties of Voting Schemes. Towards Trustworthy Election Systems - LNCS, 2008.
— 2009 —
[DKR09b]	S. Delaune and S. Kremer and M. Ryan. Verifying Privacy-type Properties of Electronic Voting Protocols. In Journal of Computer Security, 2009.
[DKR09]	S. Delaune and S. Kremer and M. Ryan. Symbolic bisimulation for the applied pi calculus. In Journal of Computer Security, To appear.
[KM09]	S. Kremer and L. Mazare. Computationally Sound Analysis of Protocols using Bilinear Pairings. In Journal of Computer Security, To appear.
[BCK09]	M. Baudet and V. Cortier and S. Kremer. Computationally Sound Implementations of Equational Theories against Passive Adversaries. In Information and Computation, 2009.
[Cor09]	V. Cortier. Verification of Security Protocols (Invited tutorial). In VMCAI'09, 10th Conference on Verification, Model Checking, and Abstract Interpretation, 2009.
[CDK09]	R. Chadha and S. Delaune and S. Kremer. Epistemic Logic for the Applied Pi Calculus. In FMOODS/FORTE'09, IFIP International Conference on Formal Techniques for Distributed Systems, 2009.
[BCD09]	M. Baudet and V. Cortier and S. Delaune. YAPA: A generic tool for computing intruder knowledge. In RTA'09, 20th International Conference on Rewriting Techniques and Applications, 2009.
[CDK09a]	S. Ciobaca and S. Delaune and S. Kremer. Computing knowledge in security protocols under convergent equational theories. In Secret'09, 4th International Workshop on Security and Rewriting Techniques, 2009.
[ACD09]	M. Arnaud and V. Cortier and S. Delaune. Modeling and Verifying Ad Hoc Routing Protocol. In secret'09, 4th International Workshop on Security and Rewriting Techniques, 2009.
[ML09]	S. Malladi and P. Lafourcade. Prudent engineering practices to prevent type-flaw attacks under algebraic properties. In secret'09, 4th International Workshop on Security and Rewriting Techniques, 2009.
[GLLS09]	M. Gagné and P. Lafourcade and Y. Lakhnech and R. Safavi-Naini. Automated Proofs for Encryption Modes. In FCC'09, 5th International Workshop on Formal and Computational Cryptography, 2009.
[CD09]	V. Cortier and S. Delaune. A method for proving observational equivalence. In CSF'09, IEEE Comp. Soc. Press, 2009.
[CDK09b]	S. Ciobaca and S. Delaune and S. Kremer. Computing knowledge in security protocols under convergent equational theories. In CADE'09, 22nd International Conference on Automated Deduction, 2009.
[BBC09]	M. Berrima and N. Ben Rajeb and V. Cortier. Deciding knowledge in security protocols under some e-voting theories. INRIA Research Report RR-6903, 2009.
[GLLS09]	M. Gagne and P. Lafourcade and Y. Lakhnech and R. Safavi-Naini. Automated Proofs for Encryption Modes. IN ASIAN'09, 13th Annual Asian Computing Science Conference Focusing on Information Security and Privacy: Theory and Practice, 2009.
[BDC09]	S. Bursuc, S. Delaune and H. Comon-Lundh. Deducibility constraints. In ASIAN'09, 13th Annual Asian Computing Science Conference Focusing on Information Security and Privacy: Theory and Practice, 2009.
[KMT09]	S. Kremer, A. Mercier and R. Treinen. Reducing Equational Theories for the Decision of Static Equivalence. IN ASIAN'09, 13th Annual Asian Computing Science Conference Focusing on Information Security and Privacy: Theory and Practice, 2009.
[JKV09]	F. Jacquemard, F. Klay and C. Vacher. Rigid Tree Automata. In LATA'09, LNCS 5457, pages 446-457, 2009.
[SRKK09]	B. Smyth, M. D. Ryan, S. Kremer and M. Kourjieh. Election verifiability in electronic voting protocols (Preliminary version). In WISSEC'09, 2009.
[KV09]	F. Klay and L. Vigneron. Automatic Methods for Analyzing Non-Repudiation Protocols with an Active Intruder. In FAST'08, 5th International Workshop on Formal Aspects in Security and Trust, Revised Selected Papers - LNCS. 2009.
[ELN09]	Cristian Ene, Yassine Lakhnech and Van Chan Ngo. Formal Indistinguishability Extended to the Random Oracle Model. In ESORICS'09, 2009.
[LTV09]	Pascal Lafourcade, Vanessa Terrade and Sylvain Vigier. Comparison of Cryptographic Verification Tools Dealing with Algebraic Properties. In FAST'09, 6th International Workshop on Formal Aspects in Security and Trust, 2009.
[CFPST09]	B. Chevalier, P-A. Fouquez, D. Pointcheval, J. Stern and J. Traoré. On Some Incompatible Properties of Voting Schemes. Towards Trustworthy Election Systems - LNCS, 2009.
[DKR09c]	S. Delaune, S. Kremer and M. D. Ryan. Verifying privacy-type properties of electronic voting protocols: a taster. Towards Trustworthy Election Systems - LNCS, 2009.
[DKP09]	S. Delaune, S. Kremer and O. Pereira. Simulation based security in the applied pi calculus. In FSTTCS'09, 2009.
— 2010 —
[SRKK10]	B. Smyth, M. D. Ryan, S. Kremer and M. Kourjieh. Towards automatic analysis of election verifiability properties. In ARSPA-WITS'10, LNCS. Springer, 2010.
[ACD10]	M. Arnaud, V. Cortier and S. Delaune. Modelling and Verifying Ad Hoc Routing Protocols. In CSF'10, IEEE Comp. Soc. Press, 2010.
[CCD10]	V. Cheval, H. Comon-Lundh and S. Delaune. Automating security analysis: symbolic equivalence of constraint systems. In IJCAR'10, LNCS, Springer, 2010.
[KSR10]	S. Kremer, B. Smyth and M. D. Ryan. Election verifiability in electronic voting protocols. In ESORICS'10, LNCS, Springer, 2010.

Page maintained by Stéphanie Delaune.
Last modified: 21 June 2010.

Research themes

Partners

Project description

Reports

Meetings

Publications

— 2008 —

— 2009 —

— 2010 —