Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

Formal Verification of Verifiable and Secret Online Elections with Strong Software Independence

Forschungsthema:Secure Electronic Voting
Typ: PdF
Datum: 2025-04-30
Betreuer: Michael Kirsten
Aushang:

Abstract

Online elections are vulnerable to both external and internal threats, compromising the privacy and integrity of the election. Properties such as strong software independence demand that a voting system for online elections should enable the detection and correction of any errors in the election result. Previous research has shown that risk-limiting audits provide statistical assurance of election integrity by examining portions of the public evidence provided by the voting system.

The e-voting community has focused on developing risk-limiting audits for paper-based elections where public evidence in the form of paper ballots is available. However, these risk-limiting audits are not feasible for online elections as no paper ballots are available. We thus adapt the idea of risk-limiting audits to the online election realm by constructing an end-to-end-verifiable online election that provides public evidence suitable for a risk-limiting audit. Additionally, we provide formal verification of the core components of the voting system using the Tamarin prover.

Literature