Abstract

In circulation since 2009, Bitcoin is a well-known cryptocurrency.  Bitcoin's popularity is a result of its capability to eliminate the need for a trusted third party such as a broker or a bank to process payments. 

The aim of this project is to develop a model of the Bitcoin model in the Modest language http://www.modestchecker.net/ This model should capture the evolution of the blockchain, including the frequency and timing of forks. The model should come with a testing framework that allows evaluation of the model against real data about the evolution from the blockchain.  The project builds on earlier models in Uppaal of the Bitcoin model.

A prerequisite for this project is knowledge of an affinity to use tools to collect publically available data and make it available for further analysis. Experience with formal modelling tools would be considered an advantage.

REFERENCES

1. Ron, Dorit and Shamir, Adi. Quantitative Analysis of the Full Bitcoin Transaction Graph (Digital version available here)
2. A. Fehnker and K. Chaudhary, Twenty Percent and a Few Days - Optimising a Bitcoin Majority Attack NFM, 2018 (Digital version available here)
3. Dennis Eijkel. Analysing the Use of Selfish Mining Among Bitcoin Miners and Mining Pools (Digital version available here)