Jon Millen

Constraint Solving for Protocol Analysis
Sp-231 on 5 August, 2004 from 1500-1550
(download slides)

The constraint solver is a fast, easily-used Prolog program for formal cryptographic protocol analysis. Authentication and key distribution protocols are specified in a strand space style. Constraint solving always terminates when the number of legitimate parties is bounded, even when other parameters such as attacker activity and constructed message depth are not. Confidentiality and authentication goals can be tested. The constraint solver enumerates possible legitimate event orderings and for each one generates a set of term closure constraints, for which solution existence is decidable and a solution yields an attack.

About Jon Millen
Jonathan K. Millen is a Senior Computer Scientist at SRI International. His areas of interest are information security, authentication protocol analysis using formal methods, public key infrastructure, and survivability modeling. Before 1997 he worked at the MITRE Corporation, and supported the National Computer Security Center's Trusted Product Evaluation Program. His doctorate in Mathematics is from Rensselaer Polytechnic Institute in 1969. Dr. Millen is Co-Editor-in-Chief of the Journal of Computer Security, a member of the editorial board of the ACM Transactions on 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.