Kent Leeding

The Blockchain approach to Distributed Ledger Technology aims for a decentralised approach to the writing of information onto a digital Ledger, an append-only sequence of blocks. Different blockchain protocols provide a variety of mechanisms for achieving consensus on selecting the agent to add the next block. Consensus is important to ensure agreement across the different agents maintaining their own record of the state of the blockchain and updates on it. Proof-of-stake protocols use the amount of `stake' agents hold in the blockchain to determine who should produce the next block, so that agents with greater commitment produce more of the blocks. This is a technology where the practice sometimes runs ahead of the theory: a number of implementations have been developed, however the protocols are complex and not always underpinned by analysis. This chapter explores an approach to formal modelling of such protocols using the PRISM model-checker, and their analysis with respect to some fairness properties expected of proof-of-stake protocols, also captured within PRISM, and in the presence of particular attacks on fairness. The approach is exemplified on the Peercoin protocol where the analysis reveals some vulnerabilities.