In my PhD I work on the game-theoretic security of Blockchain protocols . That means, I am developing a framework to mathematically prove the game-theoretic aspects of protocols secure. When studying the security of Blockchain protocols, often only cryptographic properties are considered, while the game-theoretic ones are overlooked. In the high-level example of online banking a cryptographic security property would be that a password cannot be accessed by unauthorized users. A game-theoretic one on the other hand is that no one wants to share their password with others.

The security properties we are interested in are incentive-compatibility and Byzantine-fault-tolerance . Together they ensure that no party, irrespective of their goals, has a reason to deviate from the protocol.

As the mentioned security properties are defined based on game theory, our framework requires the analyzed protocol to be modeled as a game in a first step. In a collaboration with the Ethereum Foundation we are currently working on automating this process for protocols specified entirely as Smart Contracts.

We further developed CheckMate, our open source tool to automatically verify the game-theoretic security of protocols modeled as games. More details on this can be found in the CheckMate section.

CheckMate is our automated game-theoretic security reasoning tool. It takes an extensive form game model of a protocol as input and decides its game-theoretic security. Additionally, among other features, if a game model was not secure, CheckMate can provide counterexamples and weakest precondtitions, that if added as preconditions, make the game model secure. If the analyzed game model was secure, CheckMate can present a witness behavior. The tool is available here. Be aware that CheckMate is constantly evolving, the latest stable version is tagged "lpar25".

As part of my NetIdee stipend, I regularly write blog articles about my research for a broad audience.