Анализ безопасности протокола регистрации в системе электронного голосования на основе слепых посредников с помощью инструмента Avispa

Системы электронного голосования являются будущей альтернативой традиционным способам проведения голосования. Как и для любой системы, важным является верификация ключевых алгоритмов, на которых основана её безопасность. В работе рассматривается анализ безопасности криптографического протокола на этапе регистрации, который используется в созданной авторами системе электронного голосования на основе слепых посредников. Проведено описание протокола регистрации, показаны передаваемые между сторонами сообщения и объяснено их содержимое. При моделировании протоколов предполагается использование модели угроз Долева-Яо. В качестве инструмента для анализа безопасности выбранного протокола используется система Avispa. Протокол описан на языке CAS+ и впоследствии транслирован в специальный язык HLPSL (High-Level Protocol Specification Language), с которым работает используемый инструмент. Описание протокола включает в себя роли, данные, ключи шифрования, порядок передаваемых сообщений между сторонами, знание сторон и злоумышленника, цели проверки. Поставлены цели верификации криптографического протокола на устойчивость к атакам на аутентификацию, секретность и replay-атакам. Установлены данные, которыми может владеть потенциальный злоумышленник. Произведен анализ безопасности протокола регистрации. Анализ показал, что выдвинутые цели проверки были достигнуты. Отображена подробная схема передачи сообщений и их содержимого при наличии злоумышленника, осуществляющего MITM-атаку (Man in the middle). Показана эффективность защиты протокола от действий злоумышленника.

электронное голосование, криптографические протоколы, криптографическая защита, верификация безопасности криптографических протоколов

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. Режим доступа: 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. Режим доступа: http://assets.adida.net/presentations/cambridge-university-voting-2005-01-18.pdf, accessed 10.06.2018.

7. Электронные выборы: опасение фальсификации результатов. Казахстан сегодня, 2004. Режим доступа: http://profit.kz/news/91/Elektronnie-vibori-opasenie-falsifikacii-rezultatov/, дата обращения 10.06.2018

8. Липень В.Ю., Воронецкий М.А., Липень Д.В., Полевиков Э.Л. Результаты апробирования технологий и систем электронного голосования. Объединенный институт проблем информатики НАН Беларуси, 2002. Режим доступа: http://uiip.bas-net.by/structure/l_kg/results_testing_technology.php/, дата обращения 10.06.2018

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. Л.К. Бабенко, И.А. Писарев, О.Б. Макаревич. Защищенное электронное голосование с использованием слепых посредников, Известия ЮФУ. Технические науки, №5, 2017 г., стр. 6-15.