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

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

手模型,可以选择 Scyther Compromise,其最新的版本为 Scyther Compromise-0.9.2).除此之外,该团队还开发了两
款相关的工具,分别是 Scyther-proof [26] 和 Tamarin [27] .
本文使用的 Scyther 工具版本为 Scyther Compromise-0.9.1,该工具可在 Linux,Windows 和 Mac OS X 系统
下运行.文中实验所选择的系统环境为英特尔 i5 的 2.5GHz 处理器、Ubuntu-16.04 操作系统、4G 内存的笔记本
电脑.对 Ubuntu 原有源进行添加和更新后,安装 python,graphviz,python-wxgdk3.0 插件,解压后即可使用.
1.2 CK安全模型
CK(canetti-krawczyk)模型 [28] 对敌手的能力进行了形式化的描述,反映了敌手在开放网络环境中拥有的真
实攻击能力:除了能够调度协议事件以及控制通信链路以外,攻击者还能够访问协议中使用或生成的一些秘密
信息.具体来说,CK 模型定义了一个“中间人”攻击者 A,A 全面控制通信链路,能够拦截和修改消息、延迟或阻止
消息传递、插入自己的消息、在不同的会话中交互消息以及安排所有会话的激活和会话消息的传递.此外,A 还
被允许通过以下查询获取信息.
(1) 会话状态暴露(session-state reveal):针对还未完成的会话(如输出会话密钥之前),A 能够通过此查询得
到特定会话的状态(如临时 DH 值的秘密指数,即临时私钥);
(2) 会话密钥查询(session-key query):在单个会话完成后,A 能够通过此查询得到会话密钥(在现实中,该
查询可通过密码学分析、已知密钥攻击等方法实现);
(3) 腐化参与者(party corruption):A 能够攻陷实体,得到长期私钥以及和会话具体相关的信息.此时,A 可控
制通信方所有行为.
这种模型允许攻击者显示一方测试会话时的长期私钥或显示一方的临时私钥,能帮助敌手获得更强的攻
击能力.
1.3 TLS1.3的安全性质
TLS1.3 握手协议旨在通过认证密钥交换机制(AKE)来协商密钥,这些密钥可以被记录层用来提供关键的
安全保证,包括消息的保密性和完整性.在 0-RTT 握手的情况下,应用程序数据由 PSK 保护,作为客户端第 1 条
消息的一部分.
本文分析 TLS1.3 协议以下安全性质.
1. 会话密钥安全:一个密钥协商协议被称为会话密钥安全的,如果它对于任何攻击者都满足如下性质:
(1) 未被攻陷的协议参与者在完成匹配的会话后生成的会话密钥相同;
(2) 攻击者从协议输出的会话密钥和一个随机值中区分出会话密钥的概率不超过 0.5+ε(ε为一个可
以忽略不计的概率);
2. 完美前向安全 PFS(perfect forward secrecy) [29] :即使已经泄露了用来产生会话密钥的长期密钥,也不会
影响到之前使用的会话密钥的安全性,从而确保了之前通信内容也是安全的.这意味着假设存在一个
敌手能够腐化服务器获得长期私钥,在这之前的会话密钥仍然能够保证安全性,或者导出密钥时不使
用长期密钥,而是使用临时参数完成密钥生成;
3. 抗密钥泄露伪装攻击 KCI(key compromise impersonation):如果参与协议的用户 A 的长期私钥泄露,
则攻击者能够利用 A 的私钥伪装成 A 的身份与其他用户执行协议,而不能伪装成其他用户与 A 成功
完成协议.

1.4 GDH问题
*
*
设 Z 为一乘法群,g 为其生成元,则 Z 上的 CDH,DDH 问题描述如下.
p
p
x
xy
y
(1) CDH 问题:输入 g,g ,g ,输出 g ;
z
xy
z
x
y
(2) DDH 问题:输入 g ,g ,g ,判定 g =g 是否成立.
在此基础上,定义 GDH(gap diffie-hellman)问题 [30] :在假定拥有解决 DDH 问题的有效方法的前提下,求解