NetBill [5, 21] is designed to support very low-cost transactions involving electronic goods. One central and distinguished claim of the NetBill protocol is that it satisfies goods atomicity, and this will be the focus of our analysis. In NetBill, all money-related activities are centralized at the bank and take the form of transfers between accounts; consequently, arguing money atomicity is straightforward.
Here, we use an abstracted and simplified version of the protocol that captures atomicity properties. For full details on the protocol see [5, 22].