Abstract:


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


David Basin and Cas Cremers



We present a symbolic framework, based on a modular 
operational semantics, for formalizing di erent 
notions of compromise relevant for the analysis of 
cryptographic protocols. The framework's rules can 
be combined in di erent ways to specify di erent 
adversary capabilities, capturing di erent 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 rst 
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 classi es the relative strength of 
protocols against di erent forms of compromise. In case 
studies, we use Scyther to automatically construct 
protocol-security hierarchies that re ne and correct 
relationships between protocols previously reported in 
the cryptographic literature.