A Formal Model of Bitcoin Transactions