Verificatum Mix-Net

This is our main product and the result of research and implementation efforts spread out over 13 years. Readers with a background in cryptography can look at the list of implemented protocols to get an overview and then consult the comprehensive technical documentation at the download page, including the technical fact sheet.

Basic Functionality of a Mix-Net

A mix-net is a protocol executed by a set of mix-servers. They first generate a public key such that the secret key is shared among the servers in such a way that any subset that is sufficiently large could recover the secret key and no subset smaller than this gains any knowledge about the secret key even if they collude. However, the mix-servers never recover the secret key. To decrypt a list of ciphertexts, they instead run a protocol that allows them to simultaneously re-order the input ciphertexts and decrypt them. This is illustrated in Figure 1 below.

             
         Figure 1. Voters encrypt their votes using a public key and a submission scheme and the resulting list of encrypted votes is simultaneously re-ordered and decrypted by the mix-net.

This is the most basic and classical way to use a mix-net, but it is also possible to re-order the ciphertexts without decrypting them in such a way that the output ciphertexts look like fresh encryptions of the same set of votes. Again, this is done without recovering any secret key. Moreover one can decrypt without re-ordering. There are many more variations that turn out to be useful in practice and our mix-net can perform all of them.

In a broad class of electronic voting systems a mix-net is used to tally the result in a secure and verifiable way. It is the main cryptographic component and constitutes much of the technically challenging software in the voting system as a whole.

An additional output of the mix-net is a non-interactive zero-knowledge proof of correctness. This allows anybody to write a program to verify the correctness of the complete execution without learning anything about how the messages were re-ordered. In particular the proof reveals nothing about the secret key. Since anybody can verify it and this is a particularly important property in electronic voting, it is sometimes called a universally verifiable proof. In practice one must of course require that the format of this proof is specified precisely for this to be a meaningful claim.

The Verificatum Mix-Net

Our mix-net has been used in real binding elections to tally more than 3,000,000 votes. This includes party leader elections in Israel, municipal elections in Norway, primary and local elections in Spain, and local and national elections in Estonia.

Our mix-net has a number of unique features that makes it the best mix-net in the world. The most obvious is that it is by far the most mature and refined implementation of a mix-net existing today.

It is easy to use and more flexible in functionality than any other mix-net. This is not only convenient and saves development costs for other parts of a complete system, it is an important security feature. For example, you can process multiple ciphertexts submitted by a single voter as a unit in ranked elections, you can decrypt parts of a ciphertext for partial tallying, you can shuffle without decrypting or the converse, etc.

Thus, we provide a powerful toolbox that can handle all mix-net based protocols we are aware of. There are mature manuals with worked examples for all the functionality. However, we welcome questions from users who are unsure if a mix-net can solve their problems.

All our code is of exceptional quality. We simply do not release any code that does not fulfil stringent quality requirements. These include testing, documentation, static analysis, systematic refinement and rewriting solely for clarity, and human analysis.

We wrote all our code from scratch and it has a single dependency to the to Gnu Multi-precision Library, the best library for multi-precision arithmetic in the world. The main author helped us write some arithmetic routines. This unique feature means that we do not have to worry about unknown or unvetted developers that commit code. It is also practical in terms of maintainability of the code, but our uncompromising approach is motivated by security.

The conservative principle of minimizing the number of dependencies is applied not only to the core software that is written in Java and C. All the necessary scripts are written in POSIX shell script to reduce the risk of accidentally executing a slightly modified version of a shell that has security flaws. As a consequence our software is portable across a wide variety of Linux and Unix systems without any need of special configuration or installing extra libraries.

Our mix-net is provably secure in its abstract form and the only mix-net existing today that is truly universally verifiable. No other mix-net is even fully documented. It is optimized in many ways, but not to the point that it harms readability and auditability of the code. This includes: rewriting of protocols, special arithmetic optimizations, native code where it matters, threading, and parallelization.