For this project, we decided to look at Internet Voting Protocols. The
only paper we could find that focused on its protocol instead of novel
cryptographic functions was "An Anonymous Electronic Voting Protocol for
Voting Over the Internet" by Indrajit Ray, Indrakshi Ray, and Natarajan
Narasimhamurthi of the University of Michigan-Dearborn. They described a
protocol for voting over the internet using pre-existing cryptographic
primatives, but the protocol was not very clearly specified, and several
of the parts were left unjustified. The properties we decided to focus on
for this protocol were that if fraud were to occur, it could be easily
proved, and if no fraud were to occur, it would not be possible for
someone to prove that it did.

Much of the protocol was straightforward and easy to program into
Murphi. As with the previous models we've looked at, we modeled things
like encryption, signed hashes, and voter marks using the corresponding
agent id of the sender/receiver. The interesting part of this protocol is
that rather than trying to prove that secrets are not divulged or that we
are talking with who we think we are, we have to assume instead that
everybody knows who they're talking to, but they can't trust
anybody. Essentially the entities who are distributing, collecting, and
counting ballots might be colluding to defraud the voter of their vote or
cast additional votes. In this case, rather than preventing the fraud in
the first place, the voter needs to be able to prove that it occurred.

We chose not to model and prove that the identity of the voter is kept
secret, since that seems to depend much more on the cryptosystem and the
effectiveness of the blinding in teh blinded signature submission.

In several places, we felt that the protocol was ambiguous or
under-specified, and we made an effort to give the designers the benefit
of the doubt when making decisions about what certain things meant. For
example, we decided that the one-way permutation used to turn the serial
number into an untraceable voter mark was a keyed hash function because
otherwise anybody who knew all of the serial numbers could use the serial
numbers to reconstruct all of the voter marks.

We decided to remove the FTP server from our model, as we decided that at
least within the confines of the model, it added nothing to the
protocol. The paper does not really talk about the FTP server or justify
why it should be in the protocol, but we have guessed that maybe it is
used to obfusicate the origin of a cast vote. This seems like a pretty
weak security measure, though, and they may want to think of using some
sort of anonymous routing instead if this were their intent.

In order to model intruders and collusion between the entities, we created
a bunch of "bad" voters who are people not registered to vote. Essentially
these could be actual people, or they could be fake entities created by
some combination of the BD, CA, and VC. Because all 3 essentially share
information and allow bad voters to vote, we feel that this method of
modeling them is adequate to encompass the range of possible attacks on
this protocol.

The first invariant we tried to prove was that if a voter's vote had not
been counted, they could prove that fraud had occurred. This is a simple
invariant, and within the confines of our model, it holds. While modeling
this, though, it occurred to us that with the necessary conditions stated
in the paper for proving fraud, it may be possible for a voter to prove
fraud when fraud did not occur. Our model confirmed that this was true. If
a voter registers, recieves a ballot, and gets it certified, but does not
vote, they can claim fraud by publishing their voter mark and the proper
signatures of the BD and CA.

While giving our presentation, Vitaly suggested that maybe a receipt from
the VC could be used to demonstrate that not only was the voter certified
to vote but that they actually cast a ballot. After our presentation, we
went back and re-read the paper closely. We realized that there was such a
receipt, but it was left undiscussed in the paper, and we had abstracted
it away in our model when removing the FTP server.

Because of this, we modified our model to reflect the existence of this
receipt and we changed the invariant so that a voter needed such a
receipt, as well as the signatures of the  BD and CA, to prove fraud. With
the addition of the this receipt, a voter cannot prove non-existant fraud
any more in our model.

Lastly, we wrote an invariant to confirm the attack on the protocol which
is already stated in the paper. The attack occurs when someone registers
to vote and gets certified but does not cast a ballot. In this case, the
CA, BD, and VC can collude to cast a ballot in their stead. It is
possible, if every single voter were to give up their annonymity and
publish their signed salted voter marks, that this fraud could be
proven. But first, if a number of voters equal to or greater than the
number of fraudulent votes refuse to give up their annonymity, the fraud
cannot be proven. Sencondly, and more importantly, there is no indication
that this fraud may have occurred until all of the voters have revealed
their secret voter marks. Thus, this fraud is only detectable and provable
if the vote is not longer an annonymous one.


While trying to model the protocol, we realized how under-specified it
was. This led us to find a possible bug in the protocol which may not
really have been a bug, but due to lack of solid specification, we can't
quite tell. We also ran into some problems trying to use Murphi to
demonstrate the correctness of the annonymity scheme. We feel that this is
one case where some sort of proof techniques would be a better way to
model and verify this protocol. Unlike authentication, where you are
trying to prove whether or not something can occur, for this protocol we
must assume that it can and then try to prove that the information a
certain party has is enough to show that it occurred.