Skip to main content
Erschienen in: Software and Systems Modeling 4/2016

06.01.2015 | Theme Section Paper

Automated anonymity verification of the ThreeBallot and VAV voting systems

verfasst von: Murat Moran, James Heather, Steve Schneider

Erschienen in: Software and Systems Modeling | Ausgabe 4/2016

Einloggen

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

In recent years, a large number of secure voting protocols have been proposed in the literature. Often these protocols contain flaws, but because they are complex protocols, rigorous formal analysis has proven hard to come by. Rivest’s ThreeBallot and Vote/Anti-Vote/Vote (VAV) voting systems are important because they aim to provide security (voter anonymity and voter verifiability) without requiring cryptography. In this paper, we construct CSP models of ThreeBallot and VAV, and use them to produce the first automated formal analysis of their anonymity properties. Along the way, we discover that one of the crucial assumptions under which ThreeBallot and VAV (and many other voting systems) operate—the short ballot assumption—is highly ambiguous in the literature. We give various plausible precise interpretations and discover that in each case, the interpretation either is unrealistically strong or else fails to ensure anonymity. We give a revised version of the short ballot assumption for ThreeBallot and VAV that is realistic but still provides a guarantee of anonymity.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Fußnoten
1
A previous version of this paper appeared in the Proceedings of the 10th International Conference on Integrated Formal Methods, Springer LNCS 7940. The final publication is available at http://​link.​springer.​com/​chapter/​10.​1007%2F978-3-642-38613-8_​7.
 
2
The CSP model of ThreeBallot voting system, from which the experimental results given in this paper were produced, can be downloaded from the first author’s personal webpage http://​muratmoran.​wordpress.​com/​publications/​ under the CSP codes title. It is also available on the departmental webpage http://​epubs.​surrey.​ac.​uk/​id/​eprint/​804928.
 
Literatur
1.
Zurück zum Zitat Chaum, D.: Untraceable electronic mail, return addresses, and digital pseudonyms. Commun. ACM 24, 84–90 (1981)CrossRef Chaum, D.: Untraceable electronic mail, return addresses, and digital pseudonyms. Commun. ACM 24, 84–90 (1981)CrossRef
2.
Zurück zum Zitat Fujioka, A., Okamoto, T., Ohta, K.: A practical secret voting scheme for large scale elections. In: AUSCRYPT, pp. 244–251 (1992) Fujioka, A., Okamoto, T., Ohta, K.: A practical secret voting scheme for large scale elections. In: AUSCRYPT, pp. 244–251 (1992)
3.
Zurück zum Zitat Juels, A., Catalano, D., Jakobsson, M.: Coercion-resistant electronic elections. In: IACR Cryptology ePrint Archive, p. 165 (2002) Juels, A., Catalano, D., Jakobsson, M.: Coercion-resistant electronic elections. In: IACR Cryptology ePrint Archive, p. 165 (2002)
4.
Zurück zum Zitat Chaum, D., Ryan, P.Y.A., Schneider, S.A.: A practical voter-verifiable election scheme. In: ESORICS, pp. 118–139 (2005) Chaum, D., Ryan, P.Y.A., Schneider, S.A.: A practical voter-verifiable election scheme. In: ESORICS, pp. 118–139 (2005)
7.
8.
Zurück zum Zitat Gardiner, P., Goldsmith, M., Hulance, J., Jackson, D., Roscoe, B., Scattergood, B., Armstrong, B.: FDR2 user manual Gardiner, P., Goldsmith, M., Hulance, J., Jackson, D., Roscoe, B., Scattergood, B., Armstrong, B.: FDR2 user manual
9.
Zurück zum Zitat Backes, M., Hritcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: CSF, pp. 195–209 (2008) Backes, M., Hritcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: CSF, pp. 195–209 (2008)
10.
Zurück zum Zitat Smyth, B.: Formal verification of cryptographic protocols with automated reasoning. Ph.D. thesis, School of Computer Science, University of Birmingham (2011) Smyth, B.: Formal verification of cryptographic protocols with automated reasoning. Ph.D. thesis, School of Computer Science, University of Birmingham (2011)
11.
Zurück zum Zitat Ryan, P.Y.A., Schneider, S.A.: Prêt à Voter with re-encryption mixes. In: ESORICS, pp. 313–326 (2006) Ryan, P.Y.A., Schneider, S.A.: Prêt à Voter with re-encryption mixes. In: ESORICS, pp. 313–326 (2006)
12.
Zurück zum Zitat Moran, M., Heather, J., Schneider, S.: Verifying anonymity in voting systems using CSP. Form. Asp. Comput. 26(1), 63–98 (2014) Moran, M., Heather, J., Schneider, S.: Verifying anonymity in voting systems using CSP. Form. Asp. Comput. 26(1), 63–98 (2014)
13.
Zurück zum Zitat Cichon, J., Kutylowski, M., Weglorz, B.: Short ballot assumption and threeballot voting protocol. In: SOFSEM, pp. 585–598 (2008) Cichon, J., Kutylowski, M., Weglorz, B.: Short ballot assumption and threeballot voting protocol. In: SOFSEM, pp. 585–598 (2008)
14.
Zurück zum Zitat de Marneffe, O., Pereira, O., Quisquater, J.J.: Simulation-based analysis of E2E voting systems. In: Proceedings of the 1st International Conference on E-voting and Identity. VOTE-ID’07. Springer, Berlin, Heidelberg, pp. 137–149 (2007) de Marneffe, O., Pereira, O., Quisquater, J.J.: Simulation-based analysis of E2E voting systems. In: Proceedings of the 1st International Conference on E-voting and Identity. VOTE-ID’07. Springer, Berlin, Heidelberg, pp. 137–149 (2007)
17.
Zurück zum Zitat Clark, J., Essex, A., Adams, C.: On the security of ballot receipts in E2E voting systems. In: IAVoSS Workshop on Trustworthy Elections (WOTE) (2007) Clark, J., Essex, A., Adams, C.: On the security of ballot receipts in E2E voting systems. In: IAVoSS Workshop on Trustworthy Elections (WOTE) (2007)
18.
Zurück zum Zitat Appel, A.W.: How to Defeat Rivest’s ThreeBallot Voting System (2007) Appel, A.W.: How to Defeat Rivest’s ThreeBallot Voting System (2007)
19.
Zurück zum Zitat Tjøstheim, T., Peacock, T., Ryan, P.Y.A.: A case study in system-based analysis: the ThreeBallot voting system and Prêt à Voter. In: VoComp (2007) Tjøstheim, T., Peacock, T., Ryan, P.Y.A.: A case study in system-based analysis: the ThreeBallot voting system and Prêt à Voter. In: VoComp (2007)
20.
Zurück zum Zitat Henry, K., Stinson, D.R., Sui, J.: The effectiveness of receipt-based attacks on Threeballot. Trans. Inf. Forensic Secur. 4(4), 699–707 (2009)CrossRef Henry, K., Stinson, D.R., Sui, J.: The effectiveness of receipt-based attacks on Threeballot. Trans. Inf. Forensic Secur. 4(4), 699–707 (2009)CrossRef
21.
Zurück zum Zitat Küsters, R., Truderung, T., Vogt, A.: Verifiability, privacy, and coercion–resistance: new insights from a case study. In: IEEE Symposium on Security and Privacy (SP), pp. 538–553 (2011) Küsters, R., Truderung, T., Vogt, A.: Verifiability, privacy, and coercion–resistance: new insights from a case study. In: IEEE Symposium on Security and Privacy (SP), pp. 538–553 (2011)
22.
Zurück zum Zitat Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: Proceedings of 42nd IEEE Symposium on Foundations of Computer Science, pp. 136–145 (2001) Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: Proceedings of 42nd IEEE Symposium on Foundations of Computer Science, pp. 136–145 (2001)
23.
Zurück zum Zitat Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1997) Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River (1997)
24.
Zurück zum Zitat Lazic, R.S.: A semantic study of data independence with applications to model checking. D.Phil. thesis, Oxford University Computing Laboratory (1999) Lazic, R.S.: A semantic study of data independence with applications to model checking. D.Phil. thesis, Oxford University Computing Laboratory (1999)
25.
Metadaten
Titel
Automated anonymity verification of the ThreeBallot and VAV voting systems
verfasst von
Murat Moran
James Heather
Steve Schneider
Publikationsdatum
06.01.2015
Verlag
Springer Berlin Heidelberg
Erschienen in
Software and Systems Modeling / Ausgabe 4/2016
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI
https://doi.org/10.1007/s10270-014-0445-x

Weitere Artikel der Ausgabe 4/2016

Software and Systems Modeling 4/2016 Zur Ausgabe