Verification of Voter-Verifiable Voting Protocols

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.