TLS1.3&TLS1.2形式化分析(二)

 一、下面是TLS1.2和TLS1.3握手协议过程 ,明显的能够看出存在不一样 。算法

 咱们先说TLS1.2的握手过程明显是比TLS1.3的握手过多了一次。在TLS1.3中舍弃了以前RSA的协商过程,而后基于ECDH算法优化了整个过程,下面说明 ECDH算法的含义:安全

 固然TLS1.3不光光是优化了者一点,在链接恢复过程当中TLS1.3作到了 0-RTT 的过程。   服务器

  在TLS1.2中原有的大量的特性被删除,包括下面的特性:并发

     RSA秘钥传输--------不支持向前安全函数

     RSA密钥传输——不支持前向安全性
     CBC模式密码——易受BEAST和Lucky 13攻击
     RC4流密码——在HTTPS中使用并不安全
     SHA-1哈希函数——建议以SHA-2取而代之
     任意Diffie-Hellman组——CVE-2016-0701漏洞
     输出密码——易受FREAK和LogJam攻击
同时 TLS 1.3版本还存在工做方式的修改:工具

     新的密码套件仅在TLS1.3下支持, 一些旧的密码套件再也不支持。与 TLS1.2相比  TLS1.3加密了更多的握手,减小额握手延迟并采用AEAD 方案,TLS1.3新的握手模式包括初始化的1-RTT (EC)DHE,(预共享秘钥)PSK模式和PSK-DHE模式。优化

     新的密码套件定Tamarin 义方式不一样,而且没有详细规定证书类型(RSA、DSA、ECDSA)或者秘钥交换机制,(如DHE、或者ECHDE),这对密码套件的配置会存在影响。在TLS1.3中客户端提供的key_sahre会对“组”配置产生影响。另外在新的版本中再也不使用DSA证书。编码

二、做者对TSL1.3的形式化安全分析和证实(使用的是Tamarin  工具)加密

    根据做者官网上的披露的信息,原做者并无使用 Scyther工具对 TLS1.3作形式化分析,而是使用了Tamarin  这个工具 (功能更增强大,适用于高级分析)能够自动分析安全协议的工具。对象

    做者使用的TLS1.3第十版本的协议做为研究的对象。那me做者的主要贡献是经过扩展修订版10的模型合并所需客户端的延迟机制,发现了一种潜在的攻击,其中攻击者可以在PSK回复握手期间成功的模仿客户端,做者由此强调了客户签名内容中包含更多信息的严格的必要性。在以后的发布的TLS1.3草案中更新了这部分。其中重要的一点就是做者说能够将10 版本的草案的模型进行扩展到之后的版本模型。这将是长期的。

      Tramarin-proved工具的多字节重写很是适合用于对TLS1.3协议规范所暗示的复杂转换系统进行建模,能够容许分析无线数量的并发的TLS会话的交互。

      做者使用本工具进行分析额时候,首先第一步是构造TLS握手和记录协议的抽象。而后将其编码成 Tramarin的规则(也就是使用SPDL语言进行描述形式化协议的一个过程)。规则捕获忠诚的党和对手行为,在合法的客户端和服务端下,构建的模型规则一般适用于各个消息传输相关联的全部动做,例如咱们的第一个客户端规则捕获客户端生成并发送所必要参数做为(EC)DHE握手的第一次飞行的一部分,以及在本客户端中跟踪,此规则能够在下面的C_1能够看见这种机制,该图表示客户端在不一样执行中具备全部选项的并集。(下图是TLS1.3草案10版本的部分客户端状态机制的模型分析)

接下来做者证实TLS1.3(第十版)中声明的目标和安全属性

        分析的第二步涉及将所须要的安全属性编码为 Termarin  lemmas.TLS握手协议的目标是容许通讯方的单方或者可选方的相互实体认证,以创建能够将本身置于链接中间的窃听者和攻击者不可用的共享秘钥。TLS记录协议旨在提供应用程序数据的机密性和完整性,所以,咱们将定义编码下面属性做为引理:

       单方面认证服务器,

       相互认证(可选)

       会话秘钥和秘钥的机密性和完善性和完善性的向前保密性。

       握手消息的向前保密性。

相关文章
相关标签/搜索