Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries

Abstract. We 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. We have extended an existing security-protocol analysis tool, Scyther, with our 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. We also introduce the concept of a protocol-security hierarchy, which classifies the relative strength of protocols against different forms of compromise. In case studies, we use Scyther to automatically construct protocol-security hierarchies that refine and correct relationships between protocols previously reported in the cryptographic literature.

• Type: Conference
• Year: 2010
• Where: CSL
• Authors: David A. Basin, Cas J. F. Cremers
• Keywords: Automated Reasoning, Compromise Relevant, CSL 2010, Key Compromise Impersonation, State Compromise