  The Payment Protocol standard BIP70, specifying how payments in Bitcoin are
performed by merchants and customers, is supported by the largest payment
processors and most widely-used wallets. The protocol has been shown to be
vulnerable to refund attacks due to lack of authentication of the refund
addresses. In this paper, we give the first formal model of the protocol and
formalise the refund address security goals for the protocol, namely refund
address authentication and secrecy. The formal model utilises communication
channels as abstractions conveying security goals on which the protocol
modeller and verifier can rely. We analyse the Payment Protocol confirming that
it is vulnerable to an attack violating the refund address authentication
security goal. Moreover, we present a concrete protocol revision proposal
supporting the merchant with publicly verifiable evidence that can mitigate the
attack. We verify that the revised protocol meets the security goals defined
for the refund address. Hence, we demonstrate that the revised protocol is
secure, not only against the existing attacks, but also against any further
attacks violating the formalised security goals.
