Formal specification and verification of a micropayment protocol

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 micropayment 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