en
Analyse formelle de protocoles de vote électronique ANR     SESUR




Principaux résultats du projet

Le vote électronique offre de nombreux avantages comme le vote à distance ou l'automatisation de la phase de dépouillement. Cependant, la moindre faille dans un système de vote électronique pourrait conduire à une fraude à grande échelle. L'objectif général du projet était de concevoir des techniques pour analyser la sécurité des protocoles de vote. Nos résultats s'articulent sur quatre principaux plans. L'ensemble des publications du projet est disponible ici.

Suite du projet: Une partie des thèmes de recherche du projet ANR AVOTÉ a été reprise dans le projet ERC ProSecure (Provably secure systems: foundations, design, and modularity) et dans le projet ANR VIP (Programme JCJC) (Verification of Indistinguishability Properties). Le projet ProSecure a pour but de développer des techniques modulaires et génériques pour analyser de nouvelles familles de protocoles de sécurité, et notamment les protocoles de vote. Le projet VIP s'intéresse plus particulièrement à l'analyse de propriétés du type "respect de la vie privée" qui jouent un rôle important dans de nombreuses applications (dont les protocoles de vote).
Une variante d'Helios, appelée Helios-C, est en cours de développement. Cette variante permet d'être conforme aux recommandations de la CNIL (le nom des électeurs ne doit pas être public), tout en garantissant toujours la confidentialité des vote et la vérifiabilité du scrutin, même vis-à-vis d'une urne hébergée sur un serveur malhonnête.

Thématiques de recherche

Participants

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

Description du projet

Le vote électronique offre de nombreux avantages comme par l'exemple l'automatisation de la phase de dépouillement. Cependant, la moindre faille dans un tel protocole pourrait permettre la réalisation d'une fraude å grande échelle. Ces protocoles, dont la sécurité est remise en cause par de nombreuses études, ont donc un besoin crucial d'etre vérifiés.

Formalisation des protocoles et des propriétés de sécurité : Un protocole de vote, pour etre utilisable, doit vérifier un certain nombre de propriétés bien spécifiques. Citons par exemple, les propriétés dites de vérifiabilité ou les propriétés du type anonymat. Ces différentes propriétés sont souvent exprimés en langage naturel. De telles définitions ne sont pas suffisamment précises et sont à l'origine de nombreux problèmes de sécurité. Dans un premier temps, nous proposons de donner des définitions précises et formelles des différentes propriétés de sécurité qu'un protocole devrait satisfaire pour garantir un bon niveau de séurité.

Techniques automatiques pour une analyse formelle. Nous proposons de développer des algorithmes afin de permettre une analyse formelle d'un système de vote. Des travaux récents, réalisés par des membres du projet, ont montré que les différentes propriété du type anonymat pouvaient s'exprimer en termes d'équivalence. Nous donnerons donc une attention toute particulière au développement d'algorithmes permettant d'automatiser ces équivalences, e.g. équivalence statique et équivalence observationnelle. L'équivalence statique repose sur une théorie équationnelle qui permet d'axiomatiser les propriétés des primitives cryptographiques (chiffrement, ou exclusif, ...). Des résultats de décision, permettant de décider cette équivalence pour plusieurs théories équationnelles intéressantes existent à l'heure actuelle (e.g. ou exclusif, signature en aveugle). Cependant, de nombreuses théories équationnelles ayant des applications dans le cadre des protocoles de vote électronique n'ont pas été étudiées. Nous souhaitons aussi mettre en place une approche modulaire en développant des résultats de combinaison. Enfin, nous proposons de développer des procédures permettant de décider l'équivalence observationnelle. Pour obtenir de tels résultats, nous pensons nous restreindre au cas d'un nombre borné de sessions et nous concentrer sur les théories pertinentes au vue de notre application. Nous implémenterons ces algorithmes et nous les intègrerons dans la plate-forme AVISPA.

Aspects computationnels. Il existe deux approches très différentes pour la vérification des protocoles cryptographiques: celle basée sur les modèles dits formels, également appelée modèle à la Dolev-Yao, et une approche dite computationnelle. Dans cette dernière approche, l'adversaire est représenté par n'importe quel algorithme probabiliste s'exécutant en temps polynomial. L'approche dite computationnelle est plus réaliste et permet d'obtenir des garanties de sécurité plus élevéss. D'un autre côté l'approche formelle permet une automatisation des preuves de sévurité ce qui constitue un avantage non néligeable. Ces dernières années, un important effort a permis de rapprocher ces deux modèles. Le but d'un tel rapprochement est de bénéficier du meilleur des deux approches. Nous proposons de continuer ce travail en nous intéressant de plus près aux primitives cryptographiques utilisées dans les protocoles de vote électronique. De plus, les résultats existant à l'heure actuelle concernent essentiellement des propriétés dites de trace. Il serait donc intéressant d'établir de tels résultats pour d'autres types de propriétés, comme les propriétés d'équivalence.

Études de cas. Nous validerons nos résultats sur plusieurs études de cas issues de la littérature. Nous prévoyons aussi d'analyser un protocole de vote réel, développé récemment par le Crypto Group de l'Université Catholique de Louvain (UCL). Ce protocole sera utilisé en 2009 pour l'élection du recteur de l'UCL avec plus de 5000 votants. Même si les propriétés fondamentales de sécurité semblent être satisfaites, aucune analyse formelle n'a été réalisée à l'heure actuelle sur ce protocole. Une autre étude de cas possible est un protocole développé récemment par une équipe de France Télécom. Ce protocole a été utilisé en France, en mai 2005, lors du référendum sur la constitution Europénne. De nouveau, aucune analyse formelle n'a été réalisée à l'heure actuelle.

Une présentation plus détaillée est donnée dans le texte complet du projet.

Rapports

Réunions

Outils

Plus d'informations sont disponibles sur la page web de chacun de ses outils.

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 maintenue par Stéphanie Delaune.
Dernières modifications : 5 décembre 2012.
Valid HTML 4.01! Valid CSS!