Abstract:
SELENE is a recently proposed voting protocol that provides reasonable protection against coercion. Both verifiability and security of Selene are based on cryptographic machinery applied to the concept of tracking numbers assigned to votes. In this paper, we make the first step towards a formalization of selected features of the protocol by means of formulae and models of multi-agent logics. The models define the space of strategies for the voters, the election authority, and the potential coercer. We express selected properties of the protocol using the strategic logic ATLir, and conduct preliminary verification by model hecking. While ATLir allows for intuitive specification of requirements like coercion-resistance, model checking of ATLir is notoriously hard. We show that some of the complexity can be avoided by using a recent approach of approximate model checking, based on fixpoint approximations.