TLS1.3&TLS1.2形式化分析

时间  2019-12-11 标签 tls1.3&tls1.2 tls 形式化 分析

本博客是对下面博客链接上的原文进行梳理+本身在其余方面资料作个整理html

https://blog.csdn.net/andylau00j/article/details/79269499
https://www.cnblogs.com/huanxiyun/articles/6554085.html
   TLS协议在网络的应用层提供功能 ：加密，认证、消息完整性。（创建一个安全的链接，对其中传输的数据加密保护，防止中间人嗅探明文；多对数据的完整性进行校验，防止传输的数据被中间人进行篡改，创建一个可信的链接，对双方的真实身份进行验证）
        

  一个正常的TLS1.3 握手顺序是按照下面的顺序进行：ios

  • 客户端发送Client Hello（CH）报文，包含有关密钥协商以及其余与TLS链接创建有关的扩展给服务端。
  • 服务端发送Server Hello（SH）报文，包含有关密钥协商的扩展返还给客户端，双方根据CH和SH的协商结果能够得出密钥材料。
  • 若是客户端发送的CH报文不知足服务端的须要（如：不包含服务端支持的DH组件），服务端会发送一个Hello Retry Request报文给客户端，要求客户端从新发送符合要求的CH报文。
  • 利用密钥材料和前两个报文的哈希值，使用HKDF能够计算出一个handshake_key，此后握手阶段的信息受该密钥保护。
  • 服务端发送Encypted Extension（EE）报文，包含其余与密钥协商无关的扩展数据给客户端。
  • 若是使用公钥证书进行身份认证，服务端发送Certificate报文（传递本身的证书信息），和Certificate Verify(CV)报文（使用本身的证书私钥对以前的报文进行HMAC签名证实本身持有该证书）给客户端。
  • 若是须要对客户端身份进行认证，服务端还须要发送Certificate Request（CR）报文给对方请求客户端发送证书。
  • 服务端发送Finished报文。代表服务端到客户端信道的握手阶段结束，理论上不得再由该信道发送任何握手报文。
  • 若是客户端收到了服务端的CR报文，返回本身的Certificate报文和CV报文。
  • 客户端发送Finished报文，代表握手阶段结束，能够正式开始会话通信。Finished报文使用会话密钥对上述全部握手信息进行HMAC签名，校验签名能够检验握手阶段的完整性，也能够验证双方是否协商出了一致的密钥。

TLS1.3最大的特色就是对不一样的报文使用多种不一样的秘钥，TLS1.2中只使用两种秘钥，一个事用于完整性校验，另外一个是用于报文加密，同一个链接中不一样方向的加密秘钥不同，TLS1.3使用AEAD机制再也不使用MAC_key来进行完整性校验，同时因为其余各类用途的加密须要，TLS1.3的实施过程使用一下几种key：算法

    handshake_key     early_traffic_key   resumption_key     exporter_key（导出秘钥，用户自定义的其余用途）安全

  这些秘钥都是由以前协商的秘钥材料计算而出，区别在于HKDF的计算次数不一样，HKDF计算使用的哈希值不一样，以会话秘钥application_key为例子，以整个握手阶段的报文做为输入，计算四次HKDF导出最终使用的秘钥，同时，当加密的报文长度达到必定的长度的时候，双方发送的KU报文从新计算application_key服务器

数据发送出去以后，recod层会在密报文头部加上一小段的明文信息来标识解密后明文的长度信息，对方的让recod 层收到消息以后，经过逆过程解密密文后转发给上层协议，网络

同时TLS1.3协议版本容许在末尾添加八字节整数倍的全为0的二进制数据，对方收到该消息以后，解密从末尾开始去掉0 ，当搜索到第一个不全为0的八字节的时候结束。session

总的归纳：  TLS1.3协议版本 使用的更加 复杂额秘钥导出过程，加强了最终使用秘钥的安全性，同时简化了所使用的加密秘钥，删除了RC4  3DES   SHA1  AES-CBC 等加密算法，删除了加密前压缩，从新协商等具备的漏洞，精简了协议 内容，并发

    在TLS1.2中记录协议record，占据一个TLS链接的绝大数的数据流量，app

Record 协议 — 从应用层接受数据，而且作:

分片，逆向是重组
生成序列号，为每一个数据块生成惟一编号，防止被重放或被重排序
压缩，可选步骤，使用握手协议协商出的压缩算法作压缩
加密，使用握手协议协商出来的key作加密/解密
算HMAC，对数据计算HMAC，而且验证收到的数据包的HMAC正确性
发给tcp/ip，把数据发送给 TCP/IP 作传输(或其它ipc机制)。

 下面对TLS协议秘钥协商的过程的分析  dom

基于RSA握手和秘钥交换的客户端验证服务器为示例以下

 

下面是上网的握手过程的时序图

下面对上面的协商过程解释：

 （1）Client-Hello   客户端发送请求，以明文传输信息，包含版本信息，加密候选列表，候选算法列表，随机数，扩展字段等信息，

        客户端支持加密套件 cipher suite列表，注意，每个加密条件对应前面TLS原理中的四个功能的组合，认证算法Au（身份验证），秘钥交换算法 （keyExchange 秘钥协商），对称加密算法Enc(信息加密)，信息摘要MAc（完整性验证）。在TLS1.2 中支持压缩算法，Client-Hello 中包含压缩算法列表，用于后后续的压缩阶段使用。另外还有随机数 randmo_c 用于后续秘钥的生成。最后还包括扩展字段 extension 支持协议相关算法的参数以及其余辅助信息。

（2）Server-Hello +Server_cerficate+ server_hello_done

    server_hello 服务端返回协商的信息结果，包括使用的协议版本，选择的加密套件，以及使用的压缩算法 随机数（随机数用于后续的秘钥协商）

    server_certificate 服务器端配置对应的证书链，用于身份验证和秘钥交换

    server_Hellodone 通知客户端 server_hello 信息发送结束

（3）证书校验

     客户端证书的合法性，若是验证经过才会进行后续的通讯，合法性验证主要包括下面的环节：

       证书链的可信任、证书是否吊销、证书是否在有效期内、域名，核实证书的域名是不是当前访问的域名相匹配。

（4）Client_key_excahage+ change_chiper_spec+encrypted_handshake_message

       client_key_exchage 合法性验证经过以后，客户端计算产生随机数 pre-master ,并用证书的Pk 加密发送给服务器。

      当客户端获取所有的计算协商秘钥须要的信息： 两个明文随机数 Radmon_c 和 Radmon-S 和本身计算产生的 pre-master 计算获得协商秘钥

      enc_key=fuc(randmo_C,randmo_s,pre-Master)

      change_chiper_spec,客户端通知服务器后续的通讯都采用协商的通讯加密秘钥和加密算法进行加密通讯，

      encrypted_handshake_message 结合前面全部的通讯参数的hash值和其相关的信生成一段数据，采用协商的 session-secret 与算法进行加密以后发送给服务器用于数据与握手验证

 5）Change_ciper_spec +encrypted_handshake_message

       服务器使用私钥解密加密的per-master 数据，基于以前交换的两个明文随机书卷 Random_c 和 random_S 计算协商秘钥 enc_key=fuc(randmo_C,randmo_s,pre-Master)

      计算以前所接受信息的hash 值，而后解密客户端发送 encrypted_handshake_message 验证数据和秘钥的正确性

      encrypted_handshake_message验证完以后，服务器结一样发送 change_cipher_spec以告知客户端后续的通讯采用协商秘钥与算法加密通讯

      encrypted_handshake_message服务器结合当前全部的通讯参数生成一段数据并采用协商秘钥 session secret 与算法加密并发到客户端

（6）结束握手

      客户端计算全部接受到的信息的hash值，并采用协商秘钥解密 encrypted_handshake_message 验证服务器发送的数据和秘钥，验证经过则完成握手。

（7）加密通讯

   开始使用协商秘钥与算法进行加密通讯

对TLS协议进行形式化分析的思惟导图

 下面是对 论文形式化工具Scyther 优化实例分析的关于 TSL的整理

   做者对TLS的形式化过程当中的涉及到如何将角色模型转化成安全模型的并无说明，  只是将TSL.spdl执行的结果 截图，而后说明TLS是存在安全隐患的，分别在强安全模型和DY模型下面进行了低手的攻击测试

  另外，  做者对攻击的轨迹路径没有说明。对存在的多种的轨迹路径只是截了一张图来简单的说明 确实存在安全的问题

 

Client Hello

握手第一步是客户端向服务端发送 Client Hello 消息，这个消息里包含了一个客户端生成的随机数 Random一、客户端支持的加密套件（Support Ciphers）和 SSL Version 等信息。经过 Wireshark 抓包，咱们能够看到以下信息：

Wireshark 抓包的用法能够参考这篇文章

Server Hello

第二步是服务端向客户端发送 Server Hello 消息，这个消息会从 Client Hello 传过来的 Support Ciphers 里肯定一份加密套件，这个套件决定了后续加密和生成摘要时具体使用哪些算法，另外还会生成一份随机数 Random2。注意，至此客户端和服务端都拥有了两个随机数（Random1+ Random2），这两个随机数会在后续生成对称秘钥时用到。

Certificate

这一步是服务端将本身的证书下发给客户端，让客户端验证本身的身份，客户端验证经过后取出证书中的公钥。

Server Key Exchange

若是是DH算法，这里发送服务器使用的DH参数。RSA算法不须要这一步。

Certificate Request

Certificate Request 是服务端要求客户端上报证书，这一步是可选的，对于安全性要求高的场景会用到。

Server Hello Done

Server Hello Done 通知客户端 Server Hello 过程结束。

Certificate Verify

客户端收到服务端传来的证书后，先从 CA 验证该证书的合法性，验证经过后取出证书中的服务端公钥，再生成一个随机数 Random3，再用服务端公钥非对称加密 Random3生成 PreMaster Key。

Client Key Exchange

上面客户端根据服务器传来的公钥生成了 PreMaster Key，Client Key Exchange 就是将这个 key 传给服务端，服务端再用本身的私钥解出这个 PreMaster Key 获得客户端生成的 Random3。至此，客户端和服务端都拥有 Random1 + Random2 + Random3，两边再根据一样的算法就能够生成一份秘钥，握手结束后的应用层数据都是使用这个秘钥进行对称加密。为何要使用三个随机数呢？这是由于 SSL/TLS 握手过程的数据都是明文传输的，而且多个随机数种子来生成秘钥不容易被暴力破解出来。客户端将 PreMaster Key 传给服务端的过程以下图所示：

Change Cipher Spec(Client)

这一步是客户端通知服务端后面再发送的消息都会使用前面协商出来的秘钥加密了，是一条事件消息。

Encrypted Handshake Message(Client)

这一步对应的是 Client Finish 消息，客户端将前面的握手消息生成摘要再用协商好的秘钥加密，这是客户端发出的第一条加密消息。服务端接收后会用秘钥解密，能解出来讲明前面协商出来的秘钥是一致的。

Change Cipher Spec(Server)

这一步是服务端通知客户端后面再发送的消息都会使用加密，也是一条事件消息。

Encrypted Handshake Message(Server)

这一步对应的是 Server Finish 消息，服务端也会将握手过程的消息生成摘要再用秘钥加密，这是服务端发出的第一条加密消息。客户端接收后会用秘钥解密，能解出来讲明协商的秘钥是一致的。

Application Data

到这里，双方已安全地协商出了同一份秘钥，全部的应用层数据都会用这个秘钥加密后再经过 TCP 进行可靠传输。

双向验证

前面提到 Certificate Request 是可选的，下面这张图展现了双向验证的过程：

握手过程优化

若是每次重连都要从新握手仍是比较耗时的，因此能够对握手过程进行优化。从下图里咱们看到 Client Hello 消息里还附带了上一次的 Session ID，服务端接收到这个 Session ID 后若是能复用就再也不进行后续的握手过程。

除了上述的 Session 复用，SSL/TLS 握手还有一些优化技术，例如 False Start、Session Ticket 等

参考文献：

[1] File O P. Network Infrastructure for Ethernet/IP: Introduction and Considerations[J]. ODVA Publication PUB00035R0, 2007.  
[2]EtherNet/IP:Industrial Protocol White Paper   Institute of Electrical and Electronic Engineers,
[3] File O P. Securing EtherNet/IPTM Networks: Introduction and Considerations[J]. ODVA Publication PUB00269R1.1, 2011.
[4] File O P. Common Industrial protocol CIPTM and the family of CIP networks: Introduction and Considerations[J]. ODVA Publication PUB00123R1,2016(引用的部分是隐士和显示传输的两种方式)
[5]Jack Visoky, Joakim Wiberg, Nancy Cam-Winget. Presented at the ODVA 2018 Industry Conference & 18th Annual Meeting October 10, 2018 Stone Mountain, Georgia, USA.   TLS `1.3对CIP的影响
[6]Brian Batke, Joakim Wiberg&Dennis Dube.CIP Security Phase1 Secure Transport for EtherNet/IP.Presented at the ODVA 2015 Industry Conference&17th Annual Meeting  ---TLS和DLTS安全性能的介绍
[7] A. Ginter, “The Top 20 Cyber Attacks Against Industrial Control Systems,”  https://ics-cert.us-cert.gov/sites/default/files/ICSJWGArchive/ QNL DEC 17/Waterfall top-20-attacks-article-d2%20- %20Article S508NC.pdf.   [8] 冯涛,鲁晔,方君丽.工业以太网协议脆弱性与安全防御技术综述[J]. 通讯学报, 2017(S2). [9]Ryan Grandgenett ,Robin Gandhi,William Mahoney. Exploitation of Allen Bradley's implementation  of etherNet/IP for denial of service against industrial control systems  -----漏洞 [10]Sheffer Y, Holz R, Saint-Andre P. Summarizing known attacks on transport layer security (TLS) and datagram TLS (DTLS)[R]. 2015.  [11]Sheffer Y, Holz R, Saint-Andre P. Recommendations for Secure Use of Transport Layer Security (TLS) and Datagram Transport Layer Security (DTLS)[R]. 2015.  [12]Rescorla E. The transport layer security (TLS) protocol version 1.3[R]. 2018.  [13] Song D X . Athena: a New Efficient Automatic Checker for Security Protocol Analysis[C]// IEEE Workshop on Computer Security Foundations. IEEE Computer Society, 1999. ------  算法 [14] Cremers C J F , Mauw S . Operational Semantics of Security Protocols[C]// International Conference on Scenarios: Models. Springer-Verlag, 2005.   ------Spdl 语言 [15]韩旭，陆思奇&程庆丰.形式化工具Scyther优化与实例分析 [16]陆思奇，程庆丰&赵进华.安全协议形式化分析工具比较研究 [17]魏成坤, 刘向东, 石兆军. OAuth2.0协议的安全性形式化分析[J]. 计算机工程与设计, 2016, 37(7):1746-1751. [18] Cremers C .Scyther User manual [19] MEMBER, IEEE, Dolev D , et al. On the Security of Public Key Protocols[J]. IEEE Transactions on Information Theory, 2003, 29(2):198-208.   --------Dolev -Yao模型 [19]Cremers C ,HorvatM , Scott S , et al. Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication[C]// 2016 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society, 2016. [20]Cremers C J F . The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols[C]// Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings. Springer-Verlag, 2008. -------  介绍了Scyther的功能能够性能 [21]Krawczyk H , Paterson K G , Wee H . On the Security of the TLS Protocol: A Systematic Analysis[J]. 2013.   [23] Rescorla E, Modadugu N. Datagram transport layer security version 1.2[R]. 2012.
联系我们 沪ICP备13005482号-10