Title: Anonymity versus accountability in evoting
Contact person: Hugo Jonker

Short description:

Anonymity plays an important role in voting. Not only should voters
remain anonymous, but if we consider vote buying, voters should even be
unable to prove how they voted (i.e. unable to nullify their anonymity).
The idea that voters cannot prove how they voted, is called
receipt-freeness (RF).
Another important requirement for evoting is the ensurance that a
voter's vote counts as she cast it. This individual verifiability (IV) means
that a voter is ensured that her vote constitutes part of the result, as
she cast the vote.
The obvious way to achieve IV is to give each voter a ticket they can
use to trace their votes. Equally obvious, such a ticket constitutes a
violation of RF. This leaves the question of whether the traceability
requirement of IV is fundamentally at odds with the anonymity
requirement imposed by RF.

The goal of this project is, given a formal definition
of RF, to sharpen that definition and to express IV in a similar
fashion. Compliance of some existing voting protocols to the formalised
notions is formally verified. Furthermore, the resulting definitions are
compared, establishing the common ground, if any, between the two notions.

Prerequisites:
	- Verification of security protocols
	- Process algebra
	- Formal methods