Thursday, February 20, 1:30PM
Lieb 3rd floor Conference Room
Abstract
The Dolev-Yao model of security protocol analysis may be formalized
using a notation based on multiset rewriting with existential
quantification. In this setting protocol execution is carried out
symbolically as a form of rewriting. Basic assumptions of this
formalization, perfect cryptography coupled with nondeterministic
computation on the part of the adversary, provide an idealized setting
in which protocol analysis becomes relatively tractable and detects
common protocol errors. This lecture describes the multiset rewriting
approach to security protocol analysis, algorithmic upper and lower
bounds on specific forms of protocol analysis, and some of the ways
this model is useful for formalizing subtle properties of the Kerberos
5 authentication protocol and other protocols.