Skip to main content
SpringerLink
Log in

Vote Counting as Mathematical Proof

  • Conference paper
  • First Online:
AI 2015: Advances in Artificial Intelligence (AI 2015)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 9457))

Included in the following conference series:

Abstract

Trust in the correctness of an election outcome requires proof of the correctness of vote counting. By formalising particular voting protocols as rules, correctness of vote counting amounts to verifying that all rules have been applied correctly. A proof of the outcome of any particular election then consists of a sequence (or tree) of rule applications and provides an independently checkable certificate of the validity of the result. This reduces the need to trust, or otherwise verify, the correctness of the vote counting software once the certificate has been validated. Using a rule-based formalisation of voting protocols inside a theorem prover, we synthesise vote counting programs that are not only provably correct, but also produce independently verifiable certificates. These programs are generated from a (formal) proof that every initial set of ballots allows to decide the election winner according to a set of given rules.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Appel, A.W., Michael, N.G., Stump, A., Virga, R.: A trustworthy proof checker. J. Autom. Reasoning 31(3–4), 231–260 (2003)

    Article  MATH  Google Scholar 

  2. Beckert, B., Goré, R., Schürmann, C., Bormer, T., Wang, J.: Verifying voting schemes. J. Inf. Sec. Appl. 19(2), 115–129 (2014)

    Google Scholar 

  3. Bertot, Y., Castran, P., Huet, G., Paulin-Mohring, C.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)

    Book  Google Scholar 

  4. Chaum, D.: Secret-ballot receipts: true voter-verifiable elections. IEEE Secur. Priv. 2(1), 38–47 (2004)

    Article  Google Scholar 

  5. Cochran, D., Kiniry, J.: Votail: a formally specified and verified ballot counting system for irish PR-STV elections. In: Pre-proceedings of the 1st International Conference on Formal Verification of Object-Oriented Software (FoVeOOS) (2010)

    Google Scholar 

  6. Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols: a taster. In: Chaum, D., Jakobsson, M., Rivest, R.L., Ryan, P.Y.A., Benaloh, J., Kutylowski, M., Adida, B. (eds.) Towards Trustworthy Elections. LNCS, vol. 6000, pp. 289–309. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  7. DeYoung, H., Schürmann, C.: Linear logical voting protocols. In: Kiayias, A., Lipmaa, H. (eds.) VoteID 2011. LNCS, vol. 7187, pp. 53–70. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  8. Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  9. Software Improvements. Electronic and voting and counting sytems. http://www.softimp.com.au/evacs/index.html (2015). Accessed 12 May 2015

  10. Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 200–219. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  11. Marlow, S., Peyton Jones, S.: The glasgow haskell compiler. In: The Architecture of Open Source Applications, vol. 2. Lulu (2012)

    Google Scholar 

  12. Necula, G.C.: Proof-carrying code. In: Lee, P., Henglein, F., Jones, N.D. (eds.) Proceedings of the POPL 1997, pp. 106–119. ACM Press (1997)

    Google Scholar 

  13. Schürmann, C.: Electronic elections: trust through engineering. In: Proceedings of the RE-VOTE 2009, pp. 38–46. IEEE Computer Society (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The Australian National University, Canberra, Australia

    Dirk Pattinson

  2. IT University of Copenhagen, Copenhagen, Denmark

    Carsten Schürmann

Authors
  1. Dirk Pattinson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Carsten Schürmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Carsten Schürmann .

Editor information

Editors and Affiliations

  1. The University of Waikato, Hamilton, New Zealand

    Bernhard Pfahringer

  2. The Australian National University, Canberra, Aust Capital Terr, Australia

    Jochen Renz

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Pattinson, D., Schürmann, C. (2015). Vote Counting as Mathematical Proof. In: Pfahringer, B., Renz, J. (eds) AI 2015: Advances in Artificial Intelligence. AI 2015. Lecture Notes in Computer Science(), vol 9457. Springer, Cham. https://doi.org/10.1007/978-3-319-26350-2_41

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-26350-2_41

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-26349-6

  • Online ISBN: 978-3-319-26350-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation