OpenID 金融级 API 的广泛形式化安全分析
摘要
在监管和行业需求的驱动下，全球银行正致力于通过基于Web的API向其客户的网上银行账户开放给第三方服务。通过使用这些所谓的开放银行API，第三方公司（如FinTechs）能够读取其用户银行账户的信息并发起支付。该领域最有前景的标准之一是OpenID金融级API（FAPI），目前由OpenID基金会以开放流程开发，并得到大型行业合作伙伴的支持。FAPI是OAuth 2.0的一个面向高风险场景且旨在抵御极强攻击者的配置文件。为达到此安全水平，FAPI采用了一系列为加固OAuth 2.0而开发的机制。在本文中，我们基于Fett、Kuesters和Schmitz提出的Web基础设施模型（WIM），对FAPI的安全性进行严谨、系统的形式化分析。为此，我们首先在WIM中建立FAPI的精确模型，包括不同的配置文件和安全特性组合。然后我们利用FAPI模型精确定义核心安全属性。在尝试证明这些属性时，我们发现了部分严重的攻击，破坏了认证、授权和会话完整性属性。我们针对这些攻击开发了缓解措施，并最终能够形式化证明修复版FAPI的安全性。该分析对FAPI的开发是一项重要贡献，因为它有助于定义精确的安全属性和攻击者模型，并避免严重的安全风险。作为独立关注点，我们还揭示了上述用于加固OAuth 2.0的安全机制中的弱点。我们说明这些机制未必能实现其设计所针对的安全属性。
引用
@article{arxiv.1901.11520,
title = {An Extensive Formal Security Analysis of the OpenID Financial-grade API},
author = {Daniel Fett and Pedram Hosseyni and Ralf Kuesters},
journal= {arXiv preprint arXiv:1901.11520},
year = {2019}
}
备注
An abridged version appears in Security and Privacy 2019. Parts of this work extend the web model presented in arXiv:1411.7210, arXiv:1403.1866, arXiv:1508.01719, arXiv:1601.01229, and arXiv:1704.08539