Tigran Antonyan, Seda Davtyan, Sotiris Kentros, Aggelos Kiayias, Laurent Michel, Nicolas Nicolaou, Alexander Russell and Alexander Shvartsman
In Proceedings of the 2009 USENIX/ACCURATE Electronic Voting Workshop (EVT 09)
August 10–14, 2009, Montreal, Canada www.usenix.org/events/evtwote09/

Abstract

In the interest of auditing election procedures, certain electronic voting technologies provide monitoring capabilities that record select actions undertaken by election officials before, during, and after an election process, as well as the conditions present in an electronic voting terminal as the result of its interactions with its environment. In this paper we report on an automated auditing process for detecting procedural irregularities for elections employing the AccuVote Optical Scan (AV-OS) terminal (manufactured by Premier Election Systems). Our auditing process is derived from an abstract finite state model of the AV-OS; this determines, in particular, a correspondence between state transitions and logged events that separates expected and “irregular” histories. Automating the detection of these irregular histories has permitted us to provide detailed election procedure audits for full-scale Connecticut elections. We conclude the article with a discussion of the result of the event log analysis performed within the post-election audit of the November 2008 elections in Connecticut. Additionally, we identify a defect and some deficiencies in the AV-OS event logging subsystem that can interfere with the event log transcript making it vulnerable to manipulation and discuss the effects of these deficiencies. This research is funded by the Office of the Secretary of the State of Connecticut.

Download full paper: evt09.pdf