Paper published in a book (Scientific congresses, symposiums and conference proceedings)
Cast-as-Intended: A Formal Definition and Case Studies
ROENNE, Peter; RYAN, Peter Y A; SMYTH, Benjamin
2021 • In Bernhard, Matthew (Ed.) Financial Cryptography and Data Security. FC 2021 International Workshops - CoDecFin, DeFi, VOTING, and WTSC, Revised Selected Papers
[en] Verifiable voting systems allow voters to check whether their ballot is correctly recorded (individual verifiability) and allow anyone to check whether votes expressed in recorded ballots are correctly counted (universal verifiability). This suffices to ensure that honest voters’ votes are correctly counted, assuming ballots are properly generated. Achieving ballot assurance, i.e., assuring each voter that their vote is correctly encoded inside their ballot, whilst ensuring privacy, is a challenging aspect of voting system design. This assurance property is known as cast-as-intended. Unlike many properties of voting systems, it has yet to be formalised. We provide the first formal definition and apply our definition to MarkPledge, Prêt à Voter, Selene, ThreeBallot, and schemes based upon Benaloh challenges.
Disciplines :
Computer science
Author, co-author :
ROENNE, Peter ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > APSIA
RYAN, Peter Y A ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS) ; DCS & Interdisciplinary Centre for Security, Reliability and Trust, Esch-sur-Alzette, Luxembourg
SMYTH, Benjamin ; University of Luxembourg ; DCS & Interdisciplinary Centre for Security, Reliability and Trust, Esch-sur-Alzette, Luxembourg
External co-authors :
no
Language :
English
Title :
Cast-as-Intended: A Formal Definition and Case Studies
Publication date :
2021
Event name :
6th Workshop on Advances in Secure Electronic Voting
Event date :
05-03-2021 => 05-03-2021
Audience :
International
Main work title :
Financial Cryptography and Data Security. FC 2021 International Workshops - CoDecFin, DeFi, VOTING, and WTSC, Revised Selected Papers
Editor :
Bernhard, Matthew
Publisher :
Springer Science and Business Media Deutschland GmbH
FNR12685695 - Socio-technical Verification Of Information Security And Trust In Voting Systems, 2018 (01/09/2019-31/08/2022) - Peter Y. A. Ryan FNR13643617 - Secure, Quantum-safe, Practical Voting Technologies, 2019 (01/04/2020-31/03/2023) - Peter Y. A. Ryan
Funding text :
Acknowledgements. This work received financial support from the Luxembourg National Research Fund (FNR) under the PolLux/CORE project STV (12685695) and the FNR CORE project EquiVox (13643617).
Benaloh, J.: Ballot casting assurance via voter-initiated poll station auditing. In: EVT 2007: Electronic Voting Technology Workshop. USENIX Association (2007)
Bernhard, D., Cortier, V., Galindo, D., Pereira, O., Warinschi, B.: SoK: a comprehensive analysis of game-based ballot privacy definitions. In: S&P 2015: 36th Security and Privacy Symposium, pp. 499–516. IEEE Computer Society (2015)
Blanchet, B., Smyth, B.: Automated reasoning for equivalences in the applied pi calculus with barriers. J. Comput. Secur. 26(3), 367–422 (2018)
Chaum, D.: Secret-ballot receipts and transparent integrity. Better and less-costly electronic voting at polling places. IEEE S&P 4 (2004)
Chaum, D., Ryan, P.Y.A., Schneider, S.: A practical voter-verifiable election scheme. In: di Vimercati, S.C., Syverson, P., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 118–139. Springer, Heidelberg (2005). https://doi.org/10. 1007/11555827 8
Cortier, V., Galindo, D., Küsters, R., Mueller, J., Truderung, T.: SoK: verifiability notions for e-voting protocols. In: S&P 2016: 37th IEEE Symposium on Security and Privacy, pp. 779–798. IEEE Computer Society (2016)
Cremers, C., Hirschi, L.: Improving automated symbolic analysis for e-voting protocols: a method based on sufficient conditions for ballot secrecy. arXiv, Report 1709.00194, September 2017
Culnane, C., Teague, V.: Strategies for voter-initiated election audits. In: Zhu, Q., Alpcan, T., Panaousis, E., Tambe, M., Casey, W. (eds.) GameSec 2016. LNCS, vol. 9996, pp. 235–247. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47413-7 14
Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4), 435–487 (2009)
Distler, V., Zollinger, M.-L., Lallemand, C., Rønne, P.B., Ryan, P.Y.A., Koenig, V.: Security-visible, yet unseen? In: Brewster, S.A., Fitzpatrick, G., Cox, A.L., Kostakos, V., (eds.) Proceedings of the 2019 CHI Conference on Human Factors in Computing Systems, CHI 2019, Glasgow, Scotland, UK, 04–09 May 2019, p. 605. ACM (2019)
Fraser, A., Quaglia, E.A., Smyth, B.: A critique of game-based definitions of receipt-freeness for voting. In: Steinfeld, R., Yuen, T.H. (eds.) ProvSec 2019. LNCS, vol. 11821, pp. 189–205. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31919-9 11
Iovino, V., Rial, A., Rønne, P.B., Ryan, P.Y.A.: Using selene to verify your vote in JCJ. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 385–403. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70278-0 24
Iovino, V., Rial, A., Rønne, P.B., Ryan, P.Y.A.: Universal unconditional verifiability in e-voting without trusted parties. In: 33rd IEEE Computer Security Foundations Symposium, CSF 2020, Boston, MA, USA, 22–26 June 2020, pp. 33–48. IEEE (2020)
Jamroga, W., Knapik, M., Kurpiewski, D.: Model checking the SELENE e-voting protocol in multi-agent logics. In: Krimmer, R., et al. (eds.) E-Vote-ID 2018. LNCS, vol. 11143, pp. 100–116. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00419-4 7
Juels, A., Catalano, D., Jakobsson, M.: Coercion-resistant electronic elections. In: Chaum, D., et al. (eds.) Towards Trustworthy Elections. LNCS, vol. 6000, pp. 37–63. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12980-3 2
Kiayias, A., Zacharias, T., Zhang, B.: End-to-end verifiable elections in the standard model. In: Oswald, E., Fischlin, M. (eds.) EUROCRYPT 2015. LNCS, vol. 9057, pp. 468–498. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46803-6 16
Kremer, S., Ryan, M., Smyth, B.: Election verifiability in electronic voting protocols. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 389–404. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15497-3 24
Küsters, R., Müller, J., Scapin, E., Truderung, T.: sElect: a lightweight verifiable remote voting system. In: 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pp. 341–354. IEEE (2016)
Küsters, R., Truderung, T., Vogt, A.: Accountability: definition and relationship to verifiability. In: CCS 2010: 17th ACM Conference on Computer and Communications Security, pp. 526–535. ACM Press (2010)
Küsters, R., Truderung, T., Vogt, A.: A game-based definition of coercion-resistance and its applications. J. Comput. Secur. 20(6), 709–764 (2012)
Moran, T., Naor, M.: Receipt-free universally-verifiable voting with everlasting privacy. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol. 4117, pp. 373–392. Springer, Heidelberg (2006). https://doi.org/10.1007/11818175 22
Andrew Neff, C.: Practical high certainty intent verification for encrypted votes. Unpublished manuscript (2004)
Andrew Neff, C.: Practical high certainty intent verification for encrypted votes (2004)
Rivest, R.L.: The threeballot voting system (2006)
Rønne, P.B., Ryan, P.Y.A., Zollinger, M.-L.: Electryo, in-person voting with transparent voter verifiability and eligibility verifiability. In: E-Vote-ID 2018, p. 147 (2018)
Ryan, P.Y.A., Rønne, P.B., Iovino, V.: Selene: voting with transparent verifiability and coercion-mitigation. In: Clark, J., Meiklejohn, S., Ryan, P.Y.A., Wallach, D., Brenner, M., Rohloff, K. (eds.) FC 2016. LNCS, vol. 9604, pp. 176–192. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53357-4 12
Sallal, M., et al.: Augmenting an internet voting system with selene verifiability using permissioned distributed ledger. In: 40th IEEE International Conference on Distributed Computing Systems, ICDCS 2020, Singapore, 29 November–1 December 2020, pp. 1167–1168. IEEE (2020)
Smyth, B.: Ballot secrecy: security definition, sufficient conditions, and analysis of Helios. Cryptology ePrint Archive, Report 2015/942 (2018)
Smyth, B.: Mind the gap: individual-and universal-verifiability plus cast-as-intended don’t yield verifiable voting systems. Technical Report 2020/1054, Cryptology ePrint Archive (2020)
Smyth, B.: Surveying global verifiability. Inf. Process. Lett. 163, 106000 (2020)
Smyth, B., Bernhard, D.: Ballot secrecy and ballot independence coincide. In: Crampton, J., Jajodia, S., Mayes, K. (eds.) ESORICS 2013. LNCS, vol. 8134, pp. 463–480. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40203-6 26
Smyth, B., Frink, S., Clarkson, M.R.: Election verifiability: cryptographic definitions and an analysis of Helios and JCJ. Cryptology ePrint Archive, Report 2015/233 (2017)
Smyth, B., Ryan, M., Kremer, S., Kourjieh, M.: Towards automatic analysis of election verifiability properties. In: Armando, A., Lowe, G. (eds.) ARSPA-WITS 2010. LNCS, vol. 6186, pp. 146–163. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16074-5 11
Unruh, D., Müller-Quade, J.: Universally composable incoercibility. In: Rabin, T. (ed.) CRYPTO 2010. LNCS, vol. 6223, pp. 411–428. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14623-7 22
Zollinger, M.-L., Distler, V., Roenne, P., Ryan, P., Lallemand, C., Vincent, K.: How mental models align with security mechanisms, user experience design for e-voting (2019)
Zollinger, M.-L., Rønne, P.B., Ryan, P.Y.A.: Short paper: mechanized proofs of verifiability and privacy in a paper-based e-voting scheme. In: Bernhard, M., et al. (eds.) FC 2020. LNCS, vol. 12063, pp. 310–318. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-54455-3 22
