presentation - esorics 2014

Election Verifiability for Helios under Weaker
Trust Assumptions
´
´
Veronique
Cortier, David Galindo, Stephane
Glondu, and
`
Malika Izabachene
ESORICS 2014
September 9th, Wroclaw, Poland
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Conventional/electronic voting
Conventional voting relies on a combination of tangible physical
components and established voters’ habits
Electronic voting introduces a technological component, demands new
voters’ habits and thus trustworthiness must be built from scratch
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Electronic voting
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Anonymity in Electronic Voting
Ballot privacy none should learn how an honest voter voted
Receipt-freeness a voter should not be able to produce a receipt
proving how she voted
Vote-buying resistance a vote buyer shall not be convinced
about whether a voter has voted as she was asked for
Coercion-resistance a voter can, without detection, cheat a
coercer
Everlasting privacy ballot privacy is guaranteed in the long term
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Integrity in Electronic Voting
Individual verifiability a voter can be certain that his vote has
been counted
Universal verifiability any observer is convinced that the result
published corresponds to the ballots recorded
Elegibility verifiability any observer is convinced that only
legitimate voters have cast a vote
Accountability in case any of the above properties fail, a
responsible can certainly be found
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Helios : overview
Based on [Cramer, Gennaro, Schoenmakers] and [Benaloh]
and adapted and implemented by Ben Adida, Olivier Pereira, et al.
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Helios voting system
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Helios voting system
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Helios voting system
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Helios voting system
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Helios voting system (homomorphic tallying)
pk(S) : public key. The corresponding private key is split into n shares,
distributed among n electoral authorities
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Security of Helios
Verifiability proved by [Kremer, Ryan, Smyth] in a symbolic model
Accountability analyzed by [KuestersTruderung,Vogt]
¨
from a
systems level point of view
Ballot secrecy proved by [Delaune, Kremer, Ryan] in a symbolic
model and then [Bernhard, Cortier, Pereira, Smyth, Warinschi] in a
cryptographic model.
Practical everlasting privacy Helios w/o identifiers – proved by
[Arapinis,Cortier,Kremer,Ryan] in a symbolic model
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
A known limitation of Helios
A corrupted dishonest bulletin board may add ballots (e.g. voting on
behalf of absentees)
A few ballots may easily change the outcome of the election
Mitigated when the bulletin board publishes voters identities
However
Publishing voters identities is forbidden/discouraged in
some countries (e.g. France)
Not a perfect solution (e.g. the BB may not be caught)
Not suitable for a formal analysis of accountability
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Goal : protection against ballot stuffing
Verifiability The election result should correspond to :
votes of all honest and careful voters
votes of a subset of honest but not careful voters
at most k dishonest (but valid) votes
where k is the number of dishonest voters.
We provide an adaptation of definition from [Juels, Catalano,
Jakobsson] for a dishonest bulletin board
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Adding credentials allowing public authentication
list of voters
Election Administrator
list of voters
Registrar
upk
login/pwd
upk,usk
Voter
Bulletin Box
ballot
Sign(usk,ballot)
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Adding credentials allowing public authentication
We add a new authority, the Credential issuer
Sends a credential cred (a random seed) for each voter
Computes a signature key pair (sk(cred), vk(cred))
Publishes the list of public keys vk(cred1 ), . . . , vk(credn )
Voter’s client
Computes the key pair (sk(cred), vk(cred)) out of cred
Signs the Helios’ ballot with sk(cred)
Advantages
Requires little additional infrastructure
pwd created by user when registering at server’s side
cred sent by snail mail, SMS (15-alphanumeric)
Inherits the security of Helios (or the underlying voting protocol)
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Helios-C protocol
[{vD }pk(S) ]sk(credD )
Alice
Bob
Chris
...
Bulletin Board
[{vA }pk(S) , ZKP(vA = 0 or 1)]sk(credA )
[{vB }pk(S) , ZKP(vB = 0 or 1)]sk(credB )
[{vC }pk(S) , ZKP(vC = 0 or 1)]sk(credC )
...
Each voter posts his ballot + a signature of the ballot
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
A generic transformation for verifiability
More generally, we define a generic transformation :
P 7→ P cred
Theorem
If P satisfies verifiability assuming an honest BB, then P cred satisfies
verifiability assuming that Registrar and BB are not both dishonest
It preserves existing properties :
Theorem
If P satisfies privacy, then P cred satisfies privacy against a dishonest
BB.
The above also applies to receipt-freeness and everlasting privacy
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Security assumptions
Existentially unforgeable signature scheme
The original voting protocol satisfies verifiability against an
honest BB
Partial tally : ρ(S1 ∪ S2 ) = ρ(S1 ) ∗ ρ(S2 )
(necessary to define verifiability)
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Security of Helios-C
Corollary
Helios-C satisfies privacy, individual and universal verifiability if
Bulletin Board and Registrar are not simultaneously dishonest
Proof :
Privacy : Privacy of Helios [Bernhard, Pereira, Warinschi,
AsiaCrypt 2012] + Theorem 2
Verifiability : Verifiability of Helios + Theorem 1
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
How to prove verifiability ?
Two simple criteria :
Correctness : An honest execution of the voting protocol yields the
expected outcome
Accuracy : If a (dishonest) ballot b is accepted, it is an admissible
ballot (Tally(b) is valid)
Theorem
Let P be a an accurate and correct voting protocol, then P satisfies
verifiability (for an honest BB).
Theorem
Helios is verifiable in the Random-Oracle Model under the Discrete
Log assumption
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Implementation of Helios-C
We have implemented Helios-C, based on Helios’ code
stephane.glondu.net/helios/
belenios.gforge.inria.fr
Includes :
Addition of credentials/signing to client’s code
Threshold decryption (Pedersen-based)
Implementation of server-side in Ocaml
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Benchmarks
Unsurprisingly, the overhead of the signature is small.
number of candidates
encryption+proofs
time (ms)
signature time (ms)
ballot verification
time (ms)
signature verification time
2
5
10
20
30
40
50
600
1197
2138
4059
6061
7789
9617
196
110
215
210
248
390
301
720
358
1070
423
1380
484
1730
< 10 ms
< 10 ms
< 10 ms
< 10 ms
< 10 ms
< 10 ms
< 10 ms
D. Galindo
Election Verifiability for Helios under Weaker Assumptions
Conclusion
Theoretical contributions
We provide a generic use of credentials
provides verifiability under weaker trust assumptions
preserves privacy (and receipt-freeness, everlasting privacy)
A generic criteria for verifiability (correctness, accuracy, partial
tallying)
On-going work
Our use of credentials helps proving accountability
Everlasting privacy of Helios-C
A variant of Helios-C with receipt-freeness
A question for you
Does your country allow/forbid or advise/discourage to disclose the
list of people who actually voted ?
D. Galindo
Election Verifiability for Helios under Weaker Assumptions