Formale und kryptographische Analyse von Protokollen mit spieltheoretischen Sicherheitsanforderungen
Final Report Abstract
The goal of our project was to develop models and methods for the rigorous formal and cryptographic analysis of protocols with game-theoretic security requirements, with contract-signing protocols being an important example of such protocols. Our work involved the formalization of such requirements and the development of methods and tools for the rigorous analysis of protocols with such requirements. An important game-theoretic security requirement, which was formalized as part of our project for the first time, is on-line abuse-freeness. Intuitively, this property requires that, even if one of the protocol participants may be able to determine the outcome of the protocol, e.g., whether or not a contract is signed, he/she is not able to demonstrate this to an external party, even though the external party can interact with the protocol participant during the whole protocol execution. This property involves complex reasoning about strategies and knowledge of agents. Our case studies, in which we applied our definition to prominent contract-signing protocols, revealed unexpected results, including a subtle attack on one of the studied protocols. Motivated by the problem of contract signing, we developed a general definition of accountability. Intuitively, accountability means that misbehaving parties, i.e., parties who deviated from the prescribed protocol, can be detected, and hence, blamed for their misbehavior by, for instance, a judge. Our definition turned out to be widely applicable: besides contract signing, we applied it to e-voting and auction protocols, for which we found partly severe problems and weaknesses. We also established relationships between accountability and verifiability. Finally, our project opened the door to the fully automated analysis of game-theoretic security requirements. More specifically, we implemented a constraint-based algorithm for checking game-theoretic security requirements and successfully applied it to non-trivial protocols, including the prominent ASW contract-signing protocols. We also obtained first results on the tool-supported analysis of the mentioned accountability property.
Publications
- A Formal Definition of Online Abuse-freeness. Proceedings of the 6th International ICST Conference on Security and Privacy in Communication Networks (SecureComm 2010), Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, vol. 50, Springer, 2010, pp. 484–497
Ralf Küsters, Henning Schnoor, and Tomasz Truderung
- Accountability: Definition and Relationship to Verifiability. Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS 2010), ACM, 2010, pp. 526–535
Ralf Küsters, Tomasz Truderung, and Andreas Vogt
- Implementing a Constraint Solving Algorithm for Checking Game-Theoretic Security Requirements. Tech. report, University of Trier, 2011
Ralf Küsters, Thomas Schmidt, and Tomasz Truderung
