Paul Valiant
CS259
"An Electronic Voting Protocol (revisited)"

In this project, my purpose was to understand an electronic voting
protocol and determine its properties with the aid of Murphi.

The protocol was not ideal for analysis because the paper left many
important aspects of it unspecified. The paper in which the protocol is
described is less than three pages long; in this space, it attempts to
motivate, formulate, and verify a fairly lengthy protocol. In order to
understand the protocol, I had to look through several related papers.
One particularly vague thing was the blinded signature.

After unraveling the protocol, I reduced it step by step to a simpler
protocol that was conceptually straightforward, within Murphi's modelling
limits, and verifiably equivalent. I put some heuristic explanations of
these steps on my slides. However, due to the 20 minute time limit of the
presentation, I did not put much detail. Since then, I have gone back and
rigorously justified most of the steps in the derivation (see the slides).

It is interesting to note that the protocol I derived is essentially
compatible with the protocol the other group modelled. Thus the other
group correctly guessed which terms could be removed, and implemented a
Murphi model accordingly. 

[Note: Part of the reason I devoted a significant portion of my talk to
explaining the protocol was that the other group did not. To me, a Murphi
model is meaningless unless it explicitly comes from a protocol.
Anecdotally, it would appear that most of the flaws people found in the
protocols presented in class were found in this modelling stage. I'm
slightly surprised that no one else attempted to justify this largest
conceptual step. It would appear that the purpose of automated analysis
is to eradicate such large leaps of faith.]

For the automated analysis I extended the code used by the first group in
a number of ways. 

First, there were some conceptual errors in their code. For example, even
the dishonest CA insisted that everyone was a registered voter. However,
they allowed voters to forge their voter certificate, so these two issues
almost cancelled each other out. The problem remains, however, that if
you can forge a voting certificate and have the cooperation of the three
authorities, you can dupe the whole country.

I also extended their code to consider the case when the voters (as
opposed to the authorities) tried to verify the election. This is an
important issue in the paper, that even if some agents dupe the
authorities, the election is still recoverable. I also added several new
abilities to the various agents. For example, a dishonest voter shouldn't
need to steal someone's registration certificate for a dishonest CA to
certify him.