The DEMOS family of e-voting systems: end - to - end verifiable elections in the standard model

Abstract

During the last decades, electronic voting (e-voting) systems have emerged as promising technologies for carrying out democratic procedures in the Digital Age. Their major advantages comprise the facilitation of participation of social groups with considerable physical barriers, reduction of the election cost and acceleration of the set up, voting and tally phases during an election execution. By today, e-voting systems have been used in several countries either in pilot executions or binding elections at a municipality or national level. Nonetheless, they have been subject to occasionally trenchant criticism, mainly due to the disquiet about potential securitythreats caused by the amount of power now transferred to the machines.This PhD thesis addresses the prospect of e-voting from the viewpoint of contemporarycryptography. Its main contribution is the introduction of e-voting systems that achieveend-to-end verifiability in the standard model for the first time. End-to-end verifiability is astrong security property suggesting that the voters can verify the integrity of the electionprocedure without putting trust in any administration authority. End-to-end verifiability inthe standard model denotes that verification is executed without assuming any trustedsetup. Prior to this thesis, all top-tier e-voting systems (e.g. SureVote, JCJ, Prêt à Voter,Helios, Scantegrity, etc.) assumed honesty of the voting clients, the random oracle model,or the existence a randomness beacon to achieve end-to-end verifiability. Therefore, until recently, the feasibility of end-to-end verifiable elections in the standard model remained an open question.The above question is answered affirmatively in this thesis with the introduction of theDEMOS-A and DEMOS-2 e-voting systems. The two systems follow different approacheswith respect to their design and have complementary benefits and weaknesses. In the core of both systems, is a novel mechanism that extracts the randomness required for verification from the entropy generated by the voters, when they engage in the voting phase. This entropy is internal with respect to the election environment, therefore the need for trusting an outer source of randomness is removed. For a concrete security analysis of DEMOS-A and DEMOS-2, this thesis brings in a strongcryptographic framework that adds to the literature a state-of-the-art methodologyfor the study of e-voting systems and can be seen as an independent contribution. Thesaid framework is extended by modelling e-voting systems as ceremonies, inspired by the work of Ellison in 2007. In an e-voting ceremony, the human entities are analysed separately from their associated devices and operate as finite state machines (transducers) with limited power. As a case study of an e-voting ceremony, this thesis investigates the security of the well known Helios e-voting system by providing formal proofs as well as evaluations based onreal-world and simulation data.

Τις τελευταίες δεκαετίες, τα συστήματα ηλεκτρονικής ψηφοφορίας (e-voting systems) έχουν προταθεί ως μία υποσχόμενη τεχνολογία για τη διεξαγωγή δημοκρατικών διαδικασιών στα πλαίσια της Ψηφιακής Εποχής. Τα βασικά τους πλεονεκτήματα συνίστανται στη διευκόλυνση της συμμετοχής κοινωνικών ομάδων που αντιμετωπίζουν φυσικά εμπόδια και κινησιακές δυ-σκολίες, καθώς και στη μείωση του κόστους και του απαιτούμενου χρόνου της εκλογικήςδιαδικασίας σε σημαντικό βαθμό. Μέχρι σήμερα, τα συστήματα ηλεκτρονικής ψηφοφορίαςέχουν εφαρμοστεί τόσο σε πιλοτικά πειράματα όσο και σε εκλογές σε περιφερειακό καιεθνικό επίπεδο. Εντούτοις, έχουν υπάρξει αντικείμενα ενίοτε έντονης κριτικής κυρίως λόγωζητημάτων ασφάλειας που εγείρονται από τη χρήση πιθανώς διαβλητών υπολογιστικώνσυσκευών.Η παρούσα διατριβή μελετά το αντικείμενο της ηλεκτρονικής ψηφοφορίας από τη σκοπιάτης σύγχρονης κρυπτογραφίας. Η σημαντικότερη συνεισφορά της είναι η εισαγωγή συστημάτων που επιτυγχάνουν για πρώτη φορά άμεση επαληθευσιμότητα (end-to-end verifiability) στο standard μοντέλο. Η άμεση επαληθευσιμότητα είναι μια ισχυρή ιδιότητα ασφάλειας, σύμφωνα με την οποία ο ψηφοφόρος μπορεί να επαληθεύσει την ακεραιότητα της εκλογικής διαδικασίας χωρίς να εναποθέτει εμπιστοσύνη σε καμία εκλογική αρχή. Η άμεση επαληθευσιμότητα στο standard μοντέλο υποδηλώνει ότι για την επαλήθευση δεν απαιτείται η υπόθεση κάποιας έμπιστης παραμέτρου στο εκλογικό περιβάλλον. Προγενέστερα της παρούσας διατριβής, όλα τα κορυφαία συστήματα ηλεκτρονικής ψηφοφορίας (π.χ. SureVote, JCJ, Prêt à Voter, Helios, Scantegrity κ.ά.) προϋπέθεταν αδιάβλητες συσκευές ψηψοφορίας,το μοντέλο τυχαίου μαντείου (random oracle model), ή την ύπαρξη μίας έμπιστης πηγής τυχαιότητας (randomness beacon) για την εξασφάλιση της άμεσης επαληθευσιμότητας.Κατά συνέπεια, η ύπαρξη ενός συστήματος με άμεση επαληθευσιμότητα στο standardμοντέλο παρέμενε ανοιχτό ερώτημα.Το παραπάνω ερώτημα απαντάται καταφατικά στην παρούσα διατριβή με την παρουσίασητων συστημάτων ηλεκτρονικής ψηφοφορίας DEMOS-A και DEMOS-2, τα οποίαακολουθούν διαφορετικές κατευθύνσεις ως προς το στο σχεδιασμό τους ενώ εμφανίζουν συμπληρωματικά πλεονεκτήματα και αδυναμίες. Στην καρδιά και των δύο συστημάτων εντοπίζεται ένας μηχανισμός εξαγωγής τυχαιότητας, απαιτούμενης για την άμεση επαληθευσιμότητα, από την εντροπία που παράγεται από τη διάδραση των ψηφοφόρων με το σύστημα. Η προκείμενη εντροπία είναι εσωτερική ως προς το περιβάλλον ψηφοφορίας, εξαλείφοντας έτσι την ανάγκη ύπαρξης μιας εξωτερικής πηγής τυχαιότοτητας. Για την αυστηρή ανάλυση ασφάλειας των DEMOS-A και DEMOS-2, η παρούσα διατριβήπροτείνει ένα πλήρες κρυπτογραφικού πλαισίου το οποίο προσθέτει στη βιβλιογραφία μία υψηλών προδιαγραφών μεθοδολογία για τη μελέτη των συστημάτων ηλεκτρονικής ψηφοφορίας και μπορεί να θεωρηθεί ως επιπρόσθετη συνεισφορά της παρούσας διατριβής. Το εν λόγω πλαίσιο επεκτείνεται σύμφωνα με το ceremony μοντέλο σύμφωνα με την προσέγγιση στο έργο του Ellison το 2007. Σε ένα ceremony ηλεκτρονικής ψηφοφορίας, οι ανθρώπινες οντότητες διαχωρίζονται από τις συσκευές και λειτουργούν ως μηχανές πεπερασμένων καταστάσεων (transducers) περιορισμένης ισχύος. Ως υπόδειγμα μελέτης ενός ceremony ηλεκτρονικής ψηφοφορίας, παρούσα διατριβή μελετά την ασφάλεια του ευρέως εφαρμοσμένου συστήματος ηλεκτρονικής ψηφοφορίας Helios, παρέχοντας τυπικές αποδείξεις αλλά και πειραματικές εκτιμήσεις βασισμένες σε πραγματικά δεδομένα και προσομοιώσεις.