This post is a continuation of A mixnet-based secure voting protocol and A typed purely-functional state machine. We briefly describe a prototype implementation of the former which uses techniques from the latter. An election, like baking a cake, can be understood as a process which advances in steps, ie a simple state machine. This state machine was specified in our protocol post. We can therefore apply the typed functional approach to the case of an election. The main characteristics of this approach were

  • States are modeled as types
  • State information is captured in type structure
  • The current state is modeled as a type constructor parameterized by State
  • State transitions are pure functions encoding constraints with types

In order to model the voting protocol we also need some way to represent the fact that elections require a certain number of trustees, and that certain state transitions require the participation of all these trustees before the state can advance. As before, we would like to do this with types. The technique we apply is

  • The number of trustees is represented with a type level encoding of natural numbers
  • State transitions with trustee participation include constraints based on natural number encodings

These last techniques are applied via the shapeless library. Let’s look at how each of these techniques are embodied in code. There is overlap, so some techniques will appear before they are explained.

States are modeled as types

Here we also include the second part of the technique: information available at each state is captured in the structure of the type. Thus the types corresponding to states serve two purposes. First, to nominally mark the state the machine is in. Second, to record information available at that state.

A general state is represented by the abstract ElectionState. After that, each specific state of the machine has its own type. Its fields capture the information available at that point in the process.  This enforces, at compile time, that a certain state must have certain information coupled to it. Note that we have left out some implementation details that allow easier extraction of state history.

Current state is a type constructor

The Election type takes two parameters, the second of which is one of the concrete states we just saw. An instance of an Election represents the election at some point during its evolution.

The current step in this evolution of the state machine is indicated by the second type parameter S, whereas the information about the election at that point is captured by its state field. Naturally, the state field type matches the parameter S.

Transitions are type constrained pure functions

Here we see how the type signatures of the transition methods embody the state machine specification.

Because states and state information correspond to types, transitions can encode the rules of the state machine such that it is a compile time error to violate them. The type signatures require a certain state as input, and provide a certain state as output, as seen in second type parameter of the Election type constructor. For example

It would be a compile-error to start an election with no public key (Combined state). Similarly

It would be a compile-time error to decrypt without shuffling (Mixed state). And so forth for all state transitions.

Type level encoding of number of trustees

Up to now we’ve seen how the techniques described in our previous post can be used for a real world election prototype. But the voting protocol has another type of constraint we have not seen yet, certain transitions must occur depending on a variable number of operations. We have three cases of this

  • Each authority creates its share of the key and posts the public fragment, along with proofs of correctness, at the bulletin board. The bulletin board then checks the proofs and combines the shares, resulting in the public key.
  • Each mixing authority permutes and re-encrypts the votes handling them as input to the next authority. Once all the authorities have completed the mix and the bulletin board has verified all the proofs the mixing phase is over.
  • Each authority downloads the mixed votes from the bulletin board and calculates their partial decryptions using its private share of the key, along with corresponding proofs of correctness. Once all partial decryptions are available the bulletin board combines them and subsequently obtains the plaintexts.

In effect, this requires a variable state machine parameterized by a number, the number of trustees, which specifies a variable number of states and transitions present in each of the three examples above. Of course, one could always “flatten” these into normal states and transitions, but that would be messy and result in code bloat. What we want is some way to have a parameterized state machine which preserves our compile time guarantees. We can do this is via a type level representation of the said parameter, we use shapeless for this.

As we noted before, the current step in evolution of the state machine is indicated by the second type parameter S. But now we know what the first parameter W represents, it is the type level encoding of the number of trustees in the election. It is a subtype of Nat, because Nat is the shapeless encoding of a Natural number. The variable number of states we need for the three cases above are provided by the following

We now see where the type parameters [T <: Nat] comes from. If we go back to the full list of state classes we see it is only these three which feature this. Just like the state machine as a whole contains a current state parameter, these three “composite states” do too. In a way, in representing a variable number of states, these three classes are like a mini state machine in themselves.

Finally, we need to ensure that the transitions away from these states behave according to the number of trustees. In other words, the number of variable states must matches this number, and the steps within the mini-state machines should also match. Here’s how this is enforced

The important part of the signatures is

which requires that the number of state transitions inside each composite state is always less than the number of trustees. When such number is equal, we can invoke the transition out of the state, which is enforced in

because the input of the transition is

where the current state parameter matches the number of trustees parameter. Working together these implementation features result in

  • It is a compile time error to try to generate the public key without all the shares
  • It is a compile time error to try to complete the mixing phase without all the mixes
  • It is a compile time error to try to decrypt the votes without all the partial decryptions

which is what we wanted.

Summing up

We’ve seen how the techniques introduced in the previous post together with others based on type level encoding of natural numbers allow us to enforce the logic of a more sophisticated, real world state machine corresponding to a cryptographically secure voting prototype. Violations of these constraints are compile time errors, and it is not possible to arrive at an inconsistent state. In addition, the purely functional approach is especially suited to a voting prototype because this allows auditing all the steps in the process. Since we are not using destructive mutation, all the information accumulated during the process is available to review.