-
A Declaration of Software Independence
Authors:
Wojciech Jamroga,
Peter Y. A. Ryan,
Steve Schneider,
Carsten Schurmann,
Philip B. Stark
Abstract:
A voting system should not merely report the outcome: it should also provide sufficient evidence to convince reasonable observers that the reported outcome is correct. Many deployed systems, notably paperless DRE machines still in use in US elections, fail certainly the second, and quite possibly the first of these requirements. Rivest and Wack proposed the principle of software independence (SI)…
▽ More
A voting system should not merely report the outcome: it should also provide sufficient evidence to convince reasonable observers that the reported outcome is correct. Many deployed systems, notably paperless DRE machines still in use in US elections, fail certainly the second, and quite possibly the first of these requirements. Rivest and Wack proposed the principle of software independence (SI) as a guiding principle and requirement for voting systems. In essence, a voting system is SI if its reliance on software is ``tamper-evident'', that is, if there is a way to detect that material changes were made to the software without inspecting that software. This important notion has so far been formulated only informally.
Here, we provide more formal mathematical definitions of SI. This exposes some subtleties and gaps in the original definition, among them: what elements of a system must be trusted for an election or system to be SI, how to formalize ``detection'' of a change to an election outcome, the fact that SI is with respect to a set of detection mechanisms (which must be legal and practical), the need to limit false alarms, and how SI applies when the social choice function is not deterministic.
△ Less
Submitted 26 October, 2023;
originally announced November 2023.
-
Verification of the Socio-Technical Aspects of Voting: The Case of the Polish Postal Vote 2020
Authors:
Wojciech Jamroga,
Peter Y. A. Ryan,
Yan Kim
Abstract:
Voting procedures are designed and implemented by people, for people, and with significant human involvement. Thus, one should take into account the human factors in order to comprehensively analyze properties of an election and detect threats. In particular, it is essential to assess how actions and strategies of the involved agents (voters, municipal office employees, mail clerks) can influence…
▽ More
Voting procedures are designed and implemented by people, for people, and with significant human involvement. Thus, one should take into account the human factors in order to comprehensively analyze properties of an election and detect threats. In particular, it is essential to assess how actions and strategies of the involved agents (voters, municipal office employees, mail clerks) can influence the outcome of other agents' actions as well as the overall outcome of the election. In this paper, we present our first attempt to capture those aspects in a formal multi-agent model of the Polish presidential election 2020. The election marked the first time when postal vote was universally available in Poland. Unfortunately, the voting scheme was prepared under time pressure and political pressure, and without the involvement of experts. This might have opened up possibilities for various kinds of ballot fraud, in-house coercion, etc. We propose a preliminary scalable model of the procedure in the form of a Multi-Agent Graph, and formalize selected integrity and security properties by formulas of agent logics. Then, we transform the models and formulas so that they can be input to the state-of-art model checker Uppaal. The first series of experiments demonstrates that verification scales rather badly due to the state-space explosion. However, we show that a recently developed technique of user-friendly model reduction by variable abstraction allows us to verify more complex scenarios.
△ Less
Submitted 18 October, 2023; v1 submitted 19 October, 2022;
originally announced October 2022.
-
PakeMail: authentication and key management in decentralized secure email and messaging via PAKE
Authors:
Itzel Vazquez Sandoval,
Arash Atashpendar,
Gabriele Lenzini,
Peter Y. A. Ryan
Abstract:
We propose the use of PAKE for achieving and enhancing entity authentication (EA) and key management (KM) in the context of decentralized end-to-end encrypted email and secure messaging, i.e., where neither a public key infrastructure nor trusted third parties are used. This approach not only simplifies the EA process by requiring users to share only a low-entropy secret, e.g., a memorable word, b…
▽ More
We propose the use of PAKE for achieving and enhancing entity authentication (EA) and key management (KM) in the context of decentralized end-to-end encrypted email and secure messaging, i.e., where neither a public key infrastructure nor trusted third parties are used. This approach not only simplifies the EA process by requiring users to share only a low-entropy secret, e.g., a memorable word, but it also allows us to establish a high-entropy secret key; this key enables a series of cryptographic enhancements and security properties, which are hard to achieve using out-of-band (OOB) authentication. We first study a few vulnerabilities in voice-based OOB authentication, in particular a combinatorial attack against lazy users, which we analyze in the context of a secure email solution. We then propose tackling public key authentication by solving the problem of "secure equality test" using PAKE, and discuss various protocols and their properties. This method enables the automation of important KM tasks (e.g. key renewal and future key pair authentications), reduces the impact of human errors, and lends itself to the asynchronous nature of email and modern messaging. It also provides cryptographic enhancements including multi-device synchronization and secure secret storage/retrieval, and paves the path for forward secrecy, deniability and post-quantum security. We also discuss the use of auditable PAKEs for mitigating a class of online guess and abort attacks in authentication protocols. To demonstrate the feasibility of our proposal, we present PakeMail, an implementation of the core idea, and discuss some of its cryptographic details, implemented features and efficiency aspects. We conclude with some design and security considerations, followed by future lines of work.
△ Less
Submitted 13 July, 2021;
originally announced July 2021.
-
User Experience Design for E-Voting: How mental models align with security mechanisms
Authors:
Marie-Laure Zollinger,
Verena Distler,
Peter B. Roenne,
Peter Y. A. Ryan,
Carine Lallemand,
Vincent Koenig
Abstract:
This paper presents a mobile application for vote-casting and vote-verification based on the Selene e-voting protocol and explains how it was developed and implemented using the User Experience Design process. The resulting interface was tested with 38 participants, and user experience data was collected via questionnaires and semi-structured interviews on user experience and perceived security. R…
▽ More
This paper presents a mobile application for vote-casting and vote-verification based on the Selene e-voting protocol and explains how it was developed and implemented using the User Experience Design process. The resulting interface was tested with 38 participants, and user experience data was collected via questionnaires and semi-structured interviews on user experience and perceived security. Results concerning the impact of displaying security mechanisms on UX were presented in a complementary paper. Here we expand on this analysis by studying the mental models revealed during the interviews and compare them with theoretical security notions. Finally, we propose a list of improvements for designs of future voting protocols.
△ Less
Submitted 15 June, 2021; v1 submitted 31 May, 2021;
originally announced May 2021.
-
Electryo, In-person Voting with Transparent Voter Verifiability and Eligibility Verifiability
Authors:
Peter B. Roenne,
Peter Y. A Ryan,
Marie-Laure Zollinger
Abstract:
Selene is an e-voting protocol that allows voters to directly check their individual vote, in cleartext, in the final tally via a tracker system, while providing good coercion mitigation. This is in contrast to conventional, end-to-end verifiable schemes in which the voter verifies the presence of an encryption of her vote on the bulletin board. The Selene mechanism can be applied to many e-voting…
▽ More
Selene is an e-voting protocol that allows voters to directly check their individual vote, in cleartext, in the final tally via a tracker system, while providing good coercion mitigation. This is in contrast to conventional, end-to-end verifiable schemes in which the voter verifies the presence of an encryption of her vote on the bulletin board. The Selene mechanism can be applied to many e-voting schemes, but here we present an application to the polling station context, resulting in a voter-verifiable electronic tally with a paper audit trail. The system uses a smartcard-based public key system to provide the individual verification and universal eligibility verifiability. The paper record contains an encrypted link to the voter's identity, requiring stronger assumptions on ballot privacy than normal paper voting, but with the benefit of providing good auditability and dispute resolution as well as supporting (comparison) risk limiting audits.
△ Less
Submitted 31 May, 2021;
originally announced May 2021.
-
Convergence Voting: From Pairwise Comparisons to Consensus
Authors:
Gergei Bana,
Wojciech Jamroga,
David Naccache,
Peter Y. A. Ryan
Abstract:
An important aspect of AI design and ethics is to create systems that reflect aggregate preferences of the society. To this end, the techniques of social choice theory are often utilized. We propose a new social choice function motivated by the PageRank algorithm. The function ranks voting options based on the Condorcet graph of pairwise comparisons. To this end, we transform the Condorcet graph i…
▽ More
An important aspect of AI design and ethics is to create systems that reflect aggregate preferences of the society. To this end, the techniques of social choice theory are often utilized. We propose a new social choice function motivated by the PageRank algorithm. The function ranks voting options based on the Condorcet graph of pairwise comparisons. To this end, we transform the Condorcet graph into a Markov chain whose stationary distribution provides the scores of the options. We show how the values in the stationary distribution can be interpreted as quantified aggregate support for the voting options, to which the community of voters converges through an imaginary sequence of negotiating steps. Because of that, we suggest the name "convergence voting" for the new voting scheme, and "negotiated community support" for the resulting stationary allocation of scores.
Our social choice function can be viewed as a consensus voting method, sitting somewhere between Copeland and Borda. On the one hand, it does not necessarily choose the Condorcet winner, as strong support from a part of the society can outweigh mediocre uniform support. On the other hand, the influence of unpopular candidates on the outcome is smaller than in the primary technique of consensus voting, i.e., the Borda count. We achieve that without having to introduce an ad hoc weighting that some other methods do.
△ Less
Submitted 1 March, 2021; v1 submitted 3 February, 2021;
originally announced February 2021.
-
A Survey of Requirements for COVID-19 Mitigation Strategies. Part I: Newspaper Clips
Authors:
Wojciech Jamroga,
David Mestel,
Peter B. Roenne,
Peter Y. A. Ryan,
Marjan Skrobot
Abstract:
The COVID-19 pandemic has influenced virtually all aspects of our lives. Across the world, countries have applied various mitigation strategies for the epidemic, based on social, political, and technological instruments. We postulate that one should {identify the relevant requirements} before committing to a particular mitigation strategy. One way to achieve it is through an overview of what is co…
▽ More
The COVID-19 pandemic has influenced virtually all aspects of our lives. Across the world, countries have applied various mitigation strategies for the epidemic, based on social, political, and technological instruments. We postulate that one should {identify the relevant requirements} before committing to a particular mitigation strategy. One way to achieve it is through an overview of what is considered relevant by the general public, and referred to in the media. To this end, we have collected a number of news clips that mention the possible goals and requirements for a mitigation strategy. The snippets are sorted thematically into several categories, such as health-related goals, social and political impact, civil rights, ethical requirements, and so on.
In a forthcoming companion paper, we will present a digest of the requirements, derived from the news clips, and a preliminary take on their formal specification.
△ Less
Submitted 18 October, 2023; v1 submitted 16 November, 2020;
originally announced November 2020.
-
Model Checkers Are Cool: How to Model Check Voting Protocols in Uppaal
Authors:
Wojciech Jamroga,
Yan Kim,
Damian Kurpiewski,
Peter Y. A. Ryan
Abstract:
The design and implementation of an e-voting system is a challenging task. Formal analysis can be of great help here. In particular, it can lead to a better understanding of how the voting system works, and what requirements on the system are relevant. In this paper, we propose that the state-of-art model checker Uppaal provides a good environment for modelling and preliminary verification of voti…
▽ More
The design and implementation of an e-voting system is a challenging task. Formal analysis can be of great help here. In particular, it can lead to a better understanding of how the voting system works, and what requirements on the system are relevant. In this paper, we propose that the state-of-art model checker Uppaal provides a good environment for modelling and preliminary verification of voting protocols. To illustrate this, we present an Uppaal model of Prêt à Voter, together with some natural extensions. We also show how to verify a variant of receipt-freeness, despite the severe limitations of the property specification language in the model checker.
△ Less
Submitted 18 October, 2023; v1 submitted 24 July, 2020;
originally announced July 2020.
-
Preservation of DNA Privacy During the Large Scale Detection of COVID-19
Authors:
Marcel Hollenstein,
David Naccache,
Peter B. Rønne,
Peter Y A Ryan,
Robert Weil,
Ofer Yifrach-Stav
Abstract:
As humanity struggles to contain the global COVID-19 pandemic, privacy concerns are emerging regarding confinement, tracing and testing. The scientific debate concerning privacy of the COVID-19 tracing efforts has been intense, especially focusing on the choice between centralised and decentralised tracing apps. The privacy concerns regarding COVID-19 testing, however, have not received as much at…
▽ More
As humanity struggles to contain the global COVID-19 pandemic, privacy concerns are emerging regarding confinement, tracing and testing. The scientific debate concerning privacy of the COVID-19 tracing efforts has been intense, especially focusing on the choice between centralised and decentralised tracing apps. The privacy concerns regarding COVID-19 testing, however, have not received as much attention even though the privacy at stake is arguably even higher. COVID-19 tests require the collection of samples. Those samples possibly contain viral material but inevitably also human DNA. Patient DNA is not necessary for the test but it is technically impossible to avoid collecting it. The unlawful preservation, or misuse, of such samples at a massive scale may hence disclose patient DNA information with far-reaching privacy consequences. Inspired by the cryptographic concept of "Indistinguishability under Chosen Plaintext Attack", this paper poses the blueprint of novel types of tests allowing to detect viral presence without leaving persisting traces of the patient's DNA. Authors are listed in alphabetical order.
△ Less
Submitted 1 August, 2020; v1 submitted 17 July, 2020;
originally announced July 2020.
-
Risk-Limiting Tallies
Authors:
Wojciech Jamroga,
Peter B. Roenne,
Peter Y. A. Ryan,
Philip B. Stark
Abstract:
Many voter-verifiable, coercion-resistant schemes have been proposed, but even the most carefully designed systems necessarily leak information via the announced result. In corner cases, this may be problematic. For example, if all the votes go to one candidate then all vote privacy evaporates. The mere possibility of candidates getting no or few votes could have implications for security in pract…
▽ More
Many voter-verifiable, coercion-resistant schemes have been proposed, but even the most carefully designed systems necessarily leak information via the announced result. In corner cases, this may be problematic. For example, if all the votes go to one candidate then all vote privacy evaporates. The mere possibility of candidates getting no or few votes could have implications for security in practice: if a coercer demands that a voter cast a vote for such an unpopular candidate, then the voter may feel obliged to obey, even if she is confident that the voting system satisfies the standard coercion resistance definitions. With complex ballots, there may also be a danger of "Italian" style (aka "signature") attacks: the coercer demands the voter cast a ballot with a specific, identifying pattern. Here we propose an approach to tallying end-to-end verifiable schemes that avoids revealing all the votes but still achieves whatever confidence level in the announced result is desired. Now a coerced voter can claim that the required vote must be amongst those that remained shrouded. Our approach is based on the well-established notion of Risk-Limiting Audits, but here applied to the tally rather than to the audit. We show that this approach counters coercion threats arising in extreme tallies and "Italian" attacks. We illustrate our approach by applying it to the Selene scheme, and we extend the approach to Risk-Limiting Verification, where not all vote trackers are revealed, thereby enhancing the coercion mitigation properties of Selene.
△ Less
Submitted 14 August, 2019;
originally announced August 2019.
-
Coercion-Resistant Voting in Linear Time via Fully Homomorphic Encryption: Towards a Quantum-Safe Scheme
Authors:
Peter B. Rønne,
Arash Atashpendar,
Kristian Gjøsteen,
Peter Y. A. Ryan
Abstract:
We present an approach for performing the tallying work in the coercion-resistant JCJ voting protocol, introduced by Juels, Catalano, and Jakobsson, in linear time using fully homomorphic encryption (FHE). The suggested enhancement also paves the path towards making JCJ quantum-resistant, while leaving the underlying structure of JCJ intact. The exhaustive, comparison-based approach of JCJ using p…
▽ More
We present an approach for performing the tallying work in the coercion-resistant JCJ voting protocol, introduced by Juels, Catalano, and Jakobsson, in linear time using fully homomorphic encryption (FHE). The suggested enhancement also paves the path towards making JCJ quantum-resistant, while leaving the underlying structure of JCJ intact. The exhaustive, comparison-based approach of JCJ using plaintext equivalence tests leads to a quadratic blow-up in the number of votes, which makes the tallying process rather impractical in realistic settings with a large number of voters. We show how the removal of invalid votes can be done in linear time via a solution based on recent advances in various FHE primitives such as hashing, zero-knowledge proofs of correct decryption, verifiable shuffles and threshold FHE. We conclude by touching upon some of the advantages and challenges of such an approach, followed by a discussion of further security and post-quantum considerations.
△ Less
Submitted 5 February, 2019; v1 submitted 8 January, 2019;
originally announced January 2019.
-
Revisiting Deniability in Quantum Key Exchange via Covert Communication and Entanglement Distillation
Authors:
Arash Atashpendar,
G. Vamsi Policharla,
Peter B. Rønne,
Peter Y. A. Ryan
Abstract:
We revisit the notion of deniability in quantum key exchange (QKE), a topic that remains largely unexplored. In the only work on this subject by Donald Beaver, it is argued that QKE is not necessarily deniable due to an eavesdrop** attack that limits key equivocation. We provide more insight into the nature of this attack and how it extends to other constructions such as QKE obtained from unclon…
▽ More
We revisit the notion of deniability in quantum key exchange (QKE), a topic that remains largely unexplored. In the only work on this subject by Donald Beaver, it is argued that QKE is not necessarily deniable due to an eavesdrop** attack that limits key equivocation. We provide more insight into the nature of this attack and how it extends to other constructions such as QKE obtained from uncloneable encryption. We then adopt the framework for quantum authenticated key exchange, developed by Mosca et al., and extend it to introduce the notion of coercer-deniable QKE, formalized in terms of the indistinguishability of real and fake coercer views. Next, we apply results from a recent work by Arrazola and Scarani on covert quantum communication to establish a connection between covert QKE and deniability. We propose DC-QKE, a simple deniable covert QKE protocol, and prove its deniability via a reduction to the security of covert QKE. Finally, we consider how entanglement distillation can be used to enable information-theoretically deniable protocols for QKE and tasks beyond key exchange.
△ Less
Submitted 5 December, 2018;
originally announced December 2018.
-
A Proof of Entropy Minimization for Outputs in Deletion Channels via Hidden Word Statistics
Authors:
Arash Atashpendar,
David Mestel,
A. W. Roscoe,
Peter Y. A. Ryan
Abstract:
From the output produced by a memoryless deletion channel from a uniformly random input of known length $n$, one obtains a posterior distribution on the channel input. The difference between the Shannon entropy of this distribution and that of the uniform prior measures the amount of information about the channel input which is conveyed by the output of length $m$, and it is natural to ask for whi…
▽ More
From the output produced by a memoryless deletion channel from a uniformly random input of known length $n$, one obtains a posterior distribution on the channel input. The difference between the Shannon entropy of this distribution and that of the uniform prior measures the amount of information about the channel input which is conveyed by the output of length $m$, and it is natural to ask for which outputs this is extremized. This question was posed in a previous work, where it was conjectured on the basis of experimental data that the entropy of the posterior is minimized and maximized by the constant strings $\texttt{000}\ldots$ and $\texttt{111}\ldots$ and the alternating strings $\texttt{0101}\ldots$ and $\texttt{1010}\ldots$ respectively. In the present work we confirm the minimization conjecture in the asymptotic limit using results from hidden word statistics. We show how the analytic-combinatorial methods of Flajolet, Szpankowski and Vallée for dealing with the hidden pattern matching problem can be applied to resolve the case of fixed output length and $n\rightarrow\infty$, by obtaining estimates for the entropy in terms of the moments of the posterior distribution and establishing its minimization via a measure of autocorrelation.
△ Less
Submitted 30 July, 2018;
originally announced July 2018.
-
CryptoRec: Privacy-preserving Recommendation as a Service
Authors:
Jun Wang,
Afonso Arriaga,
Qiang Tang,
Peter Y. A. Ryan
Abstract:
Recommender systems rely on large datasets of historical data and entail serious privacy risks. A server offering Recommendation as a Service to a client might leak more information than necessary regarding its recommendation model and dataset. At the same time, the disclosure of the client's preferences to the server is also a matter of concern. Devising privacy-preserving protocols using general…
▽ More
Recommender systems rely on large datasets of historical data and entail serious privacy risks. A server offering Recommendation as a Service to a client might leak more information than necessary regarding its recommendation model and dataset. At the same time, the disclosure of the client's preferences to the server is also a matter of concern. Devising privacy-preserving protocols using general cryptographic primitives (e.g., secure multi-party computation or homomorphic encryption), is a typical approach to overcome privacy concerns, but in conjunction with state-of-the-art recommender systems often yields far-from-practical solutions.
In this paper, we tackle this problem from the direction of constructing crypto-friendly machine learning algorithms. In particular, we propose CryptoRec, a secure two-party computation protocol for Recommendation as a Service, which encompasses a novel recommender system. This model possesses two interesting properties: (1) It models user-item interactions in an item-only latent feature space in which personalized user representations are automatically captured by an aggregation of pre-learned item features. This means that a server with a pre-trained model can provide recommendations for a client whose data is not in its training set. Nevertheless, re-training the model with the client's data still improves accuracy. (2) It only uses addition and multiplication operations, making the model straightforwardly compatible with homomorphic encryption schemes.
We demonstrate the efficiency and accuracy of CryptoRec on three real-world datasets. CryptoRec allows a server with thousands of items to privately answer a prediction query within a few seconds on a single PC, while its prediction accuracy is still competitive with state-of-the-art recommender systems computing over clear data.
△ Less
Submitted 13 May, 2018; v1 submitted 7 February, 2018;
originally announced February 2018.
-
From Clustering Supersequences to Entropy Minimizing Subsequences for Single and Double Deletions
Authors:
Arash Atashpendar,
Marc Beunardeau,
Aisling Connolly,
Rémi Géraud,
David Mestel,
A. W. Roscoe,
Peter Y. A. Ryan
Abstract:
A binary string transmitted via a memoryless i.i.d. deletion channel is received as a subsequence of the original input. From this, one obtains a posterior distribution on the channel input, corresponding to a set of candidate supersequences weighted by the number of times the received subsequence can be embedded in them. In a previous work it is conjectured on the basis of experimental data that…
▽ More
A binary string transmitted via a memoryless i.i.d. deletion channel is received as a subsequence of the original input. From this, one obtains a posterior distribution on the channel input, corresponding to a set of candidate supersequences weighted by the number of times the received subsequence can be embedded in them. In a previous work it is conjectured on the basis of experimental data that the entropy of the posterior is minimized and maximized by the constant and the alternating strings, respectively. In this work, in addition to revisiting the entropy minimization conjecture, we also address several related combinatorial problems. We present an algorithm for counting the number of subsequence embeddings using a run-length encoding of strings. We then describe methods for clustering the space of supersequences such that the cardinality of the resulting sets depends only on the length of the received subsequence and its Hamming weight, but not its exact form. Then, we consider supersequences that contain a single embedding of a fixed subsequence, referred to as singletons, and provide a closed form expression for enumerating them using the same run-length encoding. We prove an analogous result for the minimization and maximization of the number of singletons, by the alternating and the uniform strings, respectively. Next, we prove the original minimal entropy conjecture for the special cases of single and double deletions using similar clustering techniques and the same run-length encoding, which allow us to characterize the distribution of the number of subsequence embeddings in the space of compatible supersequences to demonstrate the effect of an entropy decreasing operation.
△ Less
Submitted 4 March, 2019; v1 submitted 2 February, 2018;
originally announced February 2018.
-
Public Evidence from Secret Ballots
Authors:
Matthew Bernhard,
Josh Benaloh,
J. Alex Halderman,
Ronald L. Rivest,
Peter Y. A. Ryan,
Philip B. Stark,
Vanessa Teague,
Poorvi L. Vora,
Dan S. Wallach
Abstract:
Elections seem simple---aren't they just counting? But they have a unique, challenging combination of security and privacy requirements. The stakes are high; the context is adversarial; the electorate needs to be convinced that the results are correct; and the secrecy of the ballot must be ensured. And they have practical constraints: time is of the essence, and voting systems need to be affordabl…
▽ More
Elections seem simple---aren't they just counting? But they have a unique, challenging combination of security and privacy requirements. The stakes are high; the context is adversarial; the electorate needs to be convinced that the results are correct; and the secrecy of the ballot must be ensured. And they have practical constraints: time is of the essence, and voting systems need to be affordable and maintainable, and usable by voters, election officials, and pollworkers. It is thus not surprising that voting is a rich research area spanning theory, applied cryptography, practical systems analysis, usable security, and statistics. Election integrity involves two key concepts: convincing evidence that outcomes are correct and privacy, which amounts to convincing assurance that there is no evidence about how any given person voted. These are obviously in tension. We examine how current systems walk this tightrope.
△ Less
Submitted 4 August, 2017; v1 submitted 26 July, 2017;
originally announced July 2017.
-
(Universal) Unconditional Verifiability in E-Voting without Trusted Parties
Authors:
Gina Gallegos-Garcia,
Vincenzo Iovino,
Alfredo Rial,
Peter B. Roenne,
Peter Y. A. Ryan
Abstract:
In traditional e-voting protocols, privacy is often provided by a trusted authority that learns the votes and computes the tally. Some protocols replace the trusted authority by a set of authorities, and privacy is guaranteed if less than a threshold number of authorities are corrupt. For verifiability, stronger security guarantees are demanded. Typically, corrupt authorities that try to fake the…
▽ More
In traditional e-voting protocols, privacy is often provided by a trusted authority that learns the votes and computes the tally. Some protocols replace the trusted authority by a set of authorities, and privacy is guaranteed if less than a threshold number of authorities are corrupt. For verifiability, stronger security guarantees are demanded. Typically, corrupt authorities that try to fake the result of the tally must always be detected.
To provide verifiability, many e-voting protocols use Non-Interactive Zero-Knowledge proofs (NIZKs). Thanks to their non-interactive nature, NIZKs allow anybody, including third parties that do not participate in the protocol, to verify the correctness of the tally. Therefore, NIZKs can be used to obtain universal verifiability. Additionally, NIZKs also improve usability because they allow voters to cast a vote using a non-interactive protocol.
The disadvantage of NIZKs is that their security is based on setup assumptions such as the common reference string (CRS) or the random oracle (RO) model. The former requires a trusted party for the generation of a common reference string. The latter, though a popular methodology for designing secure protocols, has been shown to be unsound.
In this paper, we address the design of an e-voting protocol that provides verifiability without any trust assumptions, where verifiability here is meant without eligibility verification. We show that Non-Interactive Witness-Indistinguishable proofs (NIWI) can be used for this purpose. The e-voting scheme is private under the Decision Linear assumption, while verifiability holds unconditionally. To our knowledge, this is the first private e-voting scheme with perfect universal verifiability, i.e. one in which the probability of a fake tally not being detected is 0, and with {\em non-interactive} protocols that does not rely on trust assumptions.
△ Less
Submitted 20 October, 2016;
originally announced October 2016.
-
End-to-end verifiability
Authors:
Josh Benaloh,
Ronald Rivest,
Peter Y. A. Ryan,
Philip Stark,
Vanessa Teague,
Poorvi Vora
Abstract:
This pamphlet describes end-to-end election verifiability (E2E-V) for a nontechnical audience: election officials, public policymakers, and anyone else interested in secure, transparent, evidence-based electronic elections.
This work is part of the Overseas Vote Foundation's End-to-End Verifiable Internet Voting: Specification and Feasibility Assessment Study (E2E VIV Project), funded by the Dem…
▽ More
This pamphlet describes end-to-end election verifiability (E2E-V) for a nontechnical audience: election officials, public policymakers, and anyone else interested in secure, transparent, evidence-based electronic elections.
This work is part of the Overseas Vote Foundation's End-to-End Verifiable Internet Voting: Specification and Feasibility Assessment Study (E2E VIV Project), funded by the Democracy Fund.
△ Less
Submitted 14 April, 2015;
originally announced April 2015.
-
vVote: a Verifiable Voting System
Authors:
Chris Culnane,
Peter Y. A. Ryan,
Steve Schneider,
Vanessa Teague
Abstract:
The Pret a Voter cryptographic voting system was designed to be flexible and to offer voters a familiar and easy voting experience. In this paper we present a case study of our efforts to adapt Pret a Voter to the idiosyncrasies of elections in the Australian state of Victoria. This technical report includes general background, user experience and details of the cryptographic protocols and human p…
▽ More
The Pret a Voter cryptographic voting system was designed to be flexible and to offer voters a familiar and easy voting experience. In this paper we present a case study of our efforts to adapt Pret a Voter to the idiosyncrasies of elections in the Australian state of Victoria. This technical report includes general background, user experience and details of the cryptographic protocols and human processes. We explain the problems, present solutions, then analyse their security properties and explain how they tie in to other design decisions. We hope this will be an interesting case study on the application of end-to-end verifiable voting protocols to real elections.
A preliminary version of this paper appeared as the 10th February 2014 version of "Draft Technical Report for VEC vVote System".
The team involved in develo** the vVote design described in this report were: Craig Burton, Chris Culnane, James Heather, Rui Joaquim, Peter Y. A. Ryan, Steve Schneider and Vanessa Teague.
△ Less
Submitted 20 September, 2015; v1 submitted 27 April, 2014;
originally announced April 2014.
-
Formal Modelling of a Usable Identity Management Solution for Virtual Organisations
Authors:
Ali N. Haidar,
P. V. Coveney,
Ali E. Abdallah,
P. Y. A Ryan,
B. Beckles,
J. M. Brooke,
M . A. S. Jones
Abstract:
This paper attempts to accurately model security requirements for computational grid environments with particular focus on authentication. We introduce the Audited Credential Delegation (ACD) architecture as a solution to some of the virtual organisations identity management usability problems. The approach uses two complementary models: one is state based, described in Z notation, and the other…
▽ More
This paper attempts to accurately model security requirements for computational grid environments with particular focus on authentication. We introduce the Audited Credential Delegation (ACD) architecture as a solution to some of the virtual organisations identity management usability problems. The approach uses two complementary models: one is state based, described in Z notation, and the other is event-based, expressed in the Process Algebra of Hoare's Communicating Sequential Processes (CSP). The former will be used to capture the state of the WS and to model back-end operations on it whereas the latter will be used to model behavior, and in particular, front-end interactions and communications. The modelling helps to clearly and precisely understand functional and security requirements and provide a basis for verifying that the system meets its intended requirements.
△ Less
Submitted 27 January, 2010;
originally announced January 2010.