CTL
10 février 2009 - 15h30
From Dolev-Yao to Strong Adaptive Corruption: Analyzing Security in the Presence of Compromising Adversaries
par Cas Cremers de ETH Zurich
Abstract: We formalize a hierarchy of adversary models for security protocol analysis, ranging from a Dolev-Yao style adversary to more powerful adversaries who can reveal different parts of principals' states during protocol execution. We define our hierarchy by a modular operational semantics describing adversarial capabilities. We use this to formalize various, practically-relevant notions of key and state compromise. The semantics provide a basis for protocol analysis and we extend an existing symbolic protocol-verification tool, Scyther, to reason about security properties of protocols in the presence of adversaries in our hierarchy. Our tool is the first automated tool that supports notions such as weak perfect forward secrecy, key compromise impersonation, and adversaries capable of so-called strong corruptions and state-reveal queries. As applications, we use our model hierarchy to relate different adversarial notions, gaining new insights on their relative strengths, and we use Scyther find new attacks on protocols that were previously reported to be secure.
joint work with David Basin
