26/02/2010, 16:15 — 17:15 — Room P3.10, Mathematics Building
Cas Cremers, ETH Zurich
Modeling and Analyzing Security in the Presence of Compromising
Adversaries
We present a framework for modeling adversaries in security
protocol analysis, in which we define a hierarchy of adversary
models. These models range from a Dolev-Yao style adversary to more
powerful adversaries who can reveal different parts of principals'
states during protocol execution. Our adversary models unify and
generalize many existing security notions from both the
computational and symbolic settings and lead to new, previously
unexplored security notions. We extend an existing symbolic
protocol-verification tool with our adversary models. This is the
first tool that systematically supports notions such as weak
perfect forward secrecy, key compromise impersonation, and
adversaries capable of state-reveal queries. In extensive case
studies, we automatically find new attacks and rediscover known
attacks that previously required detailed manual analysis. Joint
work with David Basin.
