Formal Verification of Anti-Cheating Protocols in Cryptoeconomic Systems
note: This repository, the models and associated paper aer a work in progress and have not been reviewed.
This repository contains a number of models written for use with the PRISM model checker assessing the game-theoretic effectiveness of proposed mechanisms to deter cheating during trading in cryptoeconomic systems.
The repository is centered around a technical report which explores three such systems:
- Discreet Log Contracts
- Double-spending Prevention for Bitcoin zero-confirmation transactions
- Bisq 1.2