Registration protocol security analysis of the electronic voting system based on blinded intermediaries using the Avispa tool
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 syste...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Ivannikov Institute for System Programming of the Russian Academy of Sciences
2018-10-01
|
| Series: | Труды Института системного программирования РАН |
| Subjects: | |
| Online Access: | https://ispranproceedings.elpub.ru/jour/article/view/561 |
| _version_ | 1818662847051202560 |
|---|---|
| author | I. A. Pisarev L. K. Babenko |
| author_facet | I. A. Pisarev L. K. Babenko |
| author_sort | I. A. Pisarev |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-17T05:07:27Z |
| format | Article |
| id | doaj.art-538973e341d44bd38119901f5d9ed557 |
| institution | Directory Open Access Journal |
| issn | 2079-8156 2220-6426 |
| language | English |
| last_indexed | 2024-12-17T05:07:27Z |
| publishDate | 2018-10-01 |
| publisher | Ivannikov Institute for System Programming of the Russian Academy of Sciences |
| record_format | Article |
| series | Труды Института системного программирования РАН |
| spelling | doaj.art-538973e341d44bd38119901f5d9ed5572022-12-21T22:02:22ZengIvannikov Institute for System Programming of the Russian Academy of SciencesТруды Института системного программирования РАН2079-81562220-64262018-10-0130415516810.15514/ISPRAS-2018-30(4)-10561Registration protocol security analysis of the electronic voting system based on blinded intermediaries using the Avispa toolI. A. Pisarev0L. K. Babenko1Южный Федеральный УниверситетЮжный Федеральный Университет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.https://ispranproceedings.elpub.ru/jour/article/view/561электронное голосованиекриптографические протоколыкриптографическая защитаверификация безопасности криптографических протоколов |
| spellingShingle | I. A. Pisarev L. K. Babenko Registration protocol security analysis of the electronic voting system based on blinded intermediaries using the Avispa tool Труды Института системного программирования РАН электронное голосование криптографические протоколы криптографическая защита верификация безопасности криптографических протоколов |
| title | Registration protocol security analysis of the electronic voting system based on blinded intermediaries using the Avispa tool |
| title_full | Registration protocol security analysis of the electronic voting system based on blinded intermediaries using the Avispa tool |
| title_fullStr | Registration protocol security analysis of the electronic voting system based on blinded intermediaries using the Avispa tool |
| title_full_unstemmed | Registration protocol security analysis of the electronic voting system based on blinded intermediaries using the Avispa tool |
| title_short | Registration protocol security analysis of the electronic voting system based on blinded intermediaries using the Avispa tool |
| title_sort | registration protocol security analysis of the electronic voting system based on blinded intermediaries using the avispa tool |
| topic | электронное голосование криптографические протоколы криптографическая защита верификация безопасности криптографических протоколов |
| url | https://ispranproceedings.elpub.ru/jour/article/view/561 |
| work_keys_str_mv | AT iapisarev registrationprotocolsecurityanalysisoftheelectronicvotingsystembasedonblindedintermediariesusingtheavispatool AT lkbabenko registrationprotocolsecurityanalysisoftheelectronicvotingsystembasedonblindedintermediariesusingtheavispatool |