© 2002 by British Computer Society
Formal Methods for Assuring Security of Protocols
1 Center for Systems Assurance, Electrical Engineering and Computer Science, Syracuse University, Syracuse, NY 13244, USA Email: sueo@ecs.syr.edu
Establishing the security of a system is an intricate problem with subtle nuances: it requires a careful examination of the underlying assumptions, abstractions, and possible actions. Consequently, assuring that a system behaves securely is virtually impossible without the use of rigorous analytical techniques. In this article, we focus on a single cryptographic protocol (NeedhamSchroeder) and show how several different formal methods can be used to identify its various vulnerabilities. These vulnerabilities include susceptibility to freshness attacks and impersonations.