In the course of my PhD studies, I worked on the game-theoretic security of blockchain protocols.
That means, I developed 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.
We implemented the above framework as 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.
I am currently contributing to a project called Act. Act
is a specification language for Ethereum Smart Contracts, which is agnostic of the used programming language.
Using Act as a backend, we aim to connect CheckMate and Act into one pipeline.
Currently, to verify a Smart Contract's incentives (a.k.a. game-theoretic security), the user has to semi-manually
model the contract as a game (see our paper on Game Modeling).
Applying Act's capabilities, we plan to automatically generate a Smart Contract's game model from its Act specification,
thereby making game-theoretic security accessible to the community.
Sophie Rain
