|
|
|
|
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.
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.
— 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.
|
