Verification of STAR-Vote and Evaluation of FDR and ProVerif
This work addresses security verification for a specific voting system, which is incremental as it applies existing formal methods to a new, complex case.
The researchers tackled the problem of verifying the privacy of the real-world STAR-Vote voting system by conducting the first automated analysis using FDR and ProVerif tools, successfully confirming ballot-secrecy in an abstracted model and finding ProVerif to be significantly faster for iterative refinement.
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.