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.
翻译:《支付协议》标准BIP70具体规定了Bitcoin的付款如何由商人和客户进行,得到了最大的付款处理人和最广泛使用的钱包的支持。协议表明,由于缺乏退款地址的认证,很容易受到退款袭击。在本文件中,我们给出了协议的第一个正式模式,并将退款涉及协议的安全目标,即退款地址认证和保密正式化。正式模式利用通信渠道作为抽象信息传递协议模型,传递协议范本和核查人可以依赖的安全目标。我们分析了支付协议,确认它很容易受到违反退款地址认证安全目标的袭击。此外,我们提出了一项具体的协议修订提案,支持商人获得可公开核查的证据,以减轻袭击。我们核实经修订的协议符合退款地址确定的安全目标,即退款地址认证和保密。因此,我们证明修订后的协议不仅对现有的袭击有保障,而且对违反正式安全目标的任何进一步袭击都有保障。