Abstract
Elections are at the heart of democratic societies and for this reason they should provide the voters the assurance that their votes have been cast as intended and that the final result is accurate, whilst at the same time, delivering voter anonymity and secrecy of the votes. On the other hand, the voters should trust the voting systems and be able to verify the correctness of the final tally and the integrity of the elections. In this regard, in recent years, thanks to the improve- ment of cryptographic techniques, different electronic voting schemes have been implemented. However, such schemes are rather complex, and in order to pre- serve their properties, rely on the integrity and trustworthiness of single points of trust and failure. With the aim of achieving anonymity and public verifiability, Mix Net protocols have been developed for use in conjunction with a trusted and publicly accessible Web site, on to which all the produced data are posted for ver- ification. However, implementing such distributed algorithms is not trivial and many Mix Net constructions have been broken after they were introduced. This thesis identifies the problems existing in Mix Net implementations and proposes sound solutions to address them. The work presented in this thesis increases the rigour with which Mix Net pro- tocols are verified against their security requirements. Moreover, it bridges the gap existing in the literature regarding the absence of formal modelling, analysis and automated verification of Mix Net implementations, by using the process algebra, Communicating Sequential Processes (CSP), and the model checker, Failures-Divergence Refinement (FDR). In particular, the version of the source code taken on 7 January 2014, which formed the basis of the analysis in this the- sis, did not meet all of the security requirements for the election to take place in November 2014, and solutions are proposed. In the event, the code was updated and the version for the election did not have the flaws identified here. More- over, a novel method is put forward for constructing and making conventional Mix Net implementations robust, by distributing the trust among its components and giving them the power to decide about the others’ honesty; an approach that can be adopted for all constructions that follow the same design principle. Ad- ditionally, different and more efficient methods for devising such protocols are demonstrated. Finally, the automated analysis conducted in this thesis has been performed under the existence of a powerful intruder, who can perform a number of active attacks.