Sommersemester 2022
E-Voting
| Veranstaltungstyp: | Seminar |
|---|---|
| Zielgruppe: | Master Informatik |
| Umfang: | 2 SWS / 3 ECTS |
| Termine: | 20.04.2022, 15.45 – 17.30 Uhr in Raum 3A-11.1 (Gebäude 05.20) (evtl. auch virtuell), Kick-Off-Veranstaltung 26.07.2022, 09.45 – 13.00 Uhr in Raum 3A-11.1 (Gebäude 05.20) (evtl. auch virtuell), Vorträge Teil I 29.07.2022, 14.00 – 17.15 Uhr in Raum 3A-11.1 (Gebäude 05.20) (evtl. auch virtuell), Vorträge Teil II Anmeldung bis 08.04., 23.59 Uhr hier (verlängert!). Melden Sie sich außerdem zum ILIAS-Kurs an. 16.09.2022, 23.59 Uhr, Fristende zur Abgabe der Ausarbeitung |
| Veranstaltungsnr.: | 2513553 |
| Lehrstühle: | Anwendungsorientierte Formale Verifikation Kryptographie und Sicherheit Security • Usability • Society (SECUSO) |
| Lehrkräfte: |
Prof. Dr. Bernhard Beckert |
| ILIAS-Kurs: | Link |
| Anmeldung: | Bei Fragen zum Seminar oder zur Anmeldung wenden Sie sich bitte an Michael Kirsten. Die Registrierung erfolgt über https://portal.wiwi.kit.edu/ys/5915 bis zum 8. April (verlängert!). Auf dieser Plattform erfolgt auchdie Bewertung der Seminarthemen. Bitte melden Sie sich auch zum ILIAS-Kurs an! |
| Platzvergabe: | Reihenfolge nach Eingang der Anmeldung |
Themenbereich
Was sollte ein Wahlverfahren erfüllen? Wann ist ein Wahlverfahren sicher? Welche Bestandteile muss man dabei untersuchen? Mithilfe welcher Methoden lässt sich dies untersuchen?
Es werden kryptographische Wahlverfahren sowie algorithmische Wahl- (auszähl-)verfahren aus verschiedenen Blickwinkeln (kryptographische Methoden, formale Korrektheit, menschliche Faktoren) untersucht.
Empfohlene Vorkenntnisse
Kenntnisse zu Grundlagen formaler Logik und Verifikationsmethoden, sowie Grundlagen der IT-Sicherheit sind hilfreich, beispielsweise aus den entsprechenden Stammmodulen.
Ablauf
Die Anmeldung für das Seminar ist im Zeitraum bis zum Freitag 08.04.2022 23:59 Uhr (geändert!) über die Seite https://portal.wiwi.kit.edu/ys/5915 möglich.
Aufgabenstellung
Für das Seminar werden von allen Teilnehmenden für eine erfolgreiche Teilnahme folgende Leistungen erwartet:
- Selbstständiges Erarbeiten der Inhalte des gewählten Themas auf Basis einer Auswahl von Einstiegspapieren. In regelmäßigen Treffen mit einem/r betreuenden wissenschaftlichen Mitarbeiter/in erhalten Sie hierbei die nötige Unterstützung.
- Auswahl und Gliederung der Inhalte, die in Ihrem Seminarvortrag präsentiert werden sollen.
- Kurze Vorstellung Ihrer Gliederung im Plenum.
- Entscheidung, wie Sie die Inhalte präsentieren wollen.
- Erstellung der Folien für Ihren Seminarvortrag und gegebenenfalls weiterer Materialien.
- Dreißminütiger Seminarvortrag im Plenum gefolgt von einer etwa fünfzehnminütigen Diskussion.
- Nach dem Vortrag: Verfassen einer etwa zehnseitigen Ausarbeitung, die die wesentlichen Inhalte Ihres Vortrags zusammenfassend darstellt.
Folien und Materialien
Liste der Themen
- Vertrauen in Online-Wahlen (Betreuung: Prof. Dr. Melanie Volkamer)
Literaturrecherche zur Identifikation von Faktoren, die einen Einfluss auf Vertrauen in ein Online-Wahlsystem haben.
- Verifizierbarkeit im Estnischen Online-Wahlsystem (Betreuung: Prof. Dr. Melanie Volkamer)
Literaturrecherche, um die eingesetzten Mechanismen inkl. der getroffenen Trust-Assumptions zu beschreiben und zu diskutieren.
- Tally-Hiding E-Voting (Betreuung: Felix Dörre)
Often the exact tally of an election is not needed, but only, e.g., a winner or a ranking of candidates. This topic discusses the advantages and disadvantages of tally-hiding systems e.g. at the example of Ordinos.
Literatur:
- Ralf Küsters, Julian Liedtke, Johannes Müller, Daniel Rausch and Andreas Vogt (2020): "Ordinos: A Verifiable Tally-Hiding E-Voting System". In: European Symposium on Security and Privacy (EuroS&P), 2020. IEEE. doi: 10.1109/EuroSP48549.2020.00022.
- The State of CH-Vote (Betreuung: Felix Dörre)
Switzerland created an E-Voting system called "CH-Vote" that had quite a few starting difficulties. This topic discusses CH-Vote and its initial problems and improvements.
Literatur:
- Rolf Haenni, Eric Dubuis, Reto E. Koenig and Philipp Locher (2020): "CHVote: Sixteen Best Practices and Lessons Learned". In: Electronic Voting (E-Vote-ID), 2020. Springer. doi: 10.1007/978-3-030-60347-2_7.
- Verified Construction of Correct Election Verifiers Using the Theorem Prover Coq (Betreuung: Michael Kirsten)
In diesem Seminarthema sollen Ansätze untersucht werden, die Wahl-Verifizierungswerkzeuge (zur Sicherstellung der Integrität der Abgabe oder Verarbeitung einer Stimme) mithilfe des allgemeinen Theorembeweisers Coq formalisiert und verifiziert, sowie direkt aus der verifizierten Formalisierung lauffähige Software generiert haben.
Literatur:
- Thomas Haines, Rajeev Goré, and Jack Stodart (2021): “Machine-Checking the Universal Verifiability of ElectionGuard”. In: Secure IT Systems (NordSec), 2020. Springer. doi: 10.1007/978-3-030-70852-8_4.
- Thomas Haines, Rajeev Goré, and Mukesh Tiwari (2019): “Verified Verifiers for Verifying Elections”. In: SIGSAC Conference on Computer and Communications Security (CCS '19), 2019. ACM. doi: 10.1145/3319535.3354247.
- Security Proofs of Election Verifiability Using the Automated Prover Tamarin (Betreuung: Michael Kirsten)
In diesem Seminarthema soll eine allgemeine symbolische Definition von Wahl-Verifizierbarkeit (zur Sicherstellung der Integrität der Abgabe oder Verarbeitung einer Stimme) sowie automatische Verifikationsansätze von Instanzen dieser (allgemeinen) Definition auf die bekannten Wahlprotokolle Helios und Belenios mithilfe des Prozessalgebra-Beweisers Tamarin untersucht und die Ergebnisse jeweils miteinander verglichen werden.
Literatur:
- Sevdenur Baloglu, Sergiu Bursuc, Sjouke Mauw, and Jun Pang (2021): “Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios.” In: 34th Computer Security Foundations Symposium (CSF). IEEE. doi: 10.1109/CSF51468.2021.00019.