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 micropayment 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 micropayment 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 mint 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 micropayment protocols as well.

• Type: Journal
• Year: 2008
• Where: IJNSEC
• Authors: Mohamed G. Gouda, Alex X. Liu
• Keywords: Abstract Protocol Notation, Hash Chain, IJNSEC 2008, Micropayment Protocols