Syverson (Ph.D. in philosophy (logic) from Indiana University) has been with the U.S. Naval Research Laboratory since 1989. His current focus is on the design and analysis of protocols and systems for anonymity and accountability. He is program chair of the 2000 IEEE Computer Security Foundations Workshop and program chair of the 2001 International Financial Cryptography Conference.

These lectures will survey some of the work in the logical analysis of security protocols over the last decade. Beginning with BAN logic in the late eighties, we will discuss belief and knowledge logics---and also temporal logics, primarily as they have been used to examine authenticated key distribution protocols. We will also touch on other protocol goals---which are often needed for e-commerce, such as accountability, anonymity, and fair exchange. We will describe the syntax and semantics of these logics and the use of both in protocol analysis. We will discuss their relation to some other formal methods for protocol analysis.