Source: http://www.lsv.fr/Projects/anr-avote/
Timestamp: 2019-04-19 20:13:34+00:00

Document:
Available here - Only in french.
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.
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.
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.
D2.2: Algorithms for observational equivalence. December 2010.
D4.1: Formal description of our case study: Helios 2.0. February 2011.
D4.2: Results on case studies from literature. February 2011.
D2.3: Implementation of prototypes for equivalence properties. January 2012.
D4.3: Results on a real life case study - Helios 2.0. January 2012.
D3.2: Soundness in presence of active adversaries. January 2012.
Poster - Grand Colloque STIC 2012. January 2012.
Kick-off meeting (Cachan, 18 January 2008).
Meeting (Cachan, 12 September 2008).
Meeting (Cachan, 9 September 2009).
Meeting (Cachan, 10 December 2010).
PhD defenses (Cachan, 9 December 2011).
More information are available on the web page of each tool.
YAPA is a tool dedicated to the analysis of deducibility and static equivalence.
KISS is a tool for deciding deduction and static equivalence under certain convergent term rewriting systems.
AKiSs is a tool for automatically checking trace equivalence for a bounded number of sessions in cryptographic protocols.
ADECS decides symbolic trace equivalence where the inputs are given as deducible constraint systems.
[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.
[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.
[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.
[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.
[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.

References: V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V.