Anja Petković Komel: CheckMate – an automated framework for proving security of off-chain protocols

Abstract: One of major concerns about using Blockchain protocols is their security. Indeed, a lot of active research is being done to prove protocols secure. An important class of Blockchain protocols are the so called off-chain protocols for which security frameworks are mostly dealing with uderlying crypotgraphic procedure and not so much how to respond to potential attacks of adversary users.

I will present the ongoing work on analysing security off-chain protocols from a game-theoretic perspective, specifically the recent developments in automating proofs of security of said protocols. Our automated framework, currently named CheckMate, uses SMT solvers to yield strategies to defend against malicious behaviour and thus proves (and also disproves) off-chain protocols safe to use. We will briefly look into how SMT solvers work and we will inspect what kind of formulas CheckMate feeds them to obtain the proofs.

This is joint work with Lea Brugger, Laura Kovács, Sophie Rain and Michael Rawson.