  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.
