Verification of STAR-Vote and Evaluation of FDR and ProVerif
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.
KeywordsSecurity protocols Formal methods Privacy E-voting STAR-Vote FDR ProVerif
This work was carried out under the NSF-funded Voting Systems Architectures for Security and Usability project. The principal author is also partly funded by TUBITAK. We would like to thank Ben Smyth, Olivier Pereira, and Thomas Gibson-Robinson for their helpful technical discussions.
- 2.Backes, M., Hritcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: CSF (2008)Google Scholar
- 3.Benaloh, J.: Simple verifiable elections. In: Proceedings of the USENIX/ACCURATE Electronic Voting Technology Workshop (EVT 2006), Vancouver, B.C., Canada, June 2006Google Scholar
- 4.Benaloh, J., Byrne, M., Kortum, P.T., McBurnett, N., Pereira, O., Stark, P.B., Wallach, D.S.: STAR-Vote: a secure, transparent, auditable, and reliable voting system. CoRR, abs/1211.1904 (2012)Google Scholar
- 5.Blanchet, B., Smyth, B.: Automated reasoning for equivalences in the applied pi calculus with barriers. In: CSF (2016)Google Scholar
- 6.Boichut, Y., Heam, P.C., Kouchnarenko, O., Oehl, F.: Improvements on the Genet and Klay technique to automatically verify security protocols. In: Workshop on Automated Verification of Infinite States Systems (2004)Google Scholar
- 11.Cremers, C.J.F., Lafourcade, P., Nadeau, P.: Comparing state spaces in automatic security protocol analysis. In: Formal to Practical Security - Papers Issued from the 2005–2008 French-Japanese Collaboration (2009)Google Scholar
- 16.Hussain, M., Seret, D.: A comparative study of security protocols validation tools: hermes vs. avispa. In: 2006 8th International Conference Advanced Communication Technology, vol. 1, pp. 303–308, 6 pages, February 2006Google Scholar
- 17.Lafourcade, P., Puys, M.: Performance evaluations of cryptographic protocols verification tools dealing with algebraic properties. In: Foundations and Practice of Security (FPS 2015), Clermont-Ferrand, France, October 2015Google Scholar
- 21.Moran, M., Heather, J.: Automated analysis of voting systems with dolev-yao intruder model. In: AVOCS 2013, September 2013Google Scholar
- 22.Moran, M., Heather, J., Schneider, S.: Verifying anonymity in voting systems using CSP. Formal Aspects Comput., 1–36 (2012)Google Scholar
- 23.Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), December 1978Google Scholar
- 24.Smyth, B.: Formal verification of cryptographic protocols with automated reasoning. Ph.D. thesis, School of Computer Science, University of Birmingham (2011)Google Scholar