Voting and blockchains are intimately connected. Voting is used in blockchains for consensus, governance, and decentralized organizations (DAOs). Conversely, blockchains can serve as a bulletin board for smaller elections. For these applications, the stakes are high, both financial and societal. Moreover, for blockchains, the adversarial model is complex: the adversary has complete knowledge of the system and full access to the network.

Here we focus on the use of blockchains for smaller elections; so-called boardroom voting. We consider one such protocol: the Open Vote Network (OVN), which provides private voting on a blockchain. Such private voting could also be applied to a DAO, improving the state of the art where voting for DAOs is often pseudonymous instead of private.

The OVN protocol has previously been implemented as a smart contract on Ethereum. It comes with an informal security argument. We propose a more complete analysis, which we formalize in the Coq proof assistant. We thus provide, for the first time, a complete analysis of a cryptographic smart contract, which is both provably functionally correct and cryptographically secure. We are extending this to a more realistic implementation.