# Verification of STAR-Vote and Evaluation of FDR and ProVerif

## TL;DR

This paper conducts an automated privacy analysis of the STAR-Vote system using FDR and ProVerif, demonstrating ballot secrecy verification and comparing tool effectiveness.

## Contribution

It is the first to formally verify STAR-Vote's privacy properties and evaluates the performance of FDR and ProVerif tools in this context.

## Key findings

- ProVerif is significantly faster than FDR.
- Both tools successfully verified ballot secrecy.
- ProVerif's speed makes it more suitable for iterative analysis.

## Abstract

We present the first automated privacy analysis of STAR-Vote, a real world voting system design with sophisticated "end-to-end" cryptography, using FDR and ProVerif. We also evaluate the effectiveness of these tools. Despite the complexity of the voting system, we were able to verify that our abstracted formal model of STAR-Vote provides ballot-secrecy using both formal approaches. Notably, ProVerif is radically faster than FDR, making it more suitable for rapid iteration and refinement of the formal model.