利用表达性 Web 模型分析具有主身份提供者的 BrowserID 单点登录系统
密码学与安全
2019-01-31 v2
摘要
BrowserID 是 Mozilla 最近开发的一种复杂的、现实世界的 Web 应用程序单点登录 (SSO) 系统。它采用了新的 HTML5 特性（如 Web 消息传递和 Web 存储）以及加密断言来提供去中心化登录，旨在尊重用户隐私。它可以在主身份提供者和次身份提供者模式下运行。在主模式下，BrowserID 可与任意身份提供者 (IdP) 一起运行；而在次模式下，仅有一个 IdP，即 Mozilla 的默认 IdP。我们最近提出了一种表达性的 Web 基础设施通用模型，并基于该 Web 模型分析了 BrowserID 次 IdP 模式的安全性。分析揭示了几处严重漏洞。在本文中，我们通过分析更为复杂的 BrowserID 主 IdP 模式来补充我们先前的工作。我们不仅像以前一样研究认证属性，还研究隐私属性。在分析过程中，我们发现了不适用于次模式的新颖且实用的攻击：一种违反 SSO 系统核心认证属性的身份注入攻击，以及破坏 BrowserID 重要隐私承诺且似乎不经重大系统重新设计就无法修复的攻击。我们的一些针对隐私的攻击利用了一种迄今为止未受到太多关注的浏览器侧信道。对于认证漏洞，我们提出了一种修复方案，并在我们通用 Web 模型的轻微扩展中形式化地证明了修复后的系统满足我们所考虑的所有要求。这构成了迄今为止基于表达性 Web 基础设施模型对 Web 应用程序进行的最复杂的形式化分析。作为另一项贡献，我们在扩展的 Web 模型中识别并证明了通用 Web 特性的重要安全属性，以促进未来对 Web 标准和 Web 应用程序的分析工作。
引用
@article{arxiv.1411.7210,
title = {Analyzing the BrowserID SSO System with Primary Identity Providers Using an Expressive Model of the Web},
author = {Daniel Fett and Ralf Kuesters and Guido Schmitz},
journal= {arXiv preprint arXiv:1411.7210},
year = {2019}
}
备注
arXiv admin note: substantial text overlap with arXiv:1403.1866