SECURITY VERIFICATION OF CRYPTOGRAPHIC PROTOCOLS OF ELECTRONIC VOTING SYSTEM USING MULTIPLE THROWING OF BULLETINS BY SOURCE CODES
Abstract
The development of electronic voting systems is a complex and urgent task. The security of any system using networking is based on cryptographic protocols. Their quality is checked using formal verification tools. However, formal verification tools work with protocols in an abstract form of the Alice-Bob format, which does not allow fully checking the protocol for all kinds of attacks. In addition, when implementing the protocol in practice using any programming lan-guage, it is possible to change this protocol with respect to its original form. As a result, it turns out that the abstract initial form of the protocol, which was verified by means of formal verifica-tion, is considered safe, but the modified implemented protocol, having a different look, can no longer be considered safe. Thus, it is relevant to verify the cryptographic protocol of the electronic voting system using source codes. The paper described the electronic voting system using multiple casting of ballots. A parser for extracting the structure of a cryptographic protocol is described, with the help of which the structure of the voting protocol was obtained. The cryptographic proto-col of electronic voting was translated using multiple casting of ballots into the CAS + specifica-tion language for the Avispa automated verifier to verify the security of the protocol.
References
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.
