论文标题
开放银行帐户和交易API协议的安全分析
Security Analysis of the Open Banking Account and Transaction API Protocol
论文作者
论文摘要
欧盟的第二支付服务指令（PSD2）旨在通过强制执行银行运营商和第三方之间的安全和标准化数据共享来创建一个对消费者友好的金融市场。因此，欧盟国家和英国采用了公开银行，这是一种标准化的数据共享API。本文对英国开放银行标准的API进行了正式的建模和安全分析，特别关注帐户和交易API协议。我们的方法采用扩展的爱丽丝和鲍勃符号（ANBX）来创建协议的形式模型，然后使用OFMC符号模型检查器和proverif加密协议验证器进行验证。我们通过使用强大的模型启用验证无限的会话来扩展以前的工作。此外，我们将正式分析与对某些必要条件的实际安全测试集成在一起，以在NATWest开放银行沙箱中证明经过验证的安全目标，评估诸如授权和身份验证程序之类的机制。
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.
