Iliano Cervesato
MSR, a framework for specifying security protocols and
investigating their meta-theory
Many design flaws and incorrect analyses of cryptographic protocols
can be traced to inadequate specification languages for message
components, environment assumptions, and goals. In this talk, we
present MSR, a strongly typed specification framework for security
protocols, which is intended to address the first two issues. Its
typing infrastructure, based on the theory of dependent types with
subsorting, yields elegant and precise formalizations, and supports a
useful array of static checks that include type-checking and access
control validation. It uses multiset rewriting rules over first-order
atomic formulas to express protocol actions and relies on a form of
existential quantification to symbolically model the generation of
nonces and other fresh data. The availability of memory predicates
enables it to faithfully encode systems consisting of a collection of
coordinated subprotocols, and constraints allow tackling objects
belonging to complex interpretation domains, e.g. time stamps, in an
abstract and modular way. Any adversary to a protocol can be
specified directly within MSR. In particular, this allows formally
stating and proving a conjecture underlying the successes of nearly
all current security protocol verfication tool, namely that the
standard Dolev-Yao intruder model can indeed emulate the actions of an
arbitrary attacker. We also show how the specification of the
Dolev-Yao intruder can be derived from the typing and access control
rules pertinent to a given protocol.
Host: Frank Pfenning
POP Seminar
February 2, 2001
3:30 p.m.
Wean Hall 8220