Upcoming paper: A formal model of Bitcoin transactions