Formal Specification and Verification of a Secure Micropayment Protocol
As online businesses keep growing and web services become pervasive, there is an increasing demand for micro-payment protocols that facilitate micro-commerce, namely selling content and services for small amounts of money (possibly less than one cent per transaction), which cannot be handled efficiently by credit cards due to substantial per transaction fee and delay. In this paper, the authors investigate the security of micropayment protocols that support low-value transactions. They focus on one type of such protocols that are based on hash chains. They present a formal specification of a typical hash chain based micropayment protocol using abstract protocol notation, and discuss how an adversary can attack this protocol using message loss, modification, and replay.