Verification of Voter-Verifiable Voting Protocols

01/09/2016 to 31/08/2019

We propose to use techniques from formal specification and verification of multi-agent systems, and apply them to verify information security requirements for voting protocols. In particular, we will look at various formalizations of confidentiality, coercion-resistance, and voter-verifiability in e-voting protocols. The research will lead to the development of a toolbox for practical verification of strategic properties in interaction protocols. Based on case studies using the toolbox, we will draft some advice on how societal processes of governance and collective choice can be improved.Voting is a mechanism of utmost importance to social processes.

Nowadays, digital technology makes it even more important, as it holds out the promise of greater citizen engagement in decision making. Throughout the history of democracy elections have been the target of attempts to manipulate the outcome. In order to counter threats of coercion or vote buying, ballot confidentiality was recognised an important property of voting systems. One can also look at more sophisticated notions of information security. In particular, coercion-resistance is intended to envelope all security concerns regarding the voting process, and can be defined informally as: whatever strategy the coercer adopts, the voter always has a strategy to vote as they intend while appearing to comply with all the coercer’s requirements. Moreover, voter-verifiability is defined as the ability of voters to confirm that their votes are correctly registered and counted.

In this project, we focus on the strategic aspect of information security in voting procedures. We argue that the properties of coercion-resistance, confidentiality, and voter-verifiability are underpinned by existence (or nonexistence) of a suitable strategy for some participants: typically for the voter, the coercer, or both. In order to formalize the properties, we will use modal logics of strategic ability, in particular variants of the strategic logic ATL. We will significantly extend the existing techniques of model checking so that it becomes possible to verify strategic properties in voting procedures. Furthermore, we will develop abstract specifications that disambiguate different flavours of confidentiality, voter-verifiability, and coercion-resistance, as well as actual models and reduction techniques for the voting domain. The research will lead to the development of a toolbox that can be used both as a general tool for verification of strategic properties in interaction protocols, and as a dedicated tool for assessment of information security level in voting procedures.Achieving confidentiality and coercion-resistance typically comes at a cost, in particular in terms of usability. There is also a trade-off between coercion-resistance and voter-verifiability. We propose that the quality of a protocol with respect to the above requirements can be measured by the accessibility and simplicity of strategies that the voter (respectively, the coercer) can have towards certain goals. With this intuition, we will define concrete metrics to assess the level of usability, confidentiality, coercion-resistance, and voter-verifiability in given threat environments. We will also use our toolbox to compute the metrics for a number of voting protocols. Based on the results, we will draft advice for the Polish and Luxembourgish electoral authorities on how societal processes of governance and collective choice can be improved.

Tuesday, 8 January, 2019

News Project of the Week: CyberSec4Europe

The CyberSec4Europe project, one of the four pilot projects aimed at establishing a European Cybersecurity Competence Network has just been launched on February 28 in Brussels.

During its 42 months of duration, the project will align and interconnect a vast pool of research excellence in existing centres and research facilities, bringing together cybersecurity expertise in an interdisciplinary manner while developing a governance model for the future European Cybersecurity Competence Network.

Future Events

Cyber Insurance and its Contribution to Cyber Risk Mitigation - Leiden March 25-29
25/03/2019 to 29/03/2019

The rise in both the scale and severity of recent cyberattacks demands new thinking about cybersecurity risk and the mitigation and transfer of that risk. Cyber insurance is one potential way to manage risk by transferring damage liability, but the cyber insurance market is immature and the understanding and actuarial knowledge of cyber-risk is currently underdeveloped.

e-SIDES workshop 2019

e-SIDES workshop: Towards Value-Centric Big Data: Connect People, Processes and Technology


2 April 2019

10am to 4pm


e-SIDES is a research project funded by European Commission H2020 Programme that deals with the ethical, legal, social and economic implications of privacy-preserving technologies in different big data context.