Who is stepping out of line here?

If she offers her hand first, it may be shaken slightly. Whoever is addressed by her may address her. The procedure of a meeting with Queen Elizabeth II is strictly regulated by court protocol. Anyone who does not adhere to it will attract unpleasant attention. It is no different with crypto protocols. Who is allowed to do what and when is precisely regulated here. The parties involved here can be, for example, web browsers and web pages that communicate with each other. CISPA researcher and research group leader Robert Künnemann wants to establish so-called accountability as a security property in protocols. In other words, he wants to ensure that parties can be held accountable if they deviate from the protocol and thus endanger IT security. The tool Tamarin, which he co-developed, can also be used to automatically analyze existing crypto protocols for their ability to guarantee accountability. He presented work on this in his paper "Automated Verification of Accountability in Security Protocols," for which he received a Distinguished Paper Award at the 2019 Computer Security Foundations Symposium. Since then, he has been working to further expand the tool's applications.

What accountability means in information security is difficult to capture in one term. "Often accountability is equated with an obligation to assume accountability. But it's actually about the ability to be held accountable," Künnemann explains. In other words, it's about being able to prove protocol parties' responsibility for their actions - at least when it becomes a security issue.

Until now, the security of many cryptographic protocols has been based on trust in outside third parties, Künnemann explains. Hacks of certification authorities, for example, of which there have been several in the past, show how problematic this can be. These few authorized bodies vouch for the identity of websites, people, and devices. They issue digital certificates and sign public keys, making them central to the Internet's security infrastructure. If these organizations issue false certificates, attackers can lure users' browsers to phishing sites, for example, and steal personal data. 

Tracing false certificates back to the issuing organization is comparatively easy. "In many other cases, however, it is very tedious or even impossible to find all parties that have deviated from the protocol. But this is precisely what the previous definition of accountability presupposed," Künnemann explains. Since such verifiability would require nothing less than total surveillance, which is neither possible nor desirable on the Internet, Künnemann has come up with a new definition of the property and what it is supposed to achieve. "The important thing is not to determine whether the protocol was followed word for word, but whether the protocol goal was violated, for example, an unauthorized transaction took place. That a protocol provides the necessary information to be able to track down the causes of such violations is called accountability."

The question of the principle of cause and effect led the researcher far back into the history of philosophy. "One of the first attempts to define when something is the cause of something else can be found in the antique work of Hippocrates. Ther, it was about the cause of a disease," Künnemann explains. Even more important for the 36-year-old, however, is the work of the Scottish philosopher David Hume, who had a decisive influence on the modern concept of causality in the 18th century. He was also the first to introduce the counterfactual, a kind of "what if" idea, into the analysis of causal relationships. This idea was further developed in the 1970s by the U.S. philosopher David Lewis. According to his definition, to be considered a cause - in simplified terms - it must make a difference to what would have happened if it did not exist. "An example would be: Had Diego Maradona not used his hand to help in 1986, the goal to make it 1-0 would not have been scored in that minute," Künnemann explains. Causality theory, developed by philosopher and computer scientist Judea Pearl only in the past few decades, provides the researcher with a graphical modeling approach for causal relationships. "To develop my accountability approach, I used these ideas in a simplified form."

So, in order to check whether the right protocol parties are always accused, Künnemann's approach considers scenarios in which only the accused protocol parties are allowed to step out of line. Is a violation even still possible with these? If not, the protocol overlooks causers. Are violations also possible if fewer parties step out of line, but the same "course of action" is followed? If so, the protocol may blame bystanders. "We are committed to finding all causers and not blaming non-causers." So, true to Humes, any counterfactual - that is, the hypothetical "lining up" of an accused - must result in the protocol running error-free. "Being able to reliably identify and substantiate misconduct can increase public confidence in third parties. At the same time, those involved can better respond to errors." For such analysis to be possible, security protocols must exhibit certain characteristics. The Tamarin tool can automatically determine whether they do.

The fact that so much has happened in the research field of causality over the past few decades fascinates the Cottbus native, who has been a research group leader at CISPA since 2019. "It excites me that I live in a time when there's been so much progress on the age-old question: 'What is causality?'"

translated by Oliver Schedler