Computer Sciences Dept.

Computer Security and Cryptography Reading Group

View the proposed reading list on the following page, or send your paper suggestions to Matt Fredrikson (mfredrik).

Date & Location Reading
Thursday, Oct 8, 2009
4:30 PM - 5:30 PM
5331 CS
Cynthia Sturton, Susmit Jha, David Wagner and Sanjit Seshia
On Voting Machine Design for Verification and Testability

Download paper

We present an approach for the design and analysis of an electronic voting machine based on a novel combination of formal verification and systematic testing. The system was designed specifically to enable verification and testing. In our architecture, the voting machine is a finite-state transducer that implements the bare essentials required for an election. We formally specify how each component of the machine is intended to work and formally verify that a Verilog implementation of our design meets this specification. However, it is more challenging to verify that the composition of these components will behave as a voter would expect, because formalizing human expectations is difficult. We show how systematic testing can be used to address this issue, and in particular to verify that the machine will behave correctly on election day.

Thursday, Oct 29, 2009
4:30 PM - 5:30 PM
3310 CS
Roxana Geambasu, Tadayoshi Kohno, Amit A. Levy, and Henry M. Levy
Vanish: Increasing Data Privacy with Self-Destructing Data

Download Paper

Today's technical and legal landscape presents formidable challenges to personal data privacy. First, our increasing reliance on Web services causes personal data to be cached, copied, and archived by third parties, often without our knowledge or control. Second, the disclosure of private data has become commonplace due to carelessness, theft, or legal actions. Our research seeks to protect the privacy of past, archived data -- such as copies of emails maintained by an email provider -- against accidental, malicious, and legal attacks. Specifically, we wish to ensure that all copies of certain data become unreadable after a user-specified time, without any specific action on the part of a user, and even if an attacker obtains both a cached copy of that data and the user's cryptographic keys and passwords. This paper presents Vanish, a system that meets this challenge through a novel integration of cryptographic techniques with global-scale, P2P, distributed hash tables (DHTs). We implemented a proof-of-concept Vanish prototype to use both the million-plus-node Vuze Bit- Torrent DHT and the restricted-membership OpenDHT. We evaluate experimentally and analytically the functionality, security, and performance properties of Vanish, demonstrating that it is practical to use and meets the privacy-preserving goals described above. We also describe two applications that we prototyped on Vanish: a Firefox plugin for Gmail and other Web sites and a Vanishing File application.

Note: An independent group of researchers have published an attack on this system. Their writeup can be found here.

   2002: Jan. Feb. Mar. Apr. May June July Aug. Sep. Oct. Nov. Dev.
   2003: Jan. Feb. Mar. Apr. May June July Aug. Sep. Oct. Nov. Dec.
   2004: Jan. Feb. Mar. Apr. May June July Aug. Sep. Oct. Nov. Dec.
   2005: Jan. Feb. Mar. Apr. May June July Aug. Sep. Oct. Nov. Dec.
   2006: Jan. Feb. Mar. Apr. May June July Aug. Sep.

< Back to the Sec & Crypto main page

Created by Mihai Christodorescu (
Created: Wed Aug 13 10:30:10 CDT 2003
Last modified by Matt Fredrikson
Last modified: Thu Oct 1 2009
Computer Science | UW Home