The Coq mailing list

[Eddy Westbrook <westbrook AT galois.com>]

Hey all,

Not sure if you are aware, but Joe Kiniry at Galois has been running a spin-out company dedicated to formally verified voting systems:

https://freeandfair.us/

IIUC, a lot of the challenge has been social, as Ralf pointed out, but on a different front: that of convincing governments (think municipal, county, and state governments, each of which have their own voting infrastructure) to invest in this technology.

DARPA has also funded some research in unhackable voting machines, and, as I think somebody pointed out, there are a number of conferences where the issue comes up, e.g. in the Defcon conference about security:

https://www.wired.com/story/darpa-voting-machine-defcon-voting-village-hackers/

-Eddy

On May 1, 2022, at 7:19 PM, Abhishek Anand <aa755 AT pm.me> wrote:

There seems to be some miscommunication so I will try to make my claim more precisely. In particular, I am not defending any currently deployed electronic voting systems. I am specifically advocating for end-to-end verifiable voting systems (which AFAIK have never been deployed): these do not have to be electronic or internet based: you can in theory run the crypto algo in your head and write or print out the encrypted "vote message" and mail it physically, possibly as a QR code. My key requirement is end-to-end verifiability: after the election, all the encrypted votes are publicly available -- possibly after some operation (e.g. permutation) for privacy -- for inspection and tallying (using something like homomorphic encryption).

Hi all,

What you describe here, Abhishek, is a social problem that I do not think can be
solved by technology. In fact I think it is made worse by technology (see e.g.
https://en.wikipedia.org/wiki/2004_United_States_election_voting_controversies).

I dont see how any of the problems in the wiki page (the version on 1-May-2022 at 9:30PM new york time) are worse for crypto end-to-end verifiable voting vs paper-based voting.

I still can't know that the computer I am voting with actually runs the code
that has been verified.

With most cryptographic voting schemes, the full protocol is open source. With Civitas (supports remote voting), you can implement your own software on your own computer.
Andrew Appel's article (https://freedom-to-tinker.com/2018/11/05/end-to-end-verifiable-elections/) mentions other convincing ways of probabilistic testing of the voting computers in case of in-person voting at machines not controlled by you.


And only very few people can actually understand the

arguments on which the integrity and correctness of this process is based.

True. But what good is understanding the process if you cannot verify that what happened in the election actually matched the process?

I agree with the others who said that one of the most important criteria of a
voting system is that everyone can understand it and be convinced that it works
as intended. I believe this criteria to be fundamentally unsatisfiable for any
form of electronic voting.

The "convinced that it works as intended part" is where the status quo fails miserably in the US. Even before mail-in voting became so prevalent, many doubted the integrity of election results, e.g. in 2016. Mail-in-voting seems to increase the TCB (interpreted liberally as the number of people who need to be trusted and for how long and how trustworthy those people are) by orders of magnitude. So I don't think it is irrational to not be convinced of integrity of the 2020 results. The only argument I have heard against that distrust is "well, there is no evidence of large-scale fraud". That is a very illogical argument IMO because lack of evidence of X is not evidence of ~X. Cryptographic end-to-end verifiable voting seems to me the most promising way to provide POSITIVE evidence of integrity. It is not perfect, but IMO it seems to drastically "reduce" the TCB at least in order to trust that the votes of rational tech-literate citizens were accounted properly. In other words, today, if a citizen wants to check whether after they mailed their ballot, their vote was counted correctly, AFAIK there is no way: they have to trust the many humans (often very polarized) that handled it after they mailed. With end-to-end verifiable voting, the citizen can check that their vote was accounted properly by looking at the PUBLIC database of encrypted votes: in civitas, as long as not ALL of the tabulation tellers were colluding.

In practice, there may be other requirements like citizens being able to keep their voting private keys secret: at least to prevent coercion. This is a non-trival problem, but can be solved by FM. (Many many non-computer-PhD/BS/MS citizens already use cryptocurrencies and with the Canada incident early this year, many if not most are increasingly storing their spending private keys in self-custody ("not your keys, not your coins"). I was recently at a crypto conference and there seemed to be some interest in FM among some vendors of hardware wallets.)

Overall, it is hard to formally compare the TCBs of paper-based voting systems and cryptographic end-to-end verifiable voting, but the latter seems promising to me, especially in the current political climate, and I think it is worthy of a serious consideration.