Formal Verification and Implementation of an E-Voting System
Authors: 
Said Meghzili, Allaoua Chaoui, Raida Elmansouri, Bardis Nadjla Alloui, Amina BouabsaAuthors Info & Claims
Pages 1 - 22
Abstract
The organization of free, democratic, and transparent elections requires on the one hand an independent national electoral authority that manages all the stages of the electoral process and on the other hand the use of new information and communication techniques to manage the election process. E-voting offers the ability to vote online anytime and from anywhere using a computer, smartphone, or tablet. In addition, it saves time and reduces costs and effort spent in the process. However, the security of e-voting applications deployed on the internet is a difficult task due to the increasing number of cyber-attacks and application vulnerabilities. On the other hand, blockchain technology is an emerging technology with a strong cryptographic foundation. In this paper, the authors propose a new secure e-voting system based on Ethereum blockchain. In addition, they propose a hierarchical coloured petri net (HCPN) model for their e-voting system using CPN Tools. They verify by means of simulation techniques and state space analysis important properties such as absence of deadlocks and livelocks.
References
[1]
Abuidris, Y., Kumar, R., Yang, T., & Onginjo, J. (2021). Secure large‐scale E‐voting system based on blockchain contract using a hybrid consensus model combined with sharding. ETRI Journal, 43(2), 357–370.
[2]
Ahmad, Z., Ahmad, F., & Gondal, Z. A. (2020). Formal Analysis of Improved and Secure Architecture of E-voting System using Hierarchical Coloured Petri Nets. The Nucleus, 56(4), 137–143.
[3]
Cansell, D., Gibson, J. P., & Méry, D. (2007). Refinement: A constructive approach to formal software design for a secure e-voting interface. Electronic Notes in Theoretical Computer Science, 183, 39–55.
[4]
Cortier, V. (2015). Formal verification of e-voting: Solutions and challenges. ACM SIGLOG News, 2(1), 25–34.
[5]
Cortier, V., & Wiedling, C. (2017). A formal analysis of the Norwegian E-voting protocol. Journal of Computer Security, 25(1), 21–57.
[6]
CPN Tools Homepage. (2022). CPN Tools – A tool for editing, simulating, and analyzing Colored Petri nets. https://cpntools.org
[7]
Encyclopedia Britannica. (2022). Electronic voting. https://www.britannica.com/topic/electronic voting.
[8]
Enguehard, C. (2019). Blockchain et vote électronique. Terminal. Technologie de l'information, culture & société, (124).
[9]
Ethereum Homepage. (2022). Home | ethereum.org. https://ethereum.org
[10]
Exonum. (2022). Exonum: Build trust into business with blockchain technology. https://exonum.com/
[11]
FanW.KumarS.JadhavV.ChangS. Y.ParkY. (2020, December). A Privacy Preserving E-Voting System Based on Blockchain. In Silicon Valley Cybersecurity Conference (pp. 148-159). Springer.
[12]
Ganache Homepage. (2022). Ganache | Truffle Suite. https://www.trufflesuite.com/ganache
[13]
Ganiyu, R. A., Omidiora, E. O., Olaoluwa, A. O., & Badmus, T. A. (2016). Simulation Based Analysis of the Hierarchical Timed Coloured Petri Net Model of the Nigerian Voting System. IOSR Journal of Computer Engineering, 18(6), 95–108.
[14]
Garg, K., Saraswat, P., Bisht, S., Aggarwal, S. K., Kothuri, S. K., & Gupta, S. (2019, April). A comparitive analysis on e-voting system using blockchain. In 2019 4th International Conference on Internet of Things: Smart Innovation and Usages (IoT-SIU) (pp. 1-4). IEEE. 10.1109/IoT-SIU.2019.8777471
[15]
Gibson, J. P., Krimmer, R., Teague, V., & Pomares, J. (2016). A review of e-voting: The past, present and future. Annales des Télécommunications, 71(7), 279–286.
[16]
Gibson, J. P., & Raffy, J. L. (2021). Modelling an e-voting domain for the formal development of a Software Product Line: when the implicit should be made explicit. In Implicit and Explicit Semantics Integration in Proof-Based Developments of Discrete Systems (pp. 3–18). Springer.
[17]
HardwickF. S.GioulisA.AkramR. N.MarkantonakisK. (2018, July). E-voting with blockchain: An e-voting protocol with decentralisation and voter privacy. In 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData) (pp. 1561-1567). IEEE. 10.1109/Cybermatics_2018.2018.00262
[18]
Hjálmarsson, F. Þ., Hreiðarsson, G. K., Hamdaqa, M., & Hjálmtýsson, G. (2018, July). Blockchain-based e-voting system. In 2018 IEEE 11th international conference on cloud computing (CLOUD) (pp. 983-986). IEEE. 10.1109/CLOUD.2018.00151
[19]
Hyperledger Homepage. (2022). Hyperledger – Open Source Blockchain Technologies. https://www.hyperledger.org/
[20]
JamrogaW.KimY.KurpiewskiD.RyanP. Y. (2020, October). Towards Model Checking of Voting Protocols in Uppaal. In International Joint Conference on Electronic Voting (pp. 129-146). Springer. 10.1007/978-3-030-60347-2_9
[21]
Jensen, K., & Kristensen, L. M. (2015). Colored Petri nets: A graphical language for formal modeling and validation of concurrent systems. Communications of the ACM, 58(6), 61–70.
[22]
Khan, K. M., Arshad, J., & Khan, M. M. (2018). Secure digital voting system based on blockchain technology. International Journal of Electronic Government Research, 14(1), 53–62.
[23]
Khan, K. M., Arshad, J., & Khan, M. M. (2021). Empirical analysis of transaction malleability within blockchain-based e-Voting. Computers & Security, 100, 102081.
[24]
Kshetri, N., & Voas, J. (2018). Blockchain-enabled e-voting. IEEE Software, 35(4), 95–99.
[25]
Lauer, T. W. (2004). The risk of e-voting. Electronic . Journal of E-Government, 2(3), 177–186.
[26]
Meghzili, S., Chaoui, A., Strecker, M., & Kerkouche, E. (2019). Verification of Model Transformations Using Isabelle/HOL and Scala. Information Systems Frontiers, 21(1), 45–65.
[27]
Multichain Homepage. (2022). MultiChain | Open source blockchain platform. https://www.multichain.com
[28]
Noizat, P. (2015). Blockchain electronic vote. In Handbook of digital currency (pp. 453–461). Academic Press.
[29]
Olayinka, O. A. (2020). Development of a Model for a Secured Bimodal Voting Framework Using Timed Coloured Petri Nets. E-Vote-ID, 2020, 414.
[30]
Panja, S., & Roy, B. (2021). A secure end-to-end verifiable e-voting system using blockchain and cloud server. Journal of Information Security and Applications, 59, 102815.
[31]
Rathee, G., Iqbal, R., Waqar, O., & Bashir, A. K. (2021). On the design and implementation of a blockchain enabled e-voting application within iot-oriented smart cities. IEEE Access: Practical Innovations, Open Solutions, 9, 34165–34176.
[32]
Saqib, M. N., Kiani, J., Shahzad, B., Anjum, A., & Ahmad, N. (2019). Anonymous and formally verified dual signature based online e-voting protocol. Cluster Computing, 22(1), 1703–1716.
[33]
Solidity Homepage. (2022). Solidity Programming Language. https://soliditylang.org/
[34]
Taş, R., & Tanrıöver, Ö. Ö. (2020). A systematic review of challenges and opportunities of blockchain for E-voting. Symmetry, 12(8), 1328.
[35]
Truffle Homepage. (2021). Sweet Tools for Smart Contracts | Truffle Suite. https://www.trufflesuite.com
[36]
Villafiorita, A., Weldemariam, K., & Tiella, R. (2009). Development, formal verification, and evaluation of an e-voting system with VVPAT. IEEE Transactions on Information Forensics and Security, 4(4), 651–661.
[37]
Wakrime, A. A., Gibson, J. P., & Raffy, J. L. (2018, June). Formalising the requirements of an E-voting software product line using Event-B. In 2018 IEEE 27th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE) (pp. 78-84). IEEE. 10.1109/WETICE.2018.00022
[38]
Weldemariam, K., Kemmerer, R. A., & Villafiorita, A. (2011). Formal analysis of an electronic voting system: An experience report. Journal of Systems and Software, 84(10), 1618–1637.
Index Terms
- Formal Verification and Implementation of an E-Voting System
Index terms have been assigned to the content through auto-classification.
Recommendations
SBvote: Scalable Self-Tallying Blockchain-Based Voting
SAC '23: Proceedings of the 38th ACM/SIGAPP Symposium on Applied ComputingDecentralized electronic voting solutions represent a promising advancement in electronic voting. One of the e-voting paradigms, the self-tallying scheme, offers strong protection of the voters' privacy while making the whole voting process verifiable. ...
A Survey on Formal Verification for Solidity Smart Contracts
ACSW '21: Proceedings of the 2021 Australasian Computer Science Week MulticonferenceOne of the 21st century’s hottest topics in the world of IT has been the emergence of what some predict to be the foundation stone for a new era of internet (web 3.0): Blockchain technology. Besides being the backbone of what we come to know as ...
On Secure E-Voting over Blockchain
This article discusses secure methods to conduct e-voting over a blockchain in three different settings: decentralized voting, centralized remote voting, and centralized polling station voting. These settings cover almost all voting scenarios that occur ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2022.
Publisher
IGI Global
United States
Publication History
Published: 30 September 2022
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 19 Dec 2024