Formal Modelling and Security Analysis of Bitcoin's Payment Protocol
Authors:
Paolo Modesti,
Siamak F. Shahandashti,
Patrick McCorry,
Feng Hao
Abstract:
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 addr…
▽ More
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.
△ Less
Submitted 15 March, 2021;
originally announced March 2021.
Security Analysis of the Open Banking Account and Transaction API Protocol
Authors:
Abdulaziz Almehrej,
Leo Freitas,
Paolo Modesti
Abstract:
To counteract the lack of competition and innovation in the financial services industry, the EU has issued the Second Payment Services Directive (PSD2) encouraging account servicing payment service providers to share data. The UK, similarly to other European countries, has promoted a standard API for data sharing:~the Open Banking Standard. We present a formal security analysis of its APIs, focusi…
▽ More
To counteract the lack of competition and innovation in the financial services industry, the EU has issued the Second Payment Services Directive (PSD2) encouraging account servicing payment service providers to share data. The UK, similarly to other European countries, has promoted a standard API for data sharing:~the Open Banking Standard. We present a formal security analysis of its APIs, focusing on the correctness of the Account and Transaction API protocol. The work relies on a previously proposed methodology, which provided a practical approach to protocol modelling and verification.
△ Less
Submitted 28 March, 2020;
originally announced March 2020.
