Analyzing the Security of Electronic Voting Systems: Can Formal Methods Really Help?

In this chapter, first the authors discuss the current trends in the usage of formal techniques in the development of e-voting systems. They then present their experiences on their usage to specify and verify the behaviors of one of the currently deployed e-voting systems, using formal techniques and verification against a subset of critical security properties that the system should meet. The authors also specify attacks that have been shown to successfully compromise the system. The attack information is used to extend the original specification of the system and derive what the authors call the extended model. This work is a step towards fostering open specification and the (partial) verification of a voting machine. The specification and verification was intended as a learning process where formal techniques were used to improve the current development of e-voting systems.