{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T11:03:46Z","timestamp":1777806226914,"version":"3.51.4"},"reference-count":20,"publisher":"SAGE Publications","issue":"5","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["JCS"],"published-print":{"date-parts":[[2023,10,13]]},"abstract":"<jats:p>Privacy is a notoriously difficult property to achieve in complicated systems and especially in electronic voting schemes. Moreover, electronic voting schemes is a class of systems that require very high assurance. The literature contains a number of ballot privacy definitions along with security proofs for common systems. Some machine-checked security proofs have also appeared. We define a new ballot privacy notion that captures a larger class of voting schemes. This notion improves on the state of the art by taking into account that verification in many schemes will happen or must happen after the tally has been published, not before as in previous definitions. As a case study we give a machine-checked proof of privacy for Selene, which is a remote electronic voting scheme which offers an attractive mix of security properties and usability. Prior to our work, the computational privacy of Selene has never been formally verified. Finally, we also prove that MiniVoting and Belenios satisfies our definition.<\/jats:p>","DOI":"10.3233\/jcs-230045","type":"journal-article","created":{"date-parts":[[2023,6,9]],"date-time":"2023-06-09T10:31:27Z","timestamp":1686306687000},"page":"469-499","source":"Crossref","is-referenced-by-count":1,"title":["Machine-checked proofs of privacy against malicious boards for Selene &amp; Co1"],"prefix":"10.1177","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4033-9880","authenticated-orcid":false,"given":"Constantin C\u0103t\u0103lin","family":"Dr\u0103gan","sequence":"first","affiliation":[{"name":"Surrey Centre for Cyber Security, University of Surrey, Guildford, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3497-3110","authenticated-orcid":false,"given":"Fran\u00e7ois","family":"Dupressoir","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Bristol, Bristol, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ehsan","family":"Estaji","sequence":"additional","affiliation":[{"name":"Department of Computer Science & SnT, University of Luxembourg, Esch-sur-Alzette, Luxembourg"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kristian","family":"Gj\u00f8steen","sequence":"additional","affiliation":[{"name":"Department of Mathematical Sciences, NTNU, Trondheim, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Haines","sequence":"additional","affiliation":[{"name":"School of Computing, Australian National University, Canberra, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1677-9034","authenticated-orcid":false,"given":"Peter Y.A.","family":"Ryan","sequence":"additional","affiliation":[{"name":"Department of Computer Science & SnT, University of Luxembourg, Esch-sur-Alzette, Luxembourg"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2785-8301","authenticated-orcid":false,"given":"Peter B.","family":"R\u00f8nne","sequence":"additional","affiliation":[{"name":"LORIA, CNRS & Univ Lorraine, France"},{"name":"University of Luxembourg, Esch-sur-Alzette, Luxembourg"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Morten Rotvold","family":"Solberg","sequence":"additional","affiliation":[{"name":"Department of Mathematical Sciences, NTNU, Trondheim, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","reference":[{"key":"10.3233\/JCS-230045_ref1","first-page":"146","volume-title":"EasyCrypt: A Tutorial","author":"Barthe","year":"2014"},{"key":"10.3233\/JCS-230045_ref2","doi-asserted-by":"crossref","unstructured":"M.\u00a0Bellare and P.\u00a0Rogaway, Random oracles are practical: A paradigm for designing efficient protocols, in: ACM CCS 93, D.E.\u00a0Denning, R.\u00a0Pyle, R.\u00a0Ganesan, R.S.\u00a0Sandhu and V.\u00a0Ashby, eds, ACM Press, 1993, pp.\u00a062\u201373.","DOI":"10.1145\/168588.168596"},{"key":"10.3233\/JCS-230045_ref3","doi-asserted-by":"crossref","unstructured":"M.\u00a0Bellare and A.\u00a0Sahai, Non-malleable encryption: Equivalence between two notions, and an indistinguishability-based characterization, in: CRYPTO\u201999, M.J.\u00a0Wiener, ed., LNCS, vol.\u00a01666, Springer, Heidelberg, 1999, pp.\u00a0519\u2013536.","DOI":"10.1007\/3-540-48405-1_33"},{"key":"10.3233\/JCS-230045_ref5","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.37"},{"key":"10.3233\/JCS-230045_ref6","doi-asserted-by":"crossref","unstructured":"D.\u00a0Bernhard, V.\u00a0Cortier, O.\u00a0Pereira, B.\u00a0Smyth and B.\u00a0Warinschi, Adapting helios for provable ballot privacy, in: ESORICS 2011, V.\u00a0Atluri and C.\u00a0D\u00edaz, eds, LNCS, Vol.\u00a06879, Springer, Heidelberg, 2011, pp.\u00a0335\u2013354.","DOI":"10.1007\/978-3-642-23822-2_19"},{"key":"10.3233\/JCS-230045_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34961-4_38"},{"key":"10.3233\/JCS-230045_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68687-5_7"},{"key":"10.3233\/JCS-230045_ref9","doi-asserted-by":"crossref","unstructured":"P.\u00a0Chaidos, V.\u00a0Cortier, G.\u00a0Fuchsbauer and D.\u00a0Galindo, BeleniosRF: A non-interactive receipt-free electronic voting scheme, in: ACM CCS 2016, E.R.\u00a0Weippl, S.\u00a0Katzenbeisser, C.\u00a0Kruegel, A.C.\u00a0Myers and S.\u00a0Halevi, eds, ACM Press, 2016, pp.\u00a01614\u20131625.","DOI":"10.1145\/2976749.2978337"},{"key":"10.3233\/JCS-230045_ref10","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.28"},{"key":"10.3233\/JCS-230045_ref11","doi-asserted-by":"crossref","unstructured":"V.\u00a0Cortier, C.C.\u00a0Dragan, F.\u00a0Dupressoir and B.\u00a0Warinschi, Machine-checked proofs for electronic voting: Privacy and verifiability for Belenios, in: CSF 2018 Computer Security Foundations Symposium, S.\u00a0Chong and S.\u00a0Delaune, eds, IEEE Computer Society Press, 2018, pp.\u00a0298\u2013312.","DOI":"10.1109\/CSF.2018.00029"},{"key":"10.3233\/JCS-230045_ref12","doi-asserted-by":"crossref","unstructured":"V.\u00a0Cortier, D.\u00a0Galindo, S.\u00a0Glondu and M.\u00a0Izabach\u00e8ne, Election verifiability for helios under weaker trust assumptions, in: ESORICS 2014, Part II, M.\u00a0Kutylowski and J.\u00a0Vaidya, eds, LNCS, Vol.\u00a08713, Springer, Heidelberg, 2014, pp.\u00a0327\u2013344.","DOI":"10.1007\/978-3-319-11212-1_19"},{"key":"10.3233\/JCS-230045_ref13","doi-asserted-by":"crossref","unstructured":"V.\u00a0Cortier, J.\u00a0Lallemand and B.\u00a0Warinschi, Fifty shades of ballot privacy: Privacy against a malicious board, in: CSF 2020 Computer Security Foundations Symposium, L.\u00a0Jia and R.\u00a0K\u00fcsters, eds, IEEE Computer Society Press, 2020, pp.\u00a017\u201332.","DOI":"10.1109\/CSF49147.2020.00010"},{"key":"10.3233\/JCS-230045_ref14","doi-asserted-by":"publisher","DOI":"10.1109\/CSF54842.2022.9919663"},{"key":"10.3233\/JCS-230045_ref15","doi-asserted-by":"crossref","unstructured":"T.\u00a0ElGamal, A public key cryptosystem and a signature scheme based on discrete logarithms, in: CRYPTO\u201984, G.R.\u00a0Blakley and D.\u00a0Chaum, eds, LNCS, vol.\u00a0196, Springer, Heidelberg, 1984, pp.\u00a010\u201318.","DOI":"10.1007\/3-540-39568-7_2"},{"key":"10.3233\/JCS-230045_ref16","doi-asserted-by":"crossref","unstructured":"T.\u00a0Haines, R.\u00a0Gor\u00e9 and B.\u00a0Sharma, Did you mix me? Formally verifying verifiable mix nets in electronic voting, in: IEEE Symposium on Security and Privacy, IEEE, 2021, pp.\u00a01748\u20131765.","DOI":"10.1109\/SP40001.2021.00033"},{"key":"10.3233\/JCS-230045_ref17","doi-asserted-by":"crossref","unstructured":"T.\u00a0Haines, R.\u00a0Gor\u00e9 and M.\u00a0Tiwari, Verified verifiers for verifying elections, in: ACM CCS 2019, L.\u00a0Cavallaro, J.\u00a0Kinder, X.\u00a0Wang and J.\u00a0Katz, eds, ACM Press, 2019, pp.\u00a0685\u2013702.","DOI":"10.1145\/3319535.3354247"},{"key":"10.3233\/JCS-230045_ref18","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2016.42"},{"key":"10.3233\/JCS-230045_ref19","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.31"},{"key":"10.3233\/JCS-230045_ref21","doi-asserted-by":"crossref","unstructured":"P.Y.A.\u00a0Ryan, P.B.\u00a0R\u00f8nne and V.\u00a0Iovino, Selene: Voting with transparent verifiability and coercion-mitigation, in: FC 2016 Workshops, J.\u00a0Clark, S.\u00a0Meiklejohn, P.Y.A.\u00a0Ryan, D.S.\u00a0Wallach, M.\u00a0Brenner and K.\u00a0Rohloff, eds, LNCS, Vol.\u00a09604, Springer, Heidelberg, 2016, pp.\u00a0176\u2013192.","DOI":"10.1007\/978-3-662-53357-4_12"},{"key":"10.3233\/JCS-230045_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54455-3_22"}],"container-title":["Journal of Computer Security"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/JCS-230045","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T20:45:44Z","timestamp":1777495544000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/JCS-230045"}},"subtitle":[],"editor":[{"given":"Stefano","family":"Calzavara","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]},{"given":"David","family":"Naumann","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[2023,10,13]]},"references-count":20,"journal-issue":{"issue":"5"},"URL":"https:\/\/doi.org\/10.3233\/jcs-230045","relation":{},"ISSN":["1875-8924","0926-227X"],"issn-type":[{"value":"1875-8924","type":"electronic"},{"value":"0926-227X","type":"print"}],"subject":[],"published":{"date-parts":[[2023,10,13]]}}}