-
Towards Verifiable Remote Voting with Paper Assurance
Authors:
Eleanor McMurtry,
Xavier Boyen,
Chris Culnane,
Kristian Gjøsteen,
Thomas Haines,
Vanessa Teague
Abstract:
We propose a protocol for verifiable remote voting with paper assurance. It is intended to augment existing postal voting procedures, allowing a ballot to be electronically constructed, printed on paper, then returned in the post. It allows each voter to verify that their vote has been correctly cast, recorded and tallied by the Electoral Commission. The system is not end-to-end verifiable, but do…
▽ More
We propose a protocol for verifiable remote voting with paper assurance. It is intended to augment existing postal voting procedures, allowing a ballot to be electronically constructed, printed on paper, then returned in the post. It allows each voter to verify that their vote has been correctly cast, recorded and tallied by the Electoral Commission. The system is not end-to-end verifiable, but does allow voters to detect manipulation by an adversary who controls either the voting device, or (the postal service and electoral commission) but not both. The protocol is not receipt-free, but if the client honestly follows the protocol (including possibly remembering everything), they cannot subsequently prove how they voted. Our proposal is the first to combine plain paper assurance with cryptographic verification in a (passively) receipt-free manner.
△ Less
Submitted 9 November, 2021; v1 submitted 7 November, 2021;
originally announced November 2021.
-
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.
-
Adversaries monitoring Tor traffic crossing their jurisdictional border and reconstructing Tor circuits
Authors:
Herman Galteland,
Kristian Gjøsteen
Abstract:
We model and analyze passive adversaries that monitors Tor traffic crossing the border of a jurisdiction an adversary is controlling. We show that a single adversary is able to connect incoming and outgoing traffic of their border, tracking the traffic, and cooperating adversaries are able to reconstruct parts of the Tor network, revealing user-server relationships. In our analysis we created two…
▽ More
We model and analyze passive adversaries that monitors Tor traffic crossing the border of a jurisdiction an adversary is controlling. We show that a single adversary is able to connect incoming and outgoing traffic of their border, tracking the traffic, and cooperating adversaries are able to reconstruct parts of the Tor network, revealing user-server relationships. In our analysis we created two algorithms to estimate the capabilities of the adversaries. The first generates Tor-like traffic and the second analyzes and reconstructs the simulated data.
△ Less
Submitted 21 January, 2020; v1 submitted 28 August, 2018;
originally announced August 2018.
-
On the Construction of Quasi-Binary and Quasi-Orthogonal Matrices over Finite Fields
Authors:
Danilo Gligoroski,
Kristian Gjosteen,
Katina Kralevska
Abstract:
Orthogonal and quasi-orthogonal matrices have a long history of use in digital image processing, digital and wireless communications, cryptography and many other areas of computer science and coding theory. The practical benefits of using orthogonal matrices come from the fact that the computation of inverse matrices is avoided, by simply using the transpose of the orthogonal matrix. In this paper…
▽ More
Orthogonal and quasi-orthogonal matrices have a long history of use in digital image processing, digital and wireless communications, cryptography and many other areas of computer science and coding theory. The practical benefits of using orthogonal matrices come from the fact that the computation of inverse matrices is avoided, by simply using the transpose of the orthogonal matrix. In this paper, we introduce a new family of matrices over finite fields that we call \emph{Quasi-Binary and Quasi-Orthogonal Matrices}. We call the matrices quasi-binary due to the fact that matrices have only two elements $a, b \in \mathbb{F}_q$, but those elements are not $0$ and $1$. In addition, the reason why we call them quasi-orthogonal is due to the fact that their inverses are obtained not just by a simple transposition, but there is a need for an additional operation: a replacement of $a$ and $b$ by two other values $c$ and $d$. We give a simple relation between the values $a, b, c$ and $d$ for any finite field and especially for finite fields with characteristic 2. Our construction is based on incident matrices from cyclic Latin Rectangles and the efficiency of the proposed algorithm comes from the avoidance of matrix-matrix or matrix-vector multiplications.
△ Less
Submitted 20 January, 2018;
originally announced January 2018.
-
A framework for compositional verification of security protocols
Authors:
Suzana Andova,
Cas Cremers,
Kristian Gjosteen,
Sjouke Mauw,
Stig F. Mjolsnes,
Sasa Radomirovic
Abstract:
Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach.
We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verifi…
▽ More
Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach.
We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verification of large structured security protocols. Our approach is to verify properties of component protocols in a multi-protocol environment, then deduce properties about the composed protocol. To reduce the complexity of multi-protocol verification, we introduce a notion of protocol independence and prove a number of theorems that enable analysis of independent component protocols in isolation.
To illustrate the applicability of our framework to real-world protocols, we study a key establishment sequence in WiMax consisting of three subprotocols. Except for a small amount of trivial reasoning, the analysis is done using automatic tools.
△ Less
Submitted 1 May, 2007; v1 submitted 14 November, 2006;
originally announced November 2006.
