Invited speakers: The final program is under construction, here is a first draft.
Sunday, June 28 VETO 2009
8:15 — 08:30 Welcome Slides
8:30 — 10:00 Session 1: Voting Systems Chair:  Ralf Kuesters
8:30 — 9:15 Peter Ryan (University of Luxembourg) Advances in Verifiable Voting Systems
Abstract: It is essential that a voting system provide a high degree of confidence in the accuracy of the outcome. The importance of this as a foundation of democracy has come to prominence in recent years, notably with the 2000 and 2004 US presidential elections, but also the decertification of electronic voting systems in the Netherlands etc. Such assurance is difficult to achieve while at the same time guaranteeing ballot secrecy unless one is prepared to vest a high degree of trust in the process and officials. Recently, considerable progress has been made in developing schemes that do provide strong guarantees of accuracy and privacy with minimal trust assumptions. Such schemes typically make significant use of cryptographic mechanisms. More recent schemes, such a Prêt à Voter or Scantegrity II also provide a fairly simple and familiar voter experience. Such schemes provide a high degree of trustworthiness, but the challenge remains to instill trust in such systems, i.e. convince the stakeholders that they should trust the system.
In this talk I discuss the challenges presented by the design and evaluation of such systems. I will present the notions of voter-verifiability, along with various requirements of voting systems: accuracy, coercion-resistance etc. and outline a number of recent proposals to achieve these properties in a way that is sufficiently usable and understandable to inspire widespread trust.
Slides
9:15 — 10:00 Olivier Pereira (UCL Belgium)Electing a University President using Open-Audit Voting
Abstract: In March 2009, the Universit\'e catholique de Louvain elected its President using a custom deployment of the Helios web-based open-audit voting system. Out of 25,000 potential voters, 5000 registered, and almost 4000 voted in each round of the election. The precision of the voting system turned out to be crucial: in the first round, the leader came short of winning the election by only 2 votes.
We will describe the Helios-based voting system used in this election, the specifics of the UCL deployment, and the lessons learned in this deployment. We note at least one interesting conclusion: while it is often assumed that open-audit voting will lead to more complaints and potentially a denial-of-service attack on the auditing process, we found that, instead, complaints are likely to be more easily handled in open-audit elections because evidence and counter-evidence can be presented.
This is a joint work with Ben Adida and Olivier de Marneffe.
Slides
10:00 — 10:30 Break I
10:30 — 12:00 Session 2: Encryption Scheme, Chair:  Pascal Lafourcade
10:30 — 11:15 Damien Vergnaud (ENS ULM) Traceable Anonymous Encryption (joint work with Julien Cathalo, Malika Izabachène and David Pointcheval)
Abstract: The notion of key privacy for (asymmetric) encryption schemes was formally defined by Bellare, Boldyreva, Desai and Pointcheval in 2001: it states that an eavesdropper in possession of a ciphertext is not able to tell which specific key, out of a set of known public keys, is the one under which the ciphertext was created. Since this notion can potentially be a dangerous tool against public safety, there should exist a tracing authority capable of revoking key privacy when illegal behavior is detected. Prior works on anonymous traceable encryption miss a critical point: an encryption scheme may produce a covert channel which malicious users may use to communicate illegally using ciphertexts that trace back to some honest user.
In this talk, we will examine covert channels in the context of anonymous traceable encryption and we introduce a new primitive termed mediated anonymous traceable encryption that provides confidentiality and anonymity while preventing malicious users to embed subliminal messages in ciphertexts. In our model, all ciphertexts passes through a mediator and our goal is to design protocols where the absence of covert channels is guaranteed as long as the mediator is honest, while semantic security and key privacy continue to hold if the mediator is dishonest. We will give security definitions for this new primitive and two constructions meeting the formalized requirements. These constructions are fairly efficient, with ciphertexts that have logarithmic size in the number of group members and their security analysis require reasonable complexity assumptions in bilinear map groups.
Slides
11:15 — 11:45 Sami Harari (Université du Sud Toulon) FSS-Id/FSA-Id A Fast Safe, Identity Based, Aggregate Signature/Authentication Scheme
Abrstact: The need for Id based signature schemes that can be aggregated is well known and has beeen outlined at veto'08. In this paper a signature scheme is presented. It is analogous to DSA/DSS but relies on the classical RSA problem for its cryptographic strength. Another essential characteristic is that the verifying key can be chosen arbitrarily and therefore can be chosen as an ID string or an e-mail address. Last useful property the scheme can be agregated, simultaneously or sequentially. Verification of the aggregate signature is obtained by taking the product of the signers of the message. Breaking such a system which means producing a verifiable signature without knowing the secret key is as hard as factoring the RSA integer n. This scheme is ``zero knowledge''. This property is obtained by using a random quantity in the signature, with the same entropy as the signature itself.
Slides
11:45 — 12:15 Mouhebeddine BERRIMA (FST-Tunis LIP2) Deciding knowledge in security protocols under some e-voting theories
Abrstact: In the last decade, formal methods have proved their interest when analyzing security protocols. Security protocols require in particular to reason about the attacker knowledge. Two standard notions are often considered in formal approaches: deducibility and indistinguishability relations. The first notion states whether an attacker can learn the value of a secret, while the latter states whether an attacker can notice some difference between protocol runs with different values of the secret. Several decision procedures have been developed so far for both notions but none of them can be applied in the context of e-voting protocols, which require dedicated cryptographic primitives. In this talk, we show that both deduction and indistinguishability are decidable in polynomial time for two theories modeling the primitives of e-voting protocols: Okamoto and Lee et al protocols.
Slides
12:00 — 1:30 Lunch
1:30 — 3:00 Session 3: Evoting Modelling, Chair:  Peter Ryan
2:00 — 2:45 Ralf Kuesters (Trier University) An Epistemic Approach to Coercion-Resistance for Electronic Voting Protocols
Abstract: Coercion resistance is an important and one of the most intricate security requirements of electronic voting protocols. Several definitions of coercion resistance have been proposed in the literature, including definitions based on symbolic models. However, existing definitions in such models are rather restricted in their scope and quite complex.
In this talk, I will report about a new definition of coercion resistance in a symbolic setting, based on an epistemic approach, that we have proposed recently. Our definition is relatively simple and intuitive. It allows for a fine-grained formulation of coercion resistance and can be stated independently of a specific, symbolic protocol and adversary model. As a proof of concept, we apply our definition to three voting protocols. In particular, we carry out the first rigorous analysis of the recently proposed Civitas system. We precisely identify those conditions under which this system guarantees coercion resistance or fails to be coercion resistant. We also analyze protocols proposed by Lee et al. and Okamoto.
Joint work with Tomasz Truderung
Slides Paper
2:45 — 3:30 Mark Ryan (University of Birmingham UK) Requirements conflict in voting protocols
Abrstact: The talk presents work on formalising properties of voting protocols. The requirements of receipt-freeness and vote-verifiability intuitively appear to conflict with each other: vote-verifiability provides proof that the voters vote was counted, and this might constitute a receipt. To resolve the conflict, we show how these properties can be formalised, and give examples from the literature of protocols that satisfy both.
Slides
3:30 — 4:00 Break II
4:00 — 5:30 Session 4: Pratical Evoting Systems, Chair: Olivier Pereira
4:00 — 4:45 Jacques Traoré Towards Practical Coercion-Resistant Electronic Elections
Abrstact: In this talk, we will focus on remote (Internet) voting. We will first introduce a security model for such electronic elections. The emphasis will be on so-called "coercion-resistance" and "universal verifiability". We will then show a practical approach for constructing coercion-resistant and universally verifiable voting systems. Our solution relies on special anonymous signature schemes (a.k.a list signatures or Direct Anonymous Attestation) and is proven secure with respect to our model under the q-Strong Diffie-Hellman (q-SDH) assumption. We will conclude our presentation with a discussion of ongoing research in the area of remote voting.
Slides
4:45 — 5:30 Takoua ABDELLATIF BERRAYANA Mosaic: A secure and practical remote voting system
Abstract: Mosaic is a practical and secure e-voting system. Compared to existent remote e-voting systems, Mosaic is realistic since it deals with availability, ease of usage and scalability in addition to the implementation of an efficient security scheme. Indeed, Mosaic architecture is component-based which helps automating the system management when unresponsiveness or security failures occur. Furthermore, Mosaic comes with convenient tools to voters to cast their votes and to administrators to configure, deploy and control the system at runtime. A performance evaluation on the French Grid 5K demonstrates Mosaic scalability. This is attributed to the optimal security scheme that the system implements and to the execution task parallelization that the system architecture allows for. Joint work with Ahmed ADOUANI
Slides