Modeling and analyzing security in the presence of compromising adversaries

Abstract. We present a framework for modeling adversaries in secu-rity protocol analysis, ranging 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 sym-bolic settings. We extend an existing symbolic protocol-verification tool with our 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. In case studies, we automatically find new attacks and rediscover known attacks that previously required detailed manual analysis.