Date Added: Jun 2010
The authors present a symbolic framework, based on a modular operational semantics, for formalizing different notions of compromise relevant for the analysis of cryptographic protocols. The framework's rules can be combined in different ways to specify different adversary capabilities, capturing different practically-relevant notions of key and state compromise. They have extended an existing security-protocol analysis tool, Scyther, with their adversary models. This is the first tool that systematically supports notions such as weak perfect forward secrecy, key compromise impersonation, and adversaries capable of state-reveal queries.