From Dolev-Yao to Strong Adaptive Corruption: Analyzing Security in the Presence of Compromising Adversaries
METADATA ONLY
Author / Producer
Date
2009
Publication Type
Report
ETH Bibliography
yes
Citations
Altmetric
METADATA ONLY
Data
Rights / License
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. Our semantics can be used as a basis for protocol analysis tools. As an example, we extend an existing symbolic protocol-verification tool with our adversary models. The result is the first tool that systematically supports notions such as weak perfect forward secrecy, key compromise impersonation, and adversaries capable of so-called strong corruptions and state-reveal queries. As further applications, we use our model hierarchy to relate different adversarial notions, gaining new insights on their relative strengths, and we use our tool to find new attacks on protocols.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
2009 (79)
Pages / Article No.
Publisher
International Association for Cryptologic Research
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
03634 - Basin, David / Basin, David
Notes
Received 12 February 2009, Last revised 9 November 2009.