Paolo Modesti

Paolo Modesti, Siamak F. Shahandashti, Patrick McCorry et al.

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.

Paolo Modesti, Leo Freitas, Qudus Shotomiwa et al.

The Second Payment Services Directive (PSD2) of the European Union aims to create a consumer-friendly financial market by mandating secure and standardised data sharing between banking operators and third parties. Consequently, EU countries and the United Kingdom have adopted Open Banking, a standardised data-sharing API. This paper presents a formal modelling and security analysis of the UK Open Banking Standard's APIs, with a specific focus on the Account and Transaction API protocol. Our methodology employs the extended Alice and Bob notation (AnBx) to create a formal model of the protocol, which is then verified using the OFMC symbolic model checker and the Proverif cryptographic protocol verifier. We extend previous work by enabling verification for unlimited sessions with a strongly typed model. Additionally, we integrate our formal analysis with practical security testing of some necessary conditions to demonstrate verified security-goals in the NatWest Open Banking sandbox, evaluating mechanisms such as authorisation and authentication procedures.