Registration protocol security analysis of the electronic voting system based on blinded intermediaries using the Avispa tool
https://doi.org/10.15514/ISPRAS-2018-30(4)-10
Abstract
Electronic voting systems are a future alternative to traditional methods of voting. It is important to verify the main algorithms on which system security is based. This paper analyzes the security of the cryptographic protocol at the registration stage, which is used in the electronic voting system based on blind intermediaries created by the authors. The registration protocol is described, the messages transmitted between the parties are shown and their content is explained. The Dolev-Yao threat model is used during protocols modeling. The Avispa tool is used for analyzing the security of the selected protocol. The protocol is described in CAS+ and subsequently translated into the HLPSL (High-Level Protocol Specification Language) special language with which Avispa work. The description of the protocol includes roles, data, encryption keys, the order of transmitted messages between parties, parties’ knowledge include attacker, the purpose of verification. The verification goals of the cryptographic protocol for resistance to attacks on authentication, secrecy and replay attacks are set. The data that a potential attacker may possess is detected. The security analysis of the registration protocol was made. The analysis showed that the objectives of the audit were put forward. A detailed diagram of the messages transmission and their contents is displayed in the presence of an attacker who performs a MITM-attack (Man in the middle). The effectiveness of protocol protection from the attacker actions is shown.
About the Authors
I. A. Pisarev
Southern Federal University
Russian Federation
Russian Federation
L. K. Babenko
Southern Federal University
Russian Federation
Russian Federation
References
1. Overview of e-voting systems, NICK Estonia. Estonian National Electoral Commission. Tallinn 2005.
2. Dossogne J., Lafitte F. Blinded additively homomorphic encryption schemes for self-tallying voting. Journal of Information Security and Applications, vol. 22, 2015, pp. 40-53.
3. Izabachene M. A Homomorphic LWE Based E-voting Scheme. In Proc. of the 7th International Workshop on Post Quantum Cryptography, 2016, pp 245-265.
4. Hirt M., Sako K. Efficient receipt-free voting based on homomorphic encryption. In Proc. of the International Conference on the Theory and Applications of Cryptographic Techniques, 2000, pp. 539-556.
5. Rivest L. R. et al. Lecture notes 15: Voting, homomorphic encryption. MIT, 2002. Available at http://web.mit.edu/6.857/OldStuff/Fall02/handouts/L15-voting.pdf, accessed 10.06.2018.
6. Ben Adida, Mixnets in Electronic Voting, Cambridge University, 2005. Available at http://assets.adida.net/presentations/cambridge-university-voting-2005-01-18.pdf, accessed 10.06.2018.
7. Electronic elections: fear of falsification of the results. Kazakhstan today, 2004. Available at http://profit.kz/news/91/Elektronnie-vibori-opasenie-falsifikacii-rezultatov/, accessed 10.06.2018 (in Russian).
8. Lipen V.Y., Voronetsky M.A., Lipen D.V., Polevikov E.L. Technology and results of testing electronic voting systems. Ob’edinennyj institut problem informatiki NAN Belarusi [United Institute of Informatics Problems NASB], 2002. Available at http://uiip.bas-net.by/structure/l_kg/results_testing_technology.php/, accessed 10.06.2018 (in Russian).
9. David L Chaum. Untraceable electronic mail, return addresses, and digital pseudonyms. Communications of the ACM, vol. 24, no. 2, 1981, pp. 84-90.
10. Ali S. T., Murray J. An Overview of End-to-End Verifiable Voting Systems. arXiv preprint arXiv: 1605.08554, 2016.
11. Smart M., Ritter E. True trustworthy elections: remote electronic voting using trusted computing. In Proc. of the International Conference on Autonomic and Trusted Computing, 2011, pp.187-202.
12. Bruck S., Jefferson D., Rivest R.L. A modular voting architecture («frog voting»). Towards trustworthy elections. LNCS, volume 6000, 2010, pp. 97-106.
13. Jonker H., Mauw S., Pang J. Privacy and verifiability in voting systems: Methods, developments and trends. Computer Science Review, vol. 10, 2013, pp. 1-30.
14. Shubhangi S. Shinde, Sonali Shukla, Prof. D. K. Chitre. Secure E-voting Using Homomorphic Technology, International Journal of Emerging Technology and Advanced Engineering, vol. 3, no. 8, 2013, pp. 203-206.
15. Neumann S., Volkamer M. Civitas and the real world: problems and solutions from a practical point of view. In Proc. of the Seventh International Conference on Availability, Reliability and Security (ARES), 2012, pp. 180-185.
16. Yi X., Okamoto E. Practical remote end-to-end voting scheme. In Proc. of the International Conference on Electronic Government and the Information Systems Perspective, 2011, pp. 386-400.
17. The AVISPA team, The High Level Protocol Specification Language. Available at http://www.avispa-project.org/, accessed 10.06.2018
18. Ronan Saillard, Thomas Genet, CAS+, March 21, 2011. Available at http://people.irisa.fr/Thomas.Genet/span/CAS_manual.pdf, accessed 10.06.2018
19. D. Basin, S. M¨odersheim, and L. Vigan`o. OFMC: A Symbolic Model- Checker for Security Protocols. International Journal of Information Security, vol. 4, issue 3, 2004, pp 181–208.
20. L.K. Babenko, I.A. Pisarev, O.B. Makarevich. Secure electronic voting using blinded intermediaries. Isvestiya SFedU. Engineering sciences, no. 5, 2017, pp. 6-15 (in Russian).
Review
For citations:
Pisarev I.A., Babenko L.K. Registration protocol security analysis of the electronic voting system based on blinded intermediaries using the Avispa tool. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(4):155-168. https://doi.org/10.15514/ISPRAS-2018-30(4)-10
Email this article 