fr
Formal analysis of electronic voting protocols ANR     SESUR




Main results of the project

Available here - Only in french.

Research themes

Partners

France Télécom R&D
(until Sept. 2008)
LORIA (Nancy) LSV (Cachan) Verimag (Grenoble)
Francis Klay
Jacques Traoré
Camille Vacher
Mathilde Arnaud
(from Sept. 2009)
Stefan Ciobaca
(from Oct. 2008)
Véronique Cortier
Stéphane Glondu
(from Sept. 2011)
Mounira Kourjieh
(from Sept. 2010)
Ben Smyth
(from Oct. 2010)
Laurent Vigneron
Mathilde Arnaud
(from Sept. 2009)
Gergei Bana
(from April. 2010)
Sergiu Bursuc
(until Sept. 2009)
Vincent Cheval
(from Sept. 2009)
Stefan Ciobaca
(from Oct. 2008)
Hubert Comon-Lundh
Stéphanie Delaune
Florent Jacquemard
Steve Kremer
Antoine Mercier
(until Sept. 2009)
Camille Vacher
(until Sept. 2010)
Scott Cotton
(Jan. 2010-Sept. 2010)
Judicael Courant
(until Sept. 2008)
Jannik Dreier
(from Sept. 2010)
Mathilde Duclos
(from Sept. 2010)
Cristian Ene
Florent Garnier
(Sept. 2008 - Sept. 2009)
Pascal Lafourcade
Yassine Lakhnech
Jean-François Monin

Project description

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 rector with 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

Meetings

Outils

More information are available on the web page of each tool.

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.

— 2009 —

[DKR09b] S. Delaune and S. Kremer and M. Ryan. Verifying Privacy-type Properties of Electronic Voting Protocols. In Journal of Computer Security, 2009.
[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.
[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.
[DKP09] S. Delaune, S. Kremer and O. Pereira. Simulation based security in the applied pi calculus. In FSTTCS'09, 2009.

— 2010 —

[DKR09] S. Delaune and S. Kremer and M. Ryan. Symbolic bisimulation for the applied pi calculus. In Journal of Computer Security, 2010.
[KM09] S. Kremer and L. Mazare. Computationally Sound Analysis of Protocols using Bilinear Pairings. In Journal of Computer Security, 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, M.D. Ryan and B. Smyth. Election verifiability in electronic voting protocols. In ESORICS'10, LNCS, Springer, 2010.
[CFPST10] B. Chevalier, P-A. Fouquez, D. Pointcheval, J. Stern and J. Traoré. On Some Incompatible Properties of Voting Schemes. Towards Trustworthy Election Systems - LNCS, 2010.
[DKR10c] S. Delaune, S. Kremer and M. D. Ryan. Verifying privacy-type properties of electronic voting protocols: a taster. Towards Trustworthy Election Systems - LNCS, 2010.

— 2011 —

[ACD11] M. Arnaud, V. Cortier and S. Delaune. Modelling and Verifying Ad Hoc Routing Protocols. In CADE'11, LNAI, Springer, 2011.
[CCD11] V. Cheval, H. Comon-Lundh and S. Delaune. Trace Equivalence Decision: Negative Tests and Non-determinism. In CCS'11, ACM Press, 2011.
[CDK11] S. Ciobaca, S. Delaune and S. Kremer. Computing knowledge in security protocols under convergent equational theories. In Journal of Automated Reasoning, 2011.
[CS11] V. Cortier and B. Smyth. Attacking and fixing Helios: An analysis of ballot secrecy. In CSF'11, IEEE Comp. Soc. Press, 2011.
[BCPSW11] D. Bernhard, V. Cortier, O. Pereira, B. Smyth, and B. Warinschi. Adapting Helios for provable ballot secrecy. In ESORICS'11, LNCS, Springer, 2011.
[CD11] V. Cortier and S. Delaune. Decidability and combination results for two notions of knowledge in security protocols. In Journal of Automated Reasoning, 2011.
[KMT11] S. Kremer, A. Mercier and R. Treinen. Reducing Equational Theories for the Decision of Static Equivalence. In Journal of Automated Reasoning, 2011.
[BBC11] M. Berrima, N. Ben Rajeb and V. Cortier. Deciding knowledge in security protocols under some e-voting theories. In Theoretical Informatics and Applications, 2011.
[CDGSTTZ11] Véronique Cortier, Jérémie Detrey, Pierrick Gaudry, Frédéric Sur, Emmanuel Thomé, Mathieu Turuani, and Paul Zimmermann. Ballot stuffing in a postal voting system. In Revote'11, 2011.
[CC11] Hubert Comon-Lundh and Véronique Cortier. How to prove security of communication protocols? A discussion on the soundness of formal models w.r.t. computational ones. In STACS'11, 2011.
[FLA11] Laurent Fousse, Pascal Lafourcade and Mohamed Alnuaimi. Benaloh's Dense Probabilistic Encryption Revisited. In AFRICACRYPT'11, 2011.
[CDELL11] Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade and Yassine Lakhnech. Automated Proofs for Asymmetric Encryption. In Journal of Automated Reasoning, 2011.
[DLL11] Jannik Dreier, Pascal Lafourcade and Yassine Lakhnech. Vote-Independence: A Powerful Privacy Notion for Voting Protocols. In FPS'11, 2011.
[SC11] Ben Smyth and Véronique Cortier. A note on replay attacks that violate privacy in electronic voting schemes. INRIA Research report, 2011.

— 2012 —

[CCK12] Rohit Chadha, Stefan Ciobaca and Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. In ESOP'12, 2012.




Page maintained by Stéphanie Delaune.
Last modified: 5 December 2012.
Valid HTML 4.01! Valid CSS!