0HAL Id: tel-014699370https://theses.hal.science/tel-014699370提交日期：2017年3月16日0HAL是一个多学科开放获取档案，用于存储和传播科学研究文档，无论是否发表。这些文档可以来自法国或国外的教育和研究机构，或者来自公共或私人研究中心。0HAL多学科开放获取档案，用于存储和传播研究水平的科学文献，无论是否发表，来自法国或国外的教育和研究机构，公共或私人实验室。0关于Web身份验证协议的安全性0Antoine Delignat-Lavaud0引用此版本：0Antoine Delignat-Lavaud. 关于Web身份验证协议的安全性. 密码学与安全性[cs.CR]. 巴黎科学与文学大学,2016. 英文. �NNT: 2016PSLEE018�. �tel-01469937�0巴黎高等师范学校0博士学院：ED386：巴黎中心数学科学0大学部门：Inria巴黎-罗昆库尔0论文作者：Antoine Delignat-Lavaud0为了从巴黎高等师范学校获得博士学位0学术领域：计算机科学0专业：安全性0关于身份验证的安全性0Web的协议0论文指导：Karthikeyan Bhargavan0巴黎高等师范学校0博士学院：ED386：巴黎中心数学科学0大学部门：Inria巴黎-罗昆库尔0论文作者：Antoine Delignat-Lavaud0为了从巴黎高等师范学校获得博士学位0学术领域：计算机科学0专业：安全性0关于身份验证的安全性0Web的协议0论文指导：Karthikeyan Bhargavan0巴黎高等师范学校0博士学院：ED386：巴黎中心数学科学0研究单位：Inria巴黎-罗昆库尔0论文作者：Antoine Delignat-Lavaud0为了获得巴黎高等师范学校博士学位0学科：计算机科学0专业：安全性0协议的安全性0Web上的身份验证0论文指导：Karthikeyan Bhargavan0巴黎高等师范学校不赞同也不审查论文中作者的观点：这些观点应被视为作者自己的观点。0关键词：Web安全，身份验证，协议分析，http，传输层安全，tls，javascript，同源策略，x.509，公钥基础设施，单点登录，协议组合，通道绑定，三次握手0关键词：Web安全，身份验证，协议分析，http，传输层安全，tls，javascript，同源策略，x.509，公钥基础设施，单点登录，委托身份验证，组合安全性，通道绑定，复合身份验证，三次握手0本论文是在以下机构准备的0Inria巴黎-罗昆库尔 B.P. 105Prosecco团队 Voluceau领地 -Rocquencourt 78153 Le Chesnay法国0电话：+33 (0)1 39 63 55 11传真：+33 (0)1 39 63 53 30网站：http://www.inria.fr0摘要 xiii0关于Web身份验证协议的安全性0摘要0是否可以证明在某些假设下，访问Web服务（如GMail）用户的机密数据需要知道其密码，而不会限制到实际可能的攻击？Web协议的特殊因素使得无法直接应用现有的来自密码协议分析领域的方法和工具。首先，Web上的攻击者能力远远超出了仅仅操纵客户端和服务器之间在网络上交换的消息。例如，用户在连接到其电子邮件时可能在浏览器中打开一个由对手控制的选项卡（例如，通过广告横幅）；这个选项卡像任何其他网站一样，可以向GMail服务器发送任意请求，尽管浏览器的页面隔离策略阻止了对这些请求的响应的直接读取。此外，连接到GMail的过程涉及复杂的协议堆叠：首先，使用TLS协议建立加密通道，并对服务器进行身份验证；然后，使用cookie创建HTTP会话；最后，浏览器执行客户端返回的JavaScript代码，该代码负责向用户请求密码。最后，即使假设该系统的设计是安全的，只需一个微小的编程错误（例如，一个简单的错误的goto语句）就足以破坏整个系统的安全性。本论文的目标是构建一套工具和库，以组合方式编程和形式化分析Web应用程序的安全性，以应对Web上攻击者当前能力的合理模型。为此，我们研究了Web基础设施的各个层面（TLS，X.509，HTTP，HTML，JavaScript）上使用的各种协议的设计，并评估了它们的组合。我们还研究了当前的实现，并开发了一些经过验证的新版本进行测试。我们发现了协议和实现中的许多漏洞，并提出了一些经过正式验证的对策，其中一些已经在浏览器、服务器和网站上实施。最后，这些发现对当前和未来的TLS协议版本产生了影响。0关键词：Web安全，身份验证，协议分析，HTTP，传输层安全，TLS，JavaScript，同源策略，X.509，公钥基础设施，单点登录，协议组合，信道绑定，三次握手0Inria Paris-Rocquencourt B.P. 105 Team Prosecco – Domaine de Voluceau - Rocquencourt –78153 Le Chesnay – France0xiv 摘要0Web上的身份验证协议的安全性0摘要0随着越来越多的私人用户数据存储在网络上，确保对这些数据的适当保护变得越来越关键（特别是当数据通过不可信任的网络传输，或者用户通过浏览器访问时）。然而，为了正式证明例如，只有知道用户的密码才能访问GMail的电子邮件，假设攻击者不能做一些合理的假设（例如，他不能破解AES加密），必须准确理解许多复杂协议和标准（包括DNS，TLS，X.509，HTTP，HTML，JavaScript）的安全属性，更重要的是，完整的Web堆栈的组合安全目标。除了这个组合安全挑战之外，还必须考虑到Web特有的强大的附加攻击者能力，除了通常的网络消息篡改。例如，用户可能在一个选项卡中浏览恶意页面，同时保持活动的GMail会话；这个页面允许使用JavaScript触发任意的隐式认证请求到GMail（即使浏览器的隔离策略可能阻止它读取响应）。攻击者还可以将自己注入到诚实的页面中（例如，作为恶意广告脚本，或者利用数据消毒漏洞），让用户点击恶意链接，或者尝试冒充其他页面。除了攻击者，协议和应用程序本身比协议分析文献中的典型示例要复杂得多。登录GMail已经需要在（至少）三个主体之间进行多个TLS会话和HTTP请求，代表数十个原子消息。因此，临时模型和手写证明无法扩展到Web协议的复杂性，必须使用先进的验证自动化和建模工具。最后，即使假设GMail的设计确实安全防御此类攻击者，任何一个编程错误都可能完全破坏整个系统的安全性。因此，除了根据规范对协议进行建模外，还需要评估实现以实现实际安全性。本论文的目标是开发新的工具和方法，作为广泛的组合Web安全分析框架的基础，该框架可用于根据Web上攻击者能力的合理广泛模型来实现和正式验证应用程序。为此，我们研究Web协议在各个层次（TLS，HTTP，HTML，JavaScript）的设计，并使用广泛的形式化方法进行组合评估，包括符号协议模型，类型系统，模型提取和基于类型的程序验证。我们还分析当前的实现并开发一些新的经过验证的版本进行测试。我们发现了协议和实现中的广泛漏洞，并提出了一些经过正式验证的对策，其中一些已经在浏览器和各种网站上实施。例如，我们发现的三次握手攻击需要协议修复（RFC7627），并影响了TLS协议的新版本1.3的设计。0关键词：网络安全，身份验证，协议分析，http，传输层安全，tls，javascript，同源策略，x.509，公钥基础设施，单点登录，委托身份验证，组合安全，通道绑定，复合身份验证，三次握手0致谢0这项工作在很大程度上要归功于Karthik对Web安全的雄心勃勃和独创性的愿景，他将其视为密码学、类型系统、编译器、进程演算或自动逻辑求解器（以及其他许多）等多样研究主题的交汇点，再加上大量的实践实验和老派黑客技术。几乎所有在这篇论文中呈现的结果都是通过与一系列令人惊叹的研究人员进行某种程度的合作获得的，他们都应该得到我的感激之情，并且应该因他们对本文的重要贡献而获得应有的赞誉。尽管这些合作的具体细节将出现在论文的相关部分中，但我想集体感谢所有的合著者Martin、Andrew、Chetan、Benjamin、Karthik、Cédric、Chantal、Nadim、Markulf、Sergio、Ilya、Alfredo、Pierre-Yves、Nikhil、Ted、Yinglian和Jean-Karim，感谢他们在我们的共同项目上所付出的所有时间和努力。其中，我特别感谢Sergio在我在伦敦帝国理工学院的各个逗留期间对我进行的接待；感谢Martin、Ted、Ilya和Yinglian在（原）微软研究硅谷实验室担任实习生期间对我的接待；最后，感谢Cédric在微软剑桥研究实验室担任实习生期间对我的接待。我与各个海外学术和工业研究团队的逗留最终对我的职业生涯选择产生了重大影响，我希望鼓励任何一位博士生，如果他们认为在本节中有任何可以学到的东西，那么他们应该寻找类似的机会。总的来说，我在Inria的整个博士学习经历非常精彩，我将对与我的同事Bruno、Graham、Cătălin、Alfredo、Ben、Santiago、Iro、Robert、Miriam以及来自世界各地的无数访问者在巴黎实验室相遇的时光保持美好的回忆。特别感谢我的办公室同事和同学Romain、David、Jean-Karim和Nadim，尽管我有些奇怪的习惯，但我们相处得很好（尽管公平地说，我相信我自己也成功地忍受了他们一些自己奇怪的习惯）。最后，我要真诚地感谢论文委员会成员们慷慨地接受了审查这篇论文的繁琐任务。随机被分配一个额外的截止日期肯定是非常不愉快的，我希望将来能够弥补给您带来的不便。0xv0致谢 xvixvii0目录0摘要 xiii0致谢 xv0目录 xvii0表格目录 xxiii0图表目录 xxv0介绍 10I 应用安全 110介绍和动机 13 典型的Web攻击向量... 13 相关出版物... 1501 WebSpi：Web建模框架 17 1.1 WebSpi库... 17 1.1.1 ProVerif... 17 1.1.2 WebSpi... 20 1.1.3从ProVerif结果到具体的Web攻击... 29 1.2 案例研究：单点登录和社交分享... 32 1.2.1非正式的安全目标... 33 1.2.2 基于Web的攻击... 33 1.2.3 社交CSRF攻击... 34 1.2.4 攻击放大... 35 1.2.5OAuth 2.0的WebSpi模型... 35 1.2.6 ProVerif分析结果... 44 1.2.7 针对OAuth 2.0的社交CSRF攻击... 481.2.8 针对OAuth 2.0的令牌窃取攻击... 50 1.2.9 讨论... 51 1.2.10 其他功能和协议流程... 52 1.2.11超越OAuth... 53 1.3 案例研究：主机安全应用... 54 1.3.1 Web上的应用级密码学... 57xviiiSommaire1.3.2Encrypted Web Storage Applications . . . . . . . . . . . . . . . . . . . . .581.3.3Attacks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .631.3.4WebSpi Extensions. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .711.3.5Application: ConfiChair . . . . . . . . . . . . . . . . . . . . . . . . . . . .721.3.6Application: SpiderOak. . . . . . . . . . . . . . . . . . . . . . . . . . . .761.3.7Application: 1Password. . . . . . . . . . . . . . . . . . . . . . . . . . . .771.3.8Concrete Attacks on Encrypted Web Storage Services . . . . . . . . . . . .792DJS: Language-based Sub-Origin Isolation of JavaScript812.1Attacks on Web Security Components . . . . . . . . . . . . . . . . . . . . . . . . .852.1.1Login with Facebook Component . . . . . . . . . . . . . . . . . . . . . . .872.1.2Client-side Decryption for Cloud Data . . . . . . . . . . . . . . . . . . . .902.1.3Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .902.2DJS: Defensive JavaScript . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .912.2.1Defensiveness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .912.2.2DJS Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .942.2.3Type System . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .952.2.4Formal defensiveness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .982.2.5Type safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .982.2.6Proof of Defensiveness . . . . . . . . . . . . . . . . . . . . . . . . . . . . .992.3DJS Analysis Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1062.3.1Conformance Checker. . . . . . . . . . . . . . . . . . . . . . . . . . . . .1062.4Defensive Libraries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1072.4.1Defensive JavaScript Crypto Library. . . . . . . . . . . . . . . . . . . . .1072.4.2Defensive JSON and JOSE . . . . . . . . . . . . . . . . . . . . . . . . . . .1082.5WebSpi Model Extraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1082.5.1Translating Client-Side JavaScript . . . . . . . . . . . . . . . . . . . . . . .1092.5.2Syntax of Target PHP Subset . . . . . . . . . . . . . . . . . . . . . . . . . .1112.5.3Translating PHP into ProVerif . . . . . . . . . . . . . . . . . . . . . . . . .1122.5.4Limitations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1132.6Applications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1162.6.1Secret-Keeping Bookmarklets . . . . . . . . . . . . . . . . . . . . . . . . .1162.6.2Script-level Token Access Control . . . . . . . . . . . . . . . . . . . . . . .1172.6.3An API for Client-side Encryption. . . . . . . . . . . . . . . . . . . . . .1192.7Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .120Related Work123Web Authorization Protocols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .123Host-proof Applications. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .123Formal Models of Web Browsing . . . . . . . . . . . . . . . . . . . . . . . . . . . .123Formal Analysis of Web Authorization . . . . . . . . . . . . . . . . . . . . . . . .125JavaScript . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .126Conclusions from Part I129SommairexixIITransport Layer Security131Introduction133TLS Protocol: Connections, Sessions, Epochs . . . . . . . . . . . . . . . . . . . . . . . .135Full Handshake. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .135The Record Protocol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .137Session Resumption . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .137Renegotiation: Changing Epochs. . . . . . . . . . . . . . . . . . . . . . . . . . .138Client Authentication . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .139Implementations and APIs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .139Related Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1403State Machine Attacks against TLS1413.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1413.2The TLS State Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1453.3Testing Implementations with FlexTLS . . . . . . . . . . . . . . . . . . . . . . . .1493.3.1FlexTLS Design and API . . . . . . . . . . . . . . . . . . . . . . . . . . . .1493.3.2FlexTLS Applications. . . . . . . . . . . . . . . . . . . . . . . . . . . . .1523.3.3TLS 1.3: Rapid prototyping of new protocol versions . . . . . . . . . . . .1583.4State Machine Flaws in TLS Implementations . . . . . . . . . . . . . . . . . . . .1593.4.1Implementation Bugs in OpenSSL. . . . . . . . . . . . . . . . . . . . . .1593.4.2Implementation Bugs in JSSE . . . . . . . . . . . . . . . . . . . . . . . . .1613.4.3Implementation bugs in other implementations . . . . . . . . . . . . . . .1633.5Attacks on TLS Implementations. . . . . . . . . . . . . . . . . . . . . . . . . . .1663.5.1Early Finished: Server Impersonation (Java,CyaSSL). . . . . . . . . . . .1663.5.2Skip Verify: Client Impersonation (Mono, CyaSSL, OpenSSL) . . . . . . .1673.5.3Skip ServerKeyExchange: Forward Secrecy Rollback (NSS, OpenSSL). .1683.5.4Inject ServerKeyExchange: FREAK . . . . . . . . . . . . . . . . . . . . . .1693.5.5Summary and Responsible Disclosure. . . . . . . . . . . . . . . . . . . .1703.6A Verified State Machine for OpenSSL. . . . . . . . . . . . . . . . . . . . . . . .1713.7Towards Security Theorems for OpenSSL . . . . . . . . . . . . . . . . . . . . . . .1773.7.1Modeling multi-ciphersuite security . . . . . . . . . . . . . . . . . . . . .1783.8Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1803.9Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1814Compound Authentication and Channel Binding1834.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1834.2Formal Protocol Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1884.2.1Threat Model. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1894.2.2Security Goals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1894.2.3Compound Authentication Protocol Examples. . . . . . . . . . . . . . .1904.3Case study: Triple Handshake Attacks on TLS . . . . . . . . . . . . . . . . . . . .1994.3.1A Man-In-The-Middle TLS Proxy Server . . . . . . . . . . . . . . . . . . .1994.3.2Exploit against HTTPS Client Authentication . . . . . . . . . . . . . . . .2074.3.3Variations using other authenticaton protocols. . . . . . . . . . . . . . .2134.3.4Breaking TLS Channel Bindings . . . . . . . . . . . . . . . . . . . . . . . .2154.3.5Breaking Channel-Bound Tokens on the Web . . . . . . . . . . . . . . . .2174.4Generic Channel Synchronization Attacks . . . . . . . . . . . . . . . . . . . . . .2184.4.1Key Synchronization via Small Subgroup Confinement. . . . . . . . . .219
我的内容管理
展开
