Formal Specification and Verification of a Secure Micropayment Protocol

10.6633/IJNS.200807.7(1).10

Mohamed G. Gouda；Alex X. Liu

Information security ； micropayment protocols ； network security

International Journal of Network Security

7卷1期（2008 / 07 / 01）

81 - 87

英文

As online businesses keep growing and Web services become pervasive, there is an increasing demand for micro-payment protocols that facilitate microcommerce, 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, we investigate the security of micro-payment protocols that support low-value transactions. We focus on one type of such protocols that are based on hash chains. We present a formal specification of a typical hash chain based micro-payment protocol using Abstract Protocol notation, and discuss how an adversary can attack this protocol using message loss, modification, and replay. We use convergence theory to show that this protocol is secure against these attacks. The specification and verification techniques used in this paper can be applied to other micro-payment protocols as well.