Modeling and Analyzing Security in the Presence of Compromising Adversaries

Download Now Date Added: Jun 2010
Format: PDF

The authors present a framework for modeling adversaries in 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. Their adversary models unify and generalize many existing security notions from both the computational and symbolic settings. They extend an existing symbolic protocol-verification tool with their adversary models, resulting in the first tool that systematically supports notions such as weak perfect forward secrecy, key compromise impersonation, and adversaries capable of state-reveal queries.