A Type Theoretic Investigation of the Verification of Voting Protocols

As the world becomes more digital we see a greater push for digital elections, but we need to be cautious when we modernize to make sure we don't introduce issues that affect the election. These issues are related to trust, on the one hand, how can we trust that the result of the election is correct, and on the other hand we can we trust that the secrecy of the vote is preserved. These seemingly contradictory statements have fuelled new developments in cryptography, but the question remain can we trust these developments?

The thesis of my dissertation is that it possible to formalise the proofs used to justify both the correctness and security of such cryptographic constructions inside type theory. This requires a theory of probabilities in order to describe the probabilistic algorithms used. My contributions include, using types and type isomorphisms to simplify both specification and calculation of probabilities, in particular ∑-types are used as they correspond to summation. Furthermore, I extend the type theory with process algebraic constructions in order to capture attack games as defined by semantic security in cryptography. To type these processes I propose a session type system based on based on linear logic, extended with the possibility of depending on the actual messages sent. I prove the consistency of this extension by giving a model of it in Agda. These contributions are combined to form a library, which is named CryptoAgda, to reason about cryptography, and as an example of the approach I prove the receipt freeness of Prêt à voter using this model.