Constraint Solving for Protocol Analysis

Speaker: Dr. Jonathan Millen, MITRE Corporation
Abstract: The constraint solver is a fast, easily used Prolog program for formal analysis of the security of authentication and cryptographic key distribution protocols. Cryptographic operations are represented by abstract operations, and the capabilities of an attacker to analyze and modify messages are represented by simple rules. Protocols are specified in a strand space style. Constraint solving separates event ordering enumeration from the algebraic solution term closure constraints. This method always terminates when the number of legitimate parties is bounded, even when other parameters such as attacker activity and constructed message depth are not.
Biography: Jonathan Millen is a Senior Principal at the MITRE Corporation, where he just returned after seven years at SRI International. His areas of interest are information security, authentication protocol analysis, public key infrastructure, and dependability modeling. Dr. Millen is Co-Editor-in-Chief of the Journal of Computer Security, Associate Editor of the ACM Transactions of Information and System Security, and he is the founder and steering committee chair of the IEEE Computer Security Foundations Workshop. He is Vice Chair of the IEEE Computer Society Technical Committee on Security and Privacy.
Presented On: Friday, February 4, 2005
Videotape: Click to View the Streaming Quicktime Presentation

This presentation requires the free Apple QuickTime Player which can be downloaded from the following link:

www.apple.com/quicktime/download