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