网络基础设施的表达性模型：定义及其在BrowserID单点登录系统中的应用

网络构成了一个复杂的基础设施，众多攻击表明，对标准和网络应用进行严格分析不可或缺。受先前成功工作的启发，特别是Akhawe等人以及Bansal等人的工作，本文提出了一个网络基础设施的形式化模型。与旨在自动分析的先前工作不同，我们的模型目前尚不能直接自动化，但在标准和规范方面更为全面和准确。因此，它可以作为分析广泛标准和应用的坚实基础。作为案例研究以及我们工作的另一个重要贡献，我们使用该模型对BrowserID系统（又称Mozilla Persona）进行了首次严格分析，这是一个最近开发的复杂真实世界单点登录系统，采用了AJAX、跨文档消息传递和HTML5网络存储等技术。我们的分析揭示了多个非常关键的缺陷，这些缺陷在先前模型中无法被捕获。我们提出了缺陷修复方案，正式陈述了相关安全属性，并证明了在具有所谓二级身份提供者的设置中，修复后的系统在我们的模型中满足这些安全属性。最关键的缺陷修复已被Mozilla采纳，我们的发现获得了Mozilla安全漏洞奖励计划的奖励。