Modeling Bitcoin protocols with probabilistic logic programming

Bitcoin is one of the first decentralized, peer to peer, payment systems based on the so-called Proof-of-Work (PoW). PoW is an algorithm that requires the computation of a hard function in order to gain access to a resource but, at the same time, the correctness of the computed result should be easily checked. The use of a PoW removes the necessity of a centralized third party and so the consistency of the network may be altered directly by the involved users. Peers, to solve the PoW more efficiently, usually organize themselves into mining pools, to increase the overall computational power: this situation, unfortunately, leads to a network centralization. In this paper we consider two typical scenarios of a Bitcoin network and we model them by probabilistic logic programming (PLP): the centralization of the hashing power by large pools and the “double spending attack”. In the first one, we verify the effectiveness of a protocol that attempts to discourage the formation of large pools. In the second one, we compute the probability of success of an attacker. Both scenarios are modeled using the PLP package cplint.