26.11.2018 - Seminarium Instytutowe - godz. 13:00,
Wojciech Jamroga (IPI PAN)
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
checking. 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.