Analyzing Prêt à Voter with Tamarin Prover

Abstract

I et stadig mer digitalisert samfunn, er elektronisk stemmegivning ved politiske valg ett viktig område å utforske. Samtidig som slike prosesser digitaliseres må det brukes ressurser på å sikre at dette foregår på en god måte, som er forenlig med den beste tilgjengeligheten kunnskapen på området. Det har blitt utviklet kryptografiske løsninger for hvordan man kan avholde elektroniske valg, og ett av disse systemene, Pret a Voter, blir nærmere undersøkt i denne oppgaven. Da dette systemet er spesifikt designet for å avholde politiske valg, er det fremtredende innen fagfeltet kryptografi.

Når en så viktig del av vårt samfunn avhenger av kryptografiske systemer, er det essensiellt at vi har gode verktøy og metoder for å undersøke disse systemene. Gjennom dette prosjektet blir en moderne protocol for electronisk stemmegivning, Pret a Voter, anaylsert ved hjelp av Tamarin Prover, ett moderne verktøy for algebraisk analyse av kryptografiske protokoller.

In a digitized society, electronic voting in a political election is an important area to explore. While processes like this are digitalized, there need to be used resources to ensure this happens in a sound way, consistent with the best available knowledge on the topic. Cryptographic solutions to holding electronic elections have been researched, and one of those systems, Prêt à Voter, will be closely examined in this project. As this system is specifically designed to perform to the standard of a political election, it is noteworthy in the field of cryptography.

When an essential part of society depends on cryptographical systems, it is important that we have good tools and methodology to examine these systems. Through this project, a modern protocol for electronic voting, Prêt à Voter is analyzed with the tool Tamarin Prover, a modern tool for algebraic analysis of cryptographic protocols.