Skip to main content

Verifying and implementing security protocols in Rust

Supervisor

Suitable for

MSc in Advanced Computer Science
Mathematics and Computer Science, Part C
Computer Science and Philosophy, Part C
Computer Science, Part C

Abstract

In this project, our goal is to develop a small working voting software like Helios [1] using Session Types. In the beginning. server will send credentials to all eligible voters before an election. On the election day, all the eligible voters will authenticate themselves and cast their ballot. At this point, the server will encrypt the ballot and will give two options to the voter, either decrypt the ballot --to ensure that server is not cheating-- or cast it. In case of decryption, the voter will again be prompted to enter a new ballot and given two options again, decrypt or cast. A voter can decrypt the ballot as many times as possible, to ensure that server is not cheating, before casting the ballot. Once it's cast, the server will send a confirmation to the voter and post the encrypted ballot to a bulletin board. After the end of the election, the server combines all the ballots homomorphically and decrypts the final tally and declares the winner.

Our first goal is to capture a simple version of Helios protocol using Session Types in NuScr (nuScribble) and generate an API, and later fill the API with Rust implementation. This project requires the knowledge of cryptography (basic understanding of ElGamal encryption), NuScibble, and Rust. 

[1]https://github.com/benadida/helios-server

[2]https://www.usenix.org/legacy/events/sec08/tech/full_papers/adida/adida.pdf