TLS1.2协议安全性分析

摘 要：安全传输层协议（TLS）用于在两个通信应用程序之间提供保密性和数据完整性。详细地分析了TLS协议，并给出了TLS1.2协议的具体工作流程。通过传输层协议中客户端对服务端的认证和服务端对客户端的认证来建立安全模型，并基于计算模型Blanchet使用自动化工具CryptoVerif证明其认证性和安全性。

关键词：TLS1.2；安全协议；计算模型

中图分类号：TP393

文献标识码：A 文章编号：1672-7800（2015）005-0154-04

作者简介：牛乐园（1990-），女，河南许昌人，中南民族大学计算机科学学院硕士研究生，研究方向为信息安全。

0 引言

人类建立了通信系统后，如何保证通信安全始终是一个重要问题。伴随着现代通信系统的建立，人们利用数学理论找到了一些行之有效的方法来保证数字通信安全。简单而言就是将双方通信的过程进行保密处理，比如对双方通信的内容进行加密，这样可有效防止偷听者轻易截获通信内容。SSL（Secure Sockets Layer） 及其后续版本 TLS（Transport Layer Security）是目前较为成熟的通信加密协议，常被用于在客户端和服务器之间建立加密通信通道。TLS是安全传输层协议，用于在两个通信应用程序之间提供保密性和数据完整性。截至目前其版本有1.0，1.1、1.2[1]，由两层协议组成：TLS 记录协议（TLS Record）和 TLS 握手协议（TLS Handshake）。

1 TLS协议结构

TLS协议是对SSL协议规范后整理的协议版本，建立在可靠的传输层上，如TCP（UDP则不行）。应用层可利用TLS协议传输各种数据，来保证数据的安全性和保密性[2]。

安全传输层协议（TLS）用于在两个通信应用程序之间提供保密性和数据完整性。该协议由两层组成：TLS 记录协议（TLS Record）和TLS握手协议（TLS Handshake）。较低层为 TLS记录协议，位于某个可靠的传输协议（如TCP）上。

TLS记录协议是一种分层协议。每一层中的信息可能包含长度、描述和内容等字段。记录协议支持信息传输、将数据分段到可处理块、压缩数据、应用 MAC、加密以及传输结果等，并对接收到的数据进行解密、校验、解压缩、重组，然后将它们传送到高层客户机。

TLS记录层从高层接收任意大小不间断的连续数据。密钥计算：记录协议通过算法从握手协议提供的安全参数中产生密钥、IV 和 MAC 密钥。TLS 握手协议由3个子协议组构成，允许对等双方在记录层的安全参数上达成一致、自我认证、例示协商安全参数、互相报告出错条件。

TLS握手协议由3种协议封装，包括改变密码规格协议、警惕协议、握手协议。TLS协议结构如图1所示。

2 TLS1.2消息流程

在整个通讯过程中，为实现TLS的安全连接，服务端与客户端要经历如下5个阶段[3]：①Client申请链接，包含自己可以实现的算法列表以及其它信息；②Server回应链接，回应中确定了这次通信所使用的算法，将证书发送给对方，证书中包含了自己的身份和公钥；③Client在收到消息后会生成一个秘密消息ClientKeyExchange――（此秘密消息经处理后，将用作加密密钥（会话密钥）），用Web服务器的公钥加密并传至Server；④Server再用私钥解密秘密消息ClientKeyExchange，并进行处理，生成会话密钥（用于之后的数据加密），会话密钥协商成功；⑤Client和Server得到会话密钥，并用此会话密钥进行数据加密。

TLS1.2在传输层协议的消息主要包含8条消息，消息结构如图2所示，分别是ClientHello版本协商、ServerHello版本协商、Server Certificate证书消息、HelloDone接收结束标识、 ClientKeyExchange即Client交换密钥消息、Client的Finished消息、CertificateVeri验证证书消息、Server的Finished消息。

2.1 ClientHello和消息

ClientServer

client_version|| client_random|| session_id|| cipher_suites|| compression_methods|| extensions

消息描述：该消息包括客户端的版本号client_version，用于告知服务器client可以支持的协议最高版本，来协商安全协议版本。client_random是client产生的一个随机数，由client的日期和时间加上28字节的伪随机数组成，用于后面的主密钥计算。session_id由服务连接得到，发送给server来建立一个新的会话连接。cipher_suites是client提供给server可供选择的密码套件，用于协商密钥交换，数据加密以及散列算法。compression_methods是客户端支持的压缩算法。extensions是客户端的扩展域。

client_version： Protocol version（协议版本），该字段表明了客户能够支持的最高协议版本3.3。

random：它由客户的日期和时间加上28字节的伪随机数组成，该客户随机数将用于计算master secret（主秘密）和prevent replay attacks（防止重放攻击）。

session_id：一个会话ID标识一个可用的或者可恢复的会话状态。一个空的会话ID表示客户想建立一个新的TLS连接或者会话，而一个非空的会话ID表明客户想恢复一个先前的会话。session_id有3个来源：①之前的会话连接；②当前连接，客户端仅仅想通过更新random结构得到连接值时使用；③当前激活的连接，为了建立几个独立的连接而不再重复发起连接握手。

2.2 ServerHello消息

ServerClient：

server_version||server_random|| session_id|| cipher_suites|| compression_methods|| extensions

消息描述：该消息包含6个消息项，server_version取客户端支持的最高版本号和服务端支持的最高版本号中的较低者，本文所用的是TLS1.2。server _random是服务端生成的随机数，由服务器的时间戳加上28字节的伪随机数组成，也用于主密钥的生成。session_id提供了与当前连接相对应的会话的标识信息。从客户端处接收到会话标识后，服务器将查找其缓存以便找到一个匹配的session_id。

server_version： Protocol version（协议版本），取客户端支持的最高版本号和服务端支持的最高版本号中的较低者。TLS版本为3.3。random：它由客户的日期和时间加上28字节的伪随机数组成，该客户随机数将用于计算master secret（主秘密）和prevent replay attacks（防止重放攻击）。session_id：该域提供了与当前连接相对应的会话的标识信息。如果从客户端接收到的会话标识符非空，则服务器将查找其缓存以便找到一个匹配。

2.3 Server Certificate消息

ServerClient：

version||serialNumber||algorithmIdentifier||issuer||utcTime||subject_name||subject_key_info|| signature

消息描述：该项消息为可选项，证书主要包含4部分内容，version是证书版本，文章统一定为X509v3。主体名称指明使用该证书的用户为server_subject。subject_key_info是证书包含的公钥信息，该消息项有两项内容：一个是证书的公钥，发送给client后用于加密client生成的预主密钥，并把密文信息发送给server。server收到该密文信息后可以使用自己的私钥解密得到预主密钥；另一个是所用的散列算法。signature：证书验证签名信息，用以验证证书。version：证书版本号，为X.509V3。subject_name：证书主体名称。

subject_key_info：标识了两个重要信息：①主体拥有的公钥的值；②公钥所应用算法的标识符。证书私钥对证书的所有域及这些域的Hash值一起加密。

2.4 ServerKeyExchange消息

ServerClient：

KeyExchangeAlgorithm|| ServerDHParams

KeyExchangeAlgorithm：密钥交换算法，文章定义的密钥交换算法为RSA。ServerDHParams：Diffi-Hellman参数，若交换算法为RSA，则此项为空。

2.5 CertificateRequest消息

ServerClient：

certificate_types|| supported_signature_algorithms|| certificate_authorities

消息描述： 可选消息项，该消息是Server服务器向Client请求验证证书信息。在一般应用中只对Server服务器进行认证，而Server服务器要允许只有某些授权的Client才能访问服务器，此时需要用到该消息对Client进行认证。Client认证是通过Server服务器给Client发送一条 CertificateRequest消息而开始，如果Server发送这条消息，则Client必须向server发送自己的证书。客户端收到该消息后，发送一条 Certifcate 消息（与服务器传送证书的消息一样）和一条 CertificateVerify 消息予以应答。

certificate_type：客户端提供的证书类型，该处为rsa_sign。supported_signature_algorithms：可以验证server的散列/签名算法对。certificate_authorities：可以接受证书消息的特定名称。

2.6 Client Certificate消息

ClientServer：

version||serialNumber||algorithmIdentifier||issuer||utcTime||subject_name||subject_key_info|| signature

消息描述：可选消息项，该证书主要包含4部分内容，version是证书版本，文章统一定为X509v3。主体名称指明使用该证书的用户为server_subject。subject_key_info是证书包含的主要公钥信息，该消息项有两项内容：一个是证书的公钥，另一个是所用的散列算法。signature是证书验证签名信息，用以验证证书。

version：证书的版本号，为X.509V3。subject_name：证书主体名称。subject_key_info：标识了两个重要信息：①主体拥有的公钥的值；②公钥所应用的算法的标识符。算法标识符指定公钥算法和散列算法（如RSA和SHA-1）。signature：用证书私钥对证书的所有域及这些域的Hash值一起加密。

2.7 ClientKeyExchange消息

ClientServer：

KeyExchangeAlgorithm|| EncryptedPreMasterSecret

消息描述：该消息是密钥交换消息。之前的消息协商中规定密钥交换算法为RSA算法，所以该消息中KeyExchangeAlgorithm的内容为RSA。此时，client随机生成一个48字节的预主密钥，用从server证书得来的公钥来加密这个预主密钥，加密算法为RSA算法。client加密预主密钥并在ClientKeyExchange消息中将密文EncryptedPreMasterSecret发给server，使server得到预主密钥。

KeyExchangeAlgorithm：算法选择为RSA。EncryptedPreMasterSecret：客户端生成一个48字节的预主密钥，用从server证书得来的公钥来加密该预主密钥，加密预主密钥消息并发送密文。

2.8 CertificateVerif消息

ClientServer

handshake_messages[handshake_messages_length]

消息描述：可选消息项，如果服务器请求验证客户端，则该消息完成服务器验证过程。客户端发送一个certificate_verify消息，其中包含一个签名，对从第一条消息以来的所有握手消息的HMAC值（用master_secret）进行签名。handshake_messages指所有发送或接收的握手消息，从clienthello消息开始到CertificateVerif消息之前（不包括CertificateVerif消息）的所有消息集合，包括握手消息的类型和变长字段。这是到目前为止HandShake结构的整合。

3 Blanchet演算模型建立流程

Blanchet演算模型主要包括类型定义、时间定义、方法定义、通道定义、时间声明、初始化进程描述[4]、客户端进程描述与服务端进程描述。TLS1.2最主要的功能体现在客户端与服务端的消息传递。

3.1 协议事件声明

在Blanchet演算中首先要声明要证明的事件。TLS1.2协议的消息流程中最重要的就是认证性和密钥的保密性[5]。认证性包括客户端对服务端的认证和服务端对客户端的认证，保密性是对会话密钥的秘密性进行认证。表示server事件发生之前client事件一定发生，用来验证服务端用户。在更严格的定义下进行服务端验证，事件声明代码如下。

event server（output）.

event client（output）.

query x：output；

event server（x）==>client（x）.

query x：output；

event inj：server（x）==>inj：client（x）.

query secret premastersecret.

3.2 初始化进程

协议模型初始化进程如下所示，ClientProcess表示客户端进程[6]，ServerProcess表示服务端端进程，表示多个ClientProcess进程并发执行，集中一次模拟现实协议执行。

process

in（start，（））；

new seedone：rsakeyseed；

let pkeyrsa：rsapkey=rsapkgen（seedone） in

let skeyrsa：rsaskey=rsaskgen（seedone） in

new seedtwo：keyseed；

let signpkey：pkey=pkgen（seedtwo） in

let signskey：skey=skgen（seedtwo） in

new keyhash：hashkey；

out（c，（pkeyrsa，signpkey，keyhash））；

（（！ N ClientProcess） |

（！ N ServerProcess） ）

3.3 客户端和服务端进程

客户端的消息流程包括版本协商、算法协商、密钥协商、密钥交换和请求验证。版本协商是协商客户端、服务端可以通用的版本[7]，一般是客户端和服务端都支持的最高版本，密钥协商完成后Client向Server发送verifydata认证请求消息，内容包括username、servicename、methodname，method_specific，请求Server验证身份，并在此定义对客户端的验证事件client（verifydata）。

服务端进程首先接收客户端进程发送的版本信息[8]，并与自己的版本信息匹配协商得到协商版本client_version。版本信息协商完成后接收客户端所支持的算法信息，至此算法协商完成。进入密钥协商阶段，首先Server接收Client发送的密钥参数信息c_s_random_s，用来计算hash验证；Server收到Client的验证请求后对Client进行验证并接收Client发来的验证消息，用所收到的所有消息计算验证信息。在此插入事件event server（verifydata_fc）来验证客户端。

3.4 验证结果

本文在介绍TLS1.2协议的基础上对其数据流程进行分析[9]，使用Blanchet建立模型并分析其安全性和认证性。经过一系列的流程跟进并使用自动化证明工具Cryptoverif对TLS1.2进行模型建立，经过一系列的Game转换得出分析结果如图3所示[10]。结果证明，TLS1.2协议的会话密钥具有安全性，在认证阶段能够对客户端通过消息签名进行验证。

4 结语

为了研究TLS1.2协议在应用中的安全性，本文对TLS1.2协议的消息流程进行了分析。通过对每一步消息流中消息项的研究分析，得出TLS1.2协议的整体消息结构，最终实现服务端对客户端的验证流程分析。基于Blanchet演算对分析的消息流程应用一致性对服务端认证客户端和客户端对服务端的验证建立模型。协议模型通过协议转换工具转换为CryptoVerif的输入代码TLS1.2.cv，使用CryptoVerif对模型进行分析，并证明了TLS1.2协议的安全性与认证性。后续研究中将给出TLS1.2协议的Java安全代码，并分析其安全性。

参考文献：

[1] 陈力琼，陈克非.认证测试方法对TLS协议的分析及其应用[J].计算机应用与软件，2008，25（11）：6-7.

[2] 于代荣，杨扬，马炳先，等.基于身份的TLS协议及其BAN逻辑分析[J].计算机工程，2011，37（1）：142-144.

[3] MORRISSEY P， P SMART N，WARINSCHI B.The TLS handshake protocol： a modular analysis[J]. Journal of Cryptology，2010，23（2）：187-223.

[4] 卢敏，申明冉.基于RSA签名的TLS协议的新攻击发现及其改进[J].消费电子，2013（14）：69-70.

[5] 高志伟，耿金阳.基于优先级策略的 TLS 握手协议研究[J].石家庄铁道大学学报：自然科学版，2014（3）：69-74.

[6] 唐郑熠，李祥.Dolev-Yao攻击者模型的形式化描述[J].计算机工程与科学，2010（8）：36-38.

[7] 邵飞.基于概率进程演算的安全协议自动化分析技术研究[D].武汉：中南民族大学，2011.

[8] 朱玉娜.密码协议符号分析方法的计算可靠性研究[D].郑州：信息工程大学，2008.

[9] 郑清雄.基于Spi 演算的安全协议验证[J].计算机应用与软件，2011，28（3）：262-264，292.

[10] 陈伟，杨伊彤，牛乐园.改进的OAuth2.0协议及其安全性分析[J].计算机系统应用，2014，23（3）：25-30.