SSH Security, TCP Leaks, and Not-so-AccuVotes: Computer Security from Proofs to People

Computer security research is a broad field, with research efforts ranging from the design and analysis of low-level cryptographic building blocks to the design and analysis of complex and socially important systems. My research illustrates how weak links and important issues often arise at the boundaries between different but relatively well-studied sub-areas. I provide three examples. My first example focuses on how results about authenticated encryption in standard cryptographic models lift to real systems. I show that although the popular Secure Shell (SSH) protocol uses the Encrypt-and-MAC method, which cryptographers have shown to be generically insecure, within SSH it is not only secure but provably so. In contrast I show that although recent versions of the popular WinZip application use the Encrypt-then-MAC method, which cryptographers have proven to be secure, within WinZip it is actually insecure. I emphasize that these results are not due to any weakness in the theory, but rather call for the the need to be careful when applying theoretical results to real systems. My second example shows that one cannot ascertain the security of a system by studying that system's software in isolation, but must rather study the complete system (software and hardware) as a whole. Specifically, I describe a new privacy issue with the TCP protocol that only arises once one considers the interaction between a device's TCP software implementation and the device's underlying hardware. For my third example, I describe my discovery of attacks against the Diebold AccuVote-TS electronic voting machines. I then describe some social and technical implications of my results.