Search

The Prêt à Voter cryptographic voting system was designed to be flexible and to offer voters a familiar and easy voting experience. In this article, we present our development of the Prêt à Voter design to a practical implementation used in a real state election in November 2014, called vVote. As well as solving practical engineering challenges, we have also had to tailor the system to the idiosyncrasies of elections in the Australian state of Victoria and the requirements of the Victorian Electoral Commission. This article includes general background, user experience, and details of the cryptographic protocols and human processes. We explain the problems, present solutions, then analyze their security properties and explain how they tie in to other design decisions. [ABSTRACT FROM AUTHOR]

Election security isn't a simple matter of a secure system defending against attacks from an external adversary. Elections must provide sound evidence of an accurate outcome even when the adversary writes the software, administers the election, or runs the country. This special issue contains four articles concerned with different aspects of end-to-end verifiability, which provides technical means for voters and observers to confirm that an election has handled votes correctly from casting to tallying. [ABSTRACT FROM PUBLISHER]

Abstract: We prove properties of a process calculus that is designed for analysing security protocols. Our long-term goal is to develop a form of protocol analysis, consistent with standard cryptographic assumptions, that provides a language for expressing probabilistic polynomial-time protocol steps, a specification method based on a compositional form of equivalence, and a logical basis for reasoning about equivalence. The process calculus is a variant of CCS, with bounded replication and probabilistic polynomial-time expressions allowed in messages and boolean tests. To avoid inconsistency between security and nondeterminism, messages are scheduled probabilistically instead of nondeterministically. We prove that evaluation of any process expression halts in probabilistic polynomial time and define a form of asymptotic protocol equivalence that allows security properties to be expressed using observational equivalence, a standard relation from programming language theory that involves quantifying over all possible environments that might interact with the protocol. We develop a form of probabilistic bisimulation and use it to establish the soundness of an equational proof system based on observational equivalences. The proof system is illustrated by a formation derivation of the assertion, well-known in cryptography, that El Gamal encryption''s semantic security is equivalent to the (computational) Decision Diffie–Hellman assumption. This example demonstrates the power of probabilistic bisimulation and equational reasoning for protocol security. [Copyright &y& Elsevier]