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.
CITATION STYLE
Moran, M., & Wallach, D. S. (2017). Verification of STAR-vote and evaluation of FDR and ProVerif. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10510 LNCS, pp. 422–436). Springer Verlag. https://doi.org/10.1007/978-3-319-66845-1_28
Mendeley helps you to discover research relevant for your work.