International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

From Dolev-Yao to Strong Adaptive Corruption: Analyzing Security in the Presence of Compromising Adversaries

Authors:
David Basin
Cas J.F. Cremers
Download:
URL: http://eprint.iacr.org/2009/079
Search ePrint
Search Google
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. We also use our semantics as a basis to extend an existing symbolic protocol-verification tool with our adversary models. This tool is the first 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 our tool find new attacks on protocols.
BibTeX
@misc{eprint-2009-18261,
  title={From Dolev-Yao to Strong Adaptive Corruption: Analyzing Security in the Presence of Compromising Adversaries},
  booktitle={IACR Eprint archive},
  keywords={foundations / adversary models, state-reveal, perfect forward secrecy, key compromise impersonation, tools},
  url={http://eprint.iacr.org/2009/079},
  note={ cas.cremers@inf.ethz.ch 14301 received 12 Feb 2009, last revised 26 Feb 2009},
  author={David Basin and Cas J.F. Cremers},
  year=2009
}