Registration protocol security analysis of the electronic voting system based on blinded intermediaries using the Avispa tool

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