University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Formal modelling and analysis of mix net implementations.

Stathakidis, Efstathios (2015) Formal modelling and analysis of mix net implementations. Doctoral thesis, University of Surrey.

[img]
Preview
Text
PhD_Thesis_Stathakidis.pdf - Thesis (version of record)
Available under License Creative Commons Attribution Non-commercial Share Alike.

Download (2MB) | Preview
[img] Text
Stathakidis_Deposit_Agreement.docx - Thesis (version of record)
Available under License Creative Commons Attribution Non-commercial Share Alike.

Download (42kB)

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.

Item Type: Thesis (Doctoral)
Divisions : Theses
Authors :
AuthorsEmailORCID
Stathakidis, Efstathiossnd86@hotmail.comUNSPECIFIED
Date : 31 July 2015
Funders : EPSRC
Contributors :
ContributionNameEmailORCID
Thesis supervisorSchneider, Steve A.s.schneider@surrey.ac.ukUNSPECIFIED
Depositing User : Efstathios Stathakidis
Date Deposited : 11 Aug 2015 10:17
Last Modified : 11 Aug 2015 10:25
URI: http://epubs.surrey.ac.uk/id/eprint/808091

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800