Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Issue title: Selected papers from the 35th IEEE Computer Security Foundations Symposium – CSF 2022
Guest editors: Stefano Calzavara and David Naumann
Article type: Research Article
Authors: Drăgan, Constantin Cătălina | Dupressoir, Françoisb | Estaji, Ehsanc | Gjøsteen, Kristiand | Haines, Thomase | Ryan, Peter Y.A.f | Rønne, Peter B.g; h | Solberg, Morten Rotvoldi; *
Affiliations: [a] Surrey Centre for Cyber Security, University of Surrey, Guildford, United Kingdom | [b] Department of Computer Science, University of Bristol, Bristol, United Kingdom | [c] Department of Computer Science & SnT, University of Luxembourg, Esch-sur-Alzette, Luxembourg | [d] Department of Mathematical Sciences, NTNU, Trondheim, Norway | [e] School of Computing, Australian National University, Canberra, Australia | [f] Department of Computer Science & SnT, University of Luxembourg, Esch-sur-Alzette, Luxembourg | [g] LORIA, CNRS & Univ Lorraine, France | [h] University of Luxembourg, Esch-sur-Alzette, Luxembourg | [i] Department of Mathematical Sciences, NTNU, Trondheim, Norway
Correspondence: [*] Corresponding author. E-mail: mosolb@ntnu.no.
Note: [1] This paper is an extended and revised version of a paper presented at CSF’22.
Abstract: 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.
Keywords: Formal verification, e-voting, Selene, privacy
DOI: 10.3233/JCS-230045
Journal: Journal of Computer Security, vol. 31, no. 5, pp. 469-499, 2023
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl