ВЕРИФИКАЦИЯ БЕЗОПАСНОСТИ КРИПТОГРАФИЧЕСКИХ ПРОТОКОЛОВ ПО ИСХОДНЫМ КОДАМ СИСТЕМЫ ЭЛЕКТРОННОГО ГОЛОСОВАНИЯ С ПРИМЕНЕНИЕМ МНОЖЕСТВЕННОГО БРОСАНИЯ БЮЛЛЕТЕНЕЙ

Л. К. Бабенко; И.А. Писарев

Л. К. Бабенко Южный Федеральный Университет
И.А. Писарев Южный Федеральный Университет

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

Аннотация

Разработка систем электронного голосования является сложной и актуальной задачей. В основе безопасности любой системы, использующей сетевое взаимодействие, лежат крип-тографические протоколы. Их качество проверяется с помощью средств формальной верифи-кации. Однако средства формальной верификации работают с протоколами в абстрактном виде формата Alice-Bob, что не позволяет полностью проверить протокол на всевозмож-ные атаки. Кроме того, при реализации протокола на практике с помощью какого-либо языка программирования возможно изменение данного протокола относительно его пер-воначального вида. В итоге получается, что абстрактный первоначальный вид протокола, который был проверен средствами формальной верификации считается безопасным, но вот измененный реализованный протокол, имеющий другой вид уже не может быть при-знан безопасным. Таким образом актуальным является проведение верификации крипто-графического протокола системы электронного голосования по исходным кодам. В работе была описана система электронного голосования с применением множественного бросания бюллетеней. Описан парсер для извлечения структуры криптографического протокола, с помощью которого была получена структура протокола голосования. Произведена трансля-ция криптографического протокола электронного голосования с применением множественного бросания бюллетеней в язык спецификации CAS+ для автоматизированного верификатора Avispa для верификации безопасности протокола.

Литература

1. Viganò L. Automated security protocol analysis with the AVISPA tool, Electronic Notes in Theoretical Computer Science, 2006, Vol. 155, pp. 61-86.
2. Cremers C.J.F. The scyther tool: Verification, falsification, and analysis of security protocols, International Conference on Computer Aided Verification. Springer, Berlin, Heidelberg, 2008, pp. 414-418.
3. Küsters R., Truderung T. Using ProVerif to analyze protocols with Diffie-Hellman exponentia-tion, Computer Security Foundations Symposium, 2009. CSF'09. 22nd IEEE. IEEE, 2009, pp. 157-171. 4. Babenko L., & Pisarev I. Cryptographic Protocol Security Verification of the Electronic Vot-ing System Based on Blinded Intermediaries, In International Conference on Intelligent In-formation Technologies for Industry. Springer, Cham, 2018, September, pp. 49-57.
5. Chaki S., Datta A. ASPIER: An automated framework for verifying security protocol imple-mentations, Computer Security Foundations Symposium, 2009. CSF'09. 22nd IEEE. IEEE, 2009, pp. 172-185.
6. Goubault-Larrecq J., Parrennes F. Cryptographic protocol analysis on real C code, Interna-tional Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, Ber-lin, Heidelberg, 2005, pp. 363-379.
7. Goubault-Larrecq J., Parrennes F. Cryptographic protocol analysis on real C code. Technical re ort, Laboratoire S écification et Vérification, Re ort LSV-09-18, 2009.
8. Jürjens J. Using interface specifications for verifying crypto-protocol implementations, Work-shop on foundations of interface technologies (FIT), 2008.
9. Jürjens J. Automated security verification for crypto protocol implementations: Verifying the jessie project, Electronic Notes in Theoretical Computer Science, 2009, Vol. 250, No. 1, pp. 123-136.
10. O’Shea N. Using Elyjah to analyse Java implementations of cryptographic protocols, Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS-2008), 2008.
11. Backes M., Maffei M., Unruh D. Computationally sound verification of source code, Proceed-ings of the 17th ACM conference on Computer and communications security. ACM, 2010, pp. 387-398.
12. Bhargavan K. et al. Cryptographically verified implementations for TLS, Proceedings of the 15th ACM conference on Computer and communications security. ACM, 2008, pp. 459-468.
13. Bhargavan K., Fournet C., Gordon A.D. Verified reference implementations of WS-Security protocols, International Workshop on Web Services and Formal Methods. Springer, Berlin, Heidelberg, 2006, pp. 88-106.
14. Bhargavan K. et al. Verified interoperable implementations of security protocols, ACM Trans-actions on Programming Languages and Systems (TOPLAS), 2008, Vol. 31, No. 1, pp. 5.
15. Bhargavan K. et al. Verified implementations of the information card federated identity-management protocol, Proceedings of the 2008 ACM symposium on Information, computer and communications security. ACM, 2008, pp. 123-135.
16. Bhargavan K. et al. Cryptographically verified implementations for TLS, Proceedings of the 15th ACM conference on Computer and communications security. ACM, 2008, pp. 459-468. 17. Babenko L.K., Pisarev I.A. Elektronnoe golosovanie s primeneniem mnozhestvennogo brosaniya byulleteney [Electronic voting with the use of multiple casting ballots] Izvestiya YuFU. Tekhnicheskie nauki [Izvestiya SFedU. Engineering Sciences], 2018, No. 5 (199), pp. 48-56. 18. Babenko L.K., & Pisarev I.A. An algorithm for analysis of C# code initial for extracting the structure of cryptographic protocols1, Cybersecurity, 2018, Issues 4, 28.
19. Capek P., Kral E., Senkerik R. Towards an empirical analysis of. NET framework and C# lan-guage features' adoption, Computational Science and Computational Intelligence (CSCI), 2015 International Conference on. IEEE, 2015, pp. 865-866.
20. Basin D., M¨odersheim S., and Vigan`o L. OFMC: A Symbolic Model-Checker for Security Protocols, International Journal of Information Security, 2004.