Page 237 - 《软件学报》2021年第9期

陆思奇 等:强安全模型下 TLS1.3 协议的形式化分析与优化 2861

3.1 优化协议的结构
从 ServerConfiguration 的有效使用期限可以看出,客户端需要频繁地缓存半静态公钥.这对于握手协议的
效率来说造成了一定的影响,并且也无法从根本上解决 0-RTT 数据的安全性问题.关于 0-RTT 数据的安全性问
题,根据第 2 节中形式化分析的结果,主要包括没有 PFS 安全和无法抵抗 KCI 攻击.本文基于 1-RTT semi-static
模式设计了一种新的支持 0-RTT 数据的协议,该协议可以有效抵抗 KCI 攻击,提高了 0-RTT 数据的安全性.协议
的消息交互过程如图 12 所示,由图可见:相比原协议传输,优化后的协议在原 Early Data 消息的基础上,添加了客
户端对 Early Data 和时间戳的签名.

chello,ceks,{Sig
sk(c) (Hash(Early Data),TimeStamp),Early Data}
⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯→
eadk
sfk (chello,ceks,shello,seks,ssks)}
shello,seks,{ssks,MAC
←⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯⎯ Server
htk
Client
Fig.12 Handshake process of the optimized protocol
图 12 优化协议的握手流程
服务器在收到客户端的第 1 条消息后,首先计算出 eadk 对 0-RTT 数据进行解密,然后使用客户端的公钥对
其中的签名进行解密,解密后对时间戳进行验证.此外,将时间戳 TimeStamp 放在签名中,同样防止了敌手对时间
戳的篡改,从而排除重放攻击的可能,再与 Early Data 的 Hash 值进行对比:如果二者不匹配,则认为这不是一个合
法的客户端发送的 0-RTT 数据,服务器应该选择立即丢弃这个数据.
3.2 优化协议的安全性证明
本文采用了 CK 模型对上述优化协议进行分析,该模型在可信的计算环境下能够简化协议的设计,使协议
更加具有普遍性和实用性.
使用基于 game 的方法对优化协议的安全性进行分析,证明在签名算法的安全性和 Gap-DH 问题的复杂性
以及密钥导出函数的安全性的前提下,该协议能够抵抗 KCI 攻击.证明过程注意以下两点.
(1) session-key query 查询的密钥为 Early Data 的密钥 eadk,而不是 Application Data 的密钥 atk;
(2) 定义匹配的会话为(chello,ssks)相等的会话(只针对 eadk,不针对 atk).
定理 1. 在假设服务器证书机制的安全性、求解 Gap-DH 的困难性、密钥导出函数的安全性、客户端签名
机制的安全性的前提下,优化协议能够抵抗 KCI 攻击.
• 正确性
s
假设一个诚实的协议参与者拥有抗重放机制来产生 chello,那么 chello 唯一识别 ceks=g .也就是说,对于一
对匹配的会话,协议双方的 chello,ceks,ssks 都相同,因此计算出相同的 eadk.
• 安全性
接下来定义一系列 Game.
(1) Game 0:优化协议的真实执行过程;
*
s
(2) Game 1:服务器证书不可伪造.游戏规则与 Game 0 相同,在该游戏中,攻击者使用随机值 ssks 代替 g ,
因为签名或者其他任何用于认证 ssks 的方案是安全的,因此攻击者无法赢得 Game 1.也就是说,攻击
者不能随意伪造服务器的证书;
(3) Game 2:eadk 的安全性.该游戏发生在 s 被泄露之前,游戏规则与 Game 0 相同,但是攻击者不能使用
xs
xs
xs
party corruption 查询.在该游戏中,攻击者查询 g ,或者从随机值和 g 中区分出 g .根据 Gap-DH 困难
xs
s
x
性假设:在给出 g,g ,g 和 DDH 查询的前提下,计算 g 是困难的.即,攻击者赢得 Game 2 的概率等同于
求解 Gap-DH 难题;
(4) Game 3:eadk 的安全性.该游戏发生在 s 被泄露之前,游戏规则与 Game 0 相同,但是攻击者不能使用
*
party corruption 查询.在该游戏中,攻击者在一个会话完成后,用随机值代替另一个会话的 eadk .因为