The Security of Ping-Pong Protocols
Jon Kleinberg, IBM Almaden Research Center
Tuesday Dec 3,1996, 4:15pm, Gates 104
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
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.