Visible to the public Security Analysis of the Electronic Voting Protocol Based on Blind Intermediaries Using the SPIN Verifier

TitleSecurity Analysis of the Electronic Voting Protocol Based on Blind Intermediaries Using the SPIN Verifier
Publication TypeConference Paper
Year of Publication2018
AuthorsBabenko, Liudmila, Pisarev, Ilya
Conference Name2018 International Conference on Cyber-Enabled Distributed Computing and Knowledge Discovery (CyberC)
Date PublishedOct. 2018
ISBN Number978-1-7281-0974-9
Keywordsauthentication, Collaboration, cryptographic protocol, cryptographic protocols, cybersecurity, data substitution, E-Government, e-voting, Electronic voting, electronic voting protocol, electronic voting system, Electronic voting systems, formal verification, government data processing, linear temporal logic, LTL, man in the middle attack, MITM, model checking, policy-based governance, Promela language, protocol security, pubcrawl, resilience, Resiliency, security analysis, SPIN, SPIN formal verifier, SPIN verifier, Tools, verification

Cryptographic protocols are the basis for the security of any protected system, including the electronic voting system. One of the most effective ways to analyze protocol security is to use verifiers. In this paper, the formal verifier SPIN was used to analyze the security of the cryptographic protocol for e-voting, which is based on model checking using linear temporal logic (LTL). The cryptographic protocol of electronic voting is described. The main structural units of the Promela language used for simulation in the SPIN verifier are described. The model of the electronic voting protocol in the language Promela is given. The interacting parties, transferred data, the order of the messages transmitted between the parties are described. Security of the cryptographic protocol using the SPIN tool is verified. The simulation of the protocol with active intruder using the man in the middle attack (MITM) to substitute data is made. In the simulation results it is established that the protocol correctly handles the case of an active attack on the parties' authentication.

Citation Keybabenko_security_2018