The Security of Ping-Pong Protocols

Jon Kleinberg, IBM Almaden Research Center
Tuesday Dec 3,1996, 4:15pm, Gates 104

Abstract

Although the verification of cryptographic protocols remains a fundamentally murky area, there has been some success in identifying restricted domains in which one can give formal proofs of security. One of the first lines of work in this direction was by Dolev and Yao, who proposed a model for multi-user ``ping-pong protocols,'' and formalized a notion of security in terms of an underlying set of possible attacks. Their framework helped to serve as the foundation of a number of subsequent approaches, including Meadows's NRL Protocol Analyzer. We'll discuss the Dolev-Yao model and some of this subsequent work, as well as some of the complications that arise when making precise a notion of ``security'' in this way.