A Formal Analysis of the Bitcoin Protocol