Development, Formal Verification and Evaluation of an eVoting System with VVPAT

The use of new technologies to support voting has been and is the subject of great debate. Several people advocate the benefits it can bring — such as improved speed and accuracy in counting, accessibility, voting from home — and as many are concerned with the risks it poses, such as unequal access (digital divide), violation to secrecy and anonymity, alteration of the results of an election (because of malicious attacks, bad design/coding, or procedural weaknesses). The attitude of different governments towards electronic voting (e-voting) varies accordingly. In this paper we present the activities related to the devel- opment and formal verification of an e-voting system, called ProVotE1. ProVotE is an end-to-end e-voting system with Voter Verified Paper Audit Trial (VVPAT), developed within the frame- work of a larger initiative whose goal is assessing the feasibility of introducing e-voting in the Autonomous Province of Trento. ProVotE has been used in trials and elections with legal value in Italy. What we believe to be of interest is the approach we took for its development, which has been based on a participatory design for the definition of the voter interface, on the usage of formal methods and model checking for the validation of the core logic of the machine, on open source components, and on the formal analysis of some critical procedures related to the usage of the machine during the election