Check out the new USENIX Web site.
USENIX, The Advanced Computing Systems Association

15th USENIX Security Symposium Abstract

Pp. 321–336 of the Proceedings

Designing Voting Machines for Verification

Naveen Sastry, University of California, Berkeley; Tadayoshi Kohno, University of California, San Diego; David Wagner, University of California, Berkeley


We provide techniques to help vendors, independent testing agencies, and others verify critical security properties in direct recording electronic (DRE) voting machines. We rely on specific hardware functionality, isolation, and architectural decision to allow one to easily verify these critical security properties; we believe our techniques will help us verify other properties as well. Verification of these security properties is one step towards a fully verified voting machine, and helps the public gain con- fidence in a critical tool for democracy. We present a voting system design and discuss our experience building a prototype implementation based on the design in Java and C.
  • View the full text of this paper in HTML and PDF. Listen to the presentation and Q & A in MP3 format.
    Click here if you have forgotten your password Until August 2007, you will need your USENIX membership identification in order to access the full papers. The Proceedings are published as a collective work, © 2006 by the USENIX Association. All Rights Reserved. Rights to individual papers remain with the author or the author's employer. Permission is granted for the noncommercial reproduction of the complete work for educational or research purposes. USENIX acknowledges all trademarks within this paper.
To become a USENIX member, please see our Membership Information.

Last changed: 20 Sept. 2006 ch