TLS(传输层安全)协议是一种广泛使用的网络协议，主要用于在服务器和客户端之间建立安全通道。TLS 1.3.详细分析18草案，并使用proverif建模已经进行了安全论证。本文是中国科技大学正式化方法的一项重要任务，不可避免地有点仓促。如有问题，请纠正。

在加密通信过程中，有时要用到共享密钥(shared key)，这信双方共享这个密钥，但要保证攻击者找不到。Diffie-Hellman密钥交换协议确保即使攻击者拦截了通信通道上的所有信息，也不能在可接受的时间内计算出共享密钥。

相比传统加密算法，AEAD加密算法支持解密前进行验证，以得知密钥正确性。为了便于理解，此处选一种AEAD加密分析进行说明。

E&M (Encryption and MAC)：首先对密文进行加密，然后使用同一密钥进行MAC运算，将Concat(Ciphertext,MAC)发给对方。对方收到消息后先解密，然后将解密的信息重新做MAC运算，如果和收到的MAC值相同，则验证成功，说明密钥正确。(下图选自wiki)

有时，可以添加nonce（如序列号）唯一地标定每次加密过程。

在安全认证中，我们需要再定义一种弱AEAD加密算法，它允许对加密的数据进行修改，定义相应方法为aead_forged，接受两个参数，第一个为预期修改的信息p，第二个是加密后的信息。输出的信息经过解密后变成p。除此之外，攻击者可以使用aead_leak方法直接由加密过的数据得到被加密的值。

Proverif建模如下：

(********************************************************)
(* Authenticated Encryption with Additional Data *)
(* extended with with weak/strong algorithms: See Lucky13, Beast, RC4 *)
(********************************************************)

type ae_alg.
const WeakAE, StrongAE: ae_alg.
type ae_key.
fun b2ae(bitstring):ae_key [data].

fun aead_enc(ae_alg, ae_key, bitstring, bitstring, bitstring): bitstring. (*编码*)
fun aead_forged(bitstring,bitstring): bitstring.

fun aead_dec(ae_alg, ae_key, bitstring, bitstring, bitstring): bitstring (*解码*)
reduc forall a:ae_alg, k:ae_key, n:bitstring, p:bitstring, ad:bitstring;
    aead_dec(a, k, n, ad, aead_enc(a, k, n, ad, p)) = p
otherwise forall a:ae_alg, k:ae_key, n:bitstring, p:bitstring, ad:bitstring,p':bitstring,ad':bitstring;
    aead_dec(WeakAE, k, n, ad, aead_forged(p,aead_enc(WeakAE, k, n, ad', p'))) = p.

fun aead_leak(bitstring):bitstring
reduc forall k:ae_key, n:bitstring, ad:bitstring, x:bitstring;
      aead_leak(aead_enc(WeakAE,k,n,ad,x)) = x.

可以将一个对象映射到某一个范围中的值。如果有两个不同对象映射到同一个值，则称为哈希冲突。一般来讲，可以通过检测两个值的Hash值是否相等，在不知道这两个具体值的情况下判断它们是否相等。和上面类似，我们可以定义一种“脆弱”的哈希算法，它很容易产生冲突。这样两个不相同的数可能被错误地被认证成相同。假设该算法下所有数据的哈希值全部被映射为collision。

哈希的proverif建模：

(********************************************************)
(* Hash Functions, including those with collisions. See SLOTH *)
(********************************************************)

type hash_alg.
const StrongHash: hash_alg [data].
const WeakHash: hash_alg [data].

const collision:bitstring [data].
fun hash_ideal(bitstring):bitstring.

fun hash(hash_alg,bitstring): bitstring
reduc forall x:bitstring;
      hash(WeakHash,x) = collision
otherwise forall x:bitstring;
      hash(StrongHash,x) = hash_ideal(x).

Hash方法可以较好地用于验证，但生成的哈希值很容易伪造。HMAC可以理解为使用密钥进行哈希，具体定义为：
$$HMAC(K,m)=H((K^{\prime }XORopad)||H((K^{\prime }XORipad)||m))$$
当K’大于某个长度时，K’=H(K)，否则K’=K。双竖线表示连接。opad和ipad解释如下：

• opad is the block-sized outer padding, consisting of repeated bytes valued 0x5c
• ipad is the block-sized inner padding, consisting of repeated bytes valued 0x36

当然在Proverif中，可以隐藏很多实现的细节。定义一个名为mac_key的类型用于标记HMAC中的密钥hmac_ideal输入密钥和待编码数据，输出编码后的数据。hmac在mac_key的基础上添加哈希算法作为第一个参数。如果是WeakHash，输出的永远都是collision，否则按hmac_ideal就行正常编码。

(********************************************************)
(* HMAC *)
(********************************************************)

type mac_key.
fun b2mk(bitstring):mac_key [data,typeConverter].

fun hmac_ideal(mac_key,bitstring): bitstring.

fun hmac(hash_alg,mac_key,bitstring):bitstring
reduc forall k:mac_key, x:bitstring;
      hmac(WeakHash,k, x) = collision
otherwise forall x:bitstring, k:mac_key;
      hmac(StrongHash,k, x) = hmac_ideal(k,x).

签名方拥有一个私钥，将使用私钥对待签名数据进行加密，随后将加密后的签名和原数据发给检验方。检验方收到数据后，使用公钥对签名进行解密，如果解密后的数据和原数据相同，则说明数据为签名方所发。由于签名需要用到私钥，任何未得知私钥的攻击者都无法构造签名。

在Proverif中可以定义两个类型：公钥pubkey和私钥privkey。对于任意一个私钥，可以假设总可以找到对应的公钥，即定义pk(privkey)，返回pubkey。但反过来，基于安全性，不存在对应的sk(pubkey)，也就是说不能根据公钥就获取私钥。verify对使用私钥k对信息x的签名sign(k,x)进行验证。给定k对应的公钥pk(k)和x，如果签名信息是sign(k,x)，则验证成功，应该返回true。整体代码如下：

(********************************************************)
(* Public Key Signatures *)
(********************************************************)

type privkey.
type pubkey.
fun pk(privkey): pubkey. 
const NoPubKey:pubkey.

(* RSA Signatures, typically the argument is a hash over some data *)

fun sign(privkey,bitstring):bitstring.

fun verify(pubkey,bitstring,bitstring): bool
reduc forall k:privkey, x:bitstring;
      verify(pk(k),x,sign(k,x)) = true.

HKDF是基于HMAC的密钥派生算法，它可以将初始密钥扩展成更强大的密钥。

主要分为两部：提取和扩展。提取是把密钥转化为固定长度的伪随机数，扩展是将提取到的伪随机数扩展到指定长度。

提取的具体过程可以用如下公式表示：
$HKDF-Extract(salt,IKM)=HMAC(salt,IKM)$得到PRK，其中salt是盐，IKM是原始密钥。

扩展可以用如下公式表示：
$HKDF-Expand(PRK,info,L)=OKM$，OKM是长度为L的密钥输出，info是可选上下文和应用程序特定信息。
首先计算一系列哈希值，记为T(n)，其中n从0到255。
T(0)=长度为0的空字符串
$T(1)=HMAC(PRK,T(0)|info|0x01)$
$T(2)=HMAC(PRK,T(1)|info|0x02)$
$T(3)=HMAC(PRK,T(2)|info|0x03)$
直到计算到T(255)。
我们将这些T(n)连接起来，记为$T=T(1)|T(2)|\cdots |T(N)$，OKM即是T的前L个字节。

在TLS 1.3中，还需要用到HKDF-Expand-Label和Derive-Secret，它们的定义如下：

HKDF-Expand-Label(Secret, Label, HashValue, Length) =
HKDF-Expand(Secret, HkdfLabel, Length)

struct { 
        
      uint16 length = Length;
      opaque label<9..255> = "TLS 1.3, " + Label;
      opaque hash_value<0..255> = HashValue;
} HkdfLabel;
Derive-Secret(Secret, Label, Messages) =
HKDF-Expand-Label(Secret, Label,
Hash(Messages), Hash.Length)

HKDF的proverif实现：

(********************************************************)
(*  TLS 1.3 Key Schedule  *)
(********************************************************)

type label.
const client_finished, server_finished, master_secret, 
      client_key_expansion, server_key_expansion: label.
const tls13_client_handshake_traffic_secret, 
      tls13_server_handshake_traffic_secret, 
      tls13_client_early_traffic_secret, 
      tls13_client_application_traffic_secret, 
      tls13_server_application_traffic_secret, 
      tls13_key, tls13_iv, 
      tls13_early_exporter_master_secret, 
      tls13_exporter_master_secret, 
      tls13_resumption_master_secret, 
      tls13_resumption_psk_binder_key,
      tls13_finished: label.

fun tls12_prf(bitstring,label,bitstring): bitstring.

letfun prf(k:bitstring,x:bitstring) = 
       hmac(StrongHash,b2mk(k),x).

letfun hkdf_extract(s:bitstring,k:bitstring) =
       prf(s,k).

letfun hkdf_expand_label(k:bitstring,l:label,h:bitstring) = 
       prf(k,(l,h)).       							  
 
letfun derive_secret(k:bitstring,l:label,m:bitstring) = 
       hkdf_expand_label(k,l,hash(StrongHash,m)).

letfun kdf_0() = hkdf_extract(zero,zero).

letfun kdf_es(psk:preSharedKey) = 
       let es = hkdf_extract(zero,psk2b(psk)) in
       let kb = derive_secret(es,tls13_resumption_psk_binder_key,zero) in
       (es,b2mk(kb)).


letfun kdf_k0(es:bitstring,log:bitstring) = 
       let atsc0 = derive_secret(es, tls13_client_early_traffic_secret, log) in
       let kc0   = hkdf_expand_label(atsc0,tls13_key,zero) in
       let ems0   = derive_secret(es,tls13_early_exporter_master_secret,log) in
       (b2ae(kc0),ems0).
       	   

letfun kdf_hs(es:bitstring,e:bitstring) = 
       hkdf_extract(es,e).

letfun kdf_ms(hs:bitstring,log:bitstring) = 
       let ms =   hkdf_extract(hs , zero) in
       let htsc = derive_secret(hs, tls13_client_handshake_traffic_secret, log) in
       let htss = derive_secret(hs, tls13_server_handshake_traffic_secret, log) in
       let kch =  hkdf_expand_label(htsc,tls13_key,zero) in
       let kcm =  hkdf_expand_label(htsc,tls13_finished,zero) in
       let ksh =  hkdf_expand_label(htss,tls13_key,zero) in
       let ksm =  hkdf_expand_label(htss,tls13_finished,zero) in
       (ms,b2ae(kch),b2ae(ksh),b2mk(kcm),b2mk(ksm)).

letfun kdf_k(ms:bitstring,log:bitstring) = 
       let atsc = derive_secret(ms, tls13_client_application_traffic_secret, log) in
       let atss = derive_secret(ms, tls13_server_application_traffic_secret, log) in
       let ems 	= derive_secret(ms, tls13_exporter_master_secret, log) in
       let kc   = hkdf_expand_label(atsc,tls13_key,zero) in
       let ks   = hkdf_expand_label(atss,tls13_key,zero) in
       (b2ae(kc),b2ae(ks),ems).

letfun kdf_psk(ms:bitstring, log:bitstring) = 
       derive_secret(ms,tls13_resumption_master_secret,log).

包含一些未提到的方法，稍后将会讲到，这里仅做参考。

在通信协议中，可能出现第三者作为“中介”，伪造成对方和双方通信。在Diffie-Hellman密钥交换协议中，假设有一个攻击者Eve，他首先谎称自己是Bob和Alice建立通信，在得到Alice传过来的$A=g^a$后，扮成Alice和Bob通信，将$C=g^c$发给Bob，此时Bob生成共享密钥$C^B=g^{bc}$，并将$B=g^b$发给Eve，Eve收到B后，计算$C^c=g^{bc}$，作为其和Bob的共享密钥，同时选取随机数d，将$D=g^d$发给Alice，并将$A^d=g^{ad}$作为和Alice的共享密钥。这样Eve和Alice和Bob各有一对共享密钥。如果Alice通过共享密钥和Bob通信，则加密信息会先发给中间人Eve，Eve进行解密后使用和Bob的共享密钥再加密，将加密信息转发给Bob。这样Alice和Bob都认为消息是通过共享密钥直接发给对方的，而事实上它们的共享密钥并不相同，有一个中介Eve收取了它们所有的密钥并使消息都中中转给了Eve，Eve解密获得全部消息。

具体流程可参考下图：

该部分参考TLS 1.3文档。

TLS的主要目的是为两台通信计算机提供一个安全的交流通道，这个通道应该保持以下三条属性：

• 服务器是经过认证的，客户端不能连到恶意服务器上。对于服务器来说，客户端只需要选择性认证。验证的方法可以是通过非对称密钥或者预共享对称密钥(pre-shared symmetric key)。
• 攻击者无法获得信道上传输的有效数据（无法解密关键数据）。
• 数据无法被攻击者修改。

TLS协议包含一下两个主要部分：

• 握手协议：对双方进行认证、协商加密方式和参数、建立共享密钥等等。
• 记录协议：使用握手协议中建立的参数进行通信。一次完整的通信可能被分成多次会话，每次都有独立的密钥，这样破解一次会话得到的信息并不能破解其他会话。

      Client                              Server
Key   ^ ClientHello
Exch  | + key_share*
      | + pre_shared_key_modes*
      v + pre_shared_key*     ------>     ServerHello ^ Key
                                         + key_share* | Exch 
                                    + pre_shared_key* v
                                {EncryptedExtensions} ^ Server
                                {CertificateRequest*} v Params
                                       {Certificate*} ^
                                 {CertificateVerify*} | Auth
                                           {Finished} v
                        <-------- [Application Data*]
      ^ {Certificate*}
 Auth | {CertificateVerify*}
      v {Finished} -------->
        [Application Data] <-------> [Application Data]
+表示在之前提到的消息
*表示可选项
{}表示被握手得到的traffic secret保护
[]表示被对应于特定会话的traffic_secret_N保护

握手过程可以分为三步：

• 密钥交换：建立共享密钥、选择密码学参数。随后的所有信息都是被加密过的。
• 服务器参数：建立其他握手参数，比如客户端是否被认证、应用层协议支持等等。
• 认证

在密钥交换的过程中，客户端发送ClientHello消息，这个消息包含一个随机数（防止降级攻击，稍后会提到）、提供的协议版本、各种密钥。服务器处理ClientHello并决定合适的密码学参数。随后发出ServerHello作为响应，这个响应中包含协商的参数以及服务器决定使用的密钥。

随后，服务器发送如下两条信息：

• 加密后的扩展(EncryptedExtensions)：对决定密码学参数不需要的扩展及其他特殊性的请求进行响应。
• 认证请求(CertificateRequest)：用于认证客户端。当客户端无需认证时，跳过这一步。

• Certificate：当服务器不需要通过证书认证时被服务器忽略，当服务器没有给客户端发送认证请求时被客户端忽略。
• CertificateVerify：对整个握手过程进行签名。
• Finished：对于整个握手过程的MAC。这条消息提供密钥确认，将整个终端绑定到密钥上，在psk模式下也可以认证握手过程。

经历以上三个过程后，握手完成，此时可以传输应用层的数据。注意在客户端发送Finished之前不允许传输应用数据，这也是安全性论证的一个点，即论证TLS 1.3协议可以防止传输应用数据给未Finish认证的对象。

当客户端在ClientHello中传输的key_share不被服务器支持，服务器将响应HelloRetryRequest，客户端需要使用一个正确的key_share扩展再次发出请求。如果没有协商到合适的密码学参数（比如客户端的supported_groups和服务器不重合），服务器必须中止握手过程并发出警告。

完整过程如下：

Client                                    Server
ClientHello
+ key_share            -------->
                       <-------- HelloRetryRequest
                                     + key_share
ClientHello
+ key_share            -------->
                                     ServerHello
                                     + key_share
                           {EncryptedExtensions}
                           {CertificateRequest*}
                                  {Certificate*}
                            {CertificateVerify*}
                                      {Finished}
                   <-------- [Application Data*]
{Certificate*}
{CertificateVerify*}
{Finished}            -------->
[Application Data] <------->  [Application Data]

当握手结束时，服务器可以给客户端一个预共享密钥。在之后的握手过程中，客户端可以复用该密钥。由于服务器已被认证，在再次使用PSK时，服务器无需发送Certificate和CertificateVerify。当客户端提供PSK时，应该再提供一个key_share扩展给服务器，以允许服务器丢弃psk开始一个完整的握手（如果需要的话）。服务器会响应一个预共享密钥，同时可以响应key_share扩展来进行(EC)DHE密钥的建立，提供前向安全性(forward secrecy，即攻击者获取某一会话所有密钥数据后仍不能对之前的所有密钥解密)。

Part 1 密钥交换信息

从ClientHello可以得到以下四组参数：

• 客户端支持的AEAD算法和HKDF哈希对。
• (EC)DHE算法支持的群和key_share扩展。
• 签名算法。
• 预共享密钥和预共享密钥交换模式(psk_key_exchange_modes)。

服务器在ServerHello中指明如下的参数：

• 如果使用psk，则发送pre_shared_key表示选中的密钥。
• 如果不适用psk，则需要使用(EC)DHE和基于证书的认证来得到密钥。
• 如果使用(EC)DHE，服务器需要提供key_share扩展。
• 使用证书认证时，服务器需要发送证书和证书验证消息。

当服务器不能协商参数时，需要中止握手过程并发送handshake_failure或insufficient_security警告。

ClientHello数据块的C语言表示（选自TLS 1.3-18官方文档）：

uint16 ProtocolVersion;
opaque Random[32];
uint8 CipherSuite[2]; /* Cryptographic suite selector */
struct { 
        
      ProtocolVersion legacy_version = 0x0303; /* TLS v1.2 */
      Random random;
      opaque legacy_session_id<0..32>;
      CipherSuite cipher_suites<2..2^16-2>;
      opaque legacy_compression_methods<1..2^8-1>;
      Extension extensions<0..2^16-1>;
} ClientHello;

以下是逐项解释：

• legacy_version：在旧版本的TLS中，用于表示客户端支持最高的版本。在TLS 1.2中，它被设为0x0303。在TLS 1.3中，仍然保持这个值，但客户端还要在supported_versions扩展中指明版本偏好。
• random：32字节的随机数，稍后将讲它的用途。
• legacy_session_id：在TLS 1.3之前，和会话恢复(ses