Formal Verification and Implementation of an E-Voting System

Introduction

Voting is a complex system that contains many sensitive and confidential activities. It is an important operation that is used in many institutions, including governments, companies and universities. Several kinds of vote exist in countries around the world such as: presidential elections, parliamentary elections, local elections and constitutional referendums. They are mainly used to elect presidents of countries, committee chairs, and people's representatives to accomplish a well-defined task. In any country, organizing free, democratic and transparent elections requires two major things. The first thing is an independent national electoral authority that manages all the stages of the electoral process, from the preparation of the elections until the announcement of the preliminary results. The second thing is the use of new information and communication techniques to manage elections in particular, the voters list and the list of candidates.

Due to technological developments, including the increasing speed of the Internet, many countries have opted for e-voting as a suitable solution for elections. The e-voting offers the possibility to vote online anytime and from anywhere using a computer, smartphone or tablet. It also saves time and reduces costs and effort spent on the election process. However, the majority of e-voting applications are deployed over the Internet, and the number of Cyber-Attacks and applications vulnerabilities has recently increased. In reality, e-voting security is a difficult task that has attracted the attention of many researchers. More precisely, honest elections should guarantee voter authentication, confidentiality and integrity of the vote, and the ability to audit the election (Lauer 2004). To this end, the current challenge is to use blockchain to address the e-voting security issues. Moreover, the blockchain technology is an emerging technology with a strong cryptographic foundation like Ethereum (Ethereum Homepage 2022), Hyperledger (Hyperledger Homepage 2022). It allows applications to take advantage of these capabilities to achieve resilient security solutions.

On the other hand, the e-voting system may suffer from many errors and inconsistencies of the design phase such as deadlocks, livelocks. For example, the system cannot stop its execution or the system crashes (fails without the failure being identified). Formal methods make it possible to unambiguously describe the behavior of systems. In addition, formal methods make it possible to verify certain qualitative properties that systems must have, such as the absence of deadlocks. In many works like (Ahmad et al. 2020), (Villafiorita et al. 2009), (Cortier et al. 2017) and (Weldemariam et al. 2011), the authors used the formal methods approaches such as: Petri nets, process algebra, Maude for the development of e-voting systems. So, the use of formal methods is the appropriate solution in the design of critical e-voting systems in order to ensure the accuracy and validity of these systems.

In this paper, we propose a new secure e-voting system based on Ethereum blockchain. This system allows the creation of elections, the voting management and the candidates management. It also allows voters to vote online at any time and from anywhere using a computer, a smartphone or a tablet. In addition, we propose a Hierarchical Colored Petri Net (HCPN) model for our e-voting system using CPN Tools (CPN Tools Homepage 2022). We verify by means of simulation techniques and state space analysis important properties such as absence of deadlocks and livelocks of this e-voting system. The rest of this paper is organized as follows: In section 2, we discuss related works. In section 3, we present the concepts and background of this work. In section 4, we propose an e-voting system based on Ethereum blockchain and its implementation. In section 5, we present the modeling and verification of our e-voting system using Hierarchical Coloured Petri Net (HCPN) in CPN Tools. Finally, conclusions and future work are presented in Section 6.