Automated Verification of Game-Theoretic Security Properties for Decentralized Protocols

I aim to develop an automated framework to formally prove off-chain protocols, a certain type of blockchain protocols secure from a game-theoretical perspective. Thereby, I ensure that honest blockchain users cannot be harmed and that rational users behave honestly.

Hence, the goal of my research is to find security risks in existing protocols, or prove their absence respectively. Using only “secure” protocols, honest users have a guarantee that even in the presence of rational or Byzantine adversaries their assets will not be compromised. Further, rational adversaries are guaranteed to act honestly, as this is the behavior that yields the highest pay-off. Justice and the protection of honest beings are very important to me and I therefore aim to support the development of candid technology.

In my research I plan to define security in terms of game theory, employ the SMT solver Z3 to automatically reason about the model and derive security results about blockchain technology.