Abstract:


Modeling and Analyzing Security in the Presence 
of Compromising Adversaries


David Basin and Cas Cremers



We present a framework for modeling adversaries in 
security protocolanalysis, ranging from a Dolev-Yao 
style adversary to more powerfuladversaries who can 
reveal different parts of principals' states during 
protocol execution. Our adversary models unify and 
generalize manyexisting security notions from both 
the computational and symbolicsettings.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 attacksthat previously required 
detailed manual 
analysis.