2021, Vol. 32
2. 信息安全国家重点实验室(中国科学院 信息工程研究所), 北京 100093;
3. 中国科学院大学 网络空间安全学院, 北京 100093
2. State Key Laboratory of Information Security (Institute of Information Engineering, Chinese Academy of Sciences), Beijing 100093, China;
3. School of Cyber Security, University of Chinese Academy of Sciences, Beijing 100093, China
网络安全协议能够解决信息的传输安全问题, 以互联网工程任务组(Internet engineering task force, 简称IETF)为代表的有关组织, 为了弥补基本的TCP/IP协议簇在安全方面的设计缺陷, 对现有的TCP/IP协议簇进行设计和改进, 从而构成了包含多层网络安全协议的TCP/IP协议簇安全架构, 传输层安全协议TLS(transport layer security)就是这个安全架构中重要的组成部分.
TLS协议是在安全套阶层协议SSL(secure socket layer)获得了推广使用之后, 由IETF基于SSL3.0协议[1]制定的正式行业标准[2], TLS1.2[3]为当前大部分浏览器和使用HTTPS协议的Web服务主要使用的版本.然而, 随着网络环境日趋复杂, TLS1.2也开始暴露出越来越多的漏洞, 既有加密算法的漏洞, 如RC4的漏洞[4], 也有协议设计中的漏洞, 如Lucky 13[5]、POODLE[6]、Logjam[7]、三次握手攻击[8], 以及实现过程中的漏洞, 如Heartbleed[9]、状态机攻击[10]等.虽然很多安全漏洞已经通过不定期更新和补丁解决, 但由于TLS庞大的规模以及许多不同的设置, 这些反复的修改增加了TLS的复杂性和部署难度.因此, IETF的TLS工作组开始着手设计“下一代TLS”——TLS1.3.目前, TLS1.3正处于草案阶段[11], 吸引了协议研究者们的广泛关注, 既有针对TLS1.3攻击方法的研究, 如证书转发攻击[12]、中间人攻击[13]、DROWN[14]、Client AuthenticationAttack [15, 16], 也有对TLS1.3的安全性分析和建议, 如OPTLS[17], TLS-Attacker模型[18]等.
为了满足更高的安全需求, 设计开发出更加安全稳定的网络安全协议, 对网络安全协议进行更加严格、可信的分析, 一直以来就是信息安全和密码学领域的一大热点.形式化方法使用数学的方法描述和推理计算机系统, 具有准确的语法以及语义, 并通过精确的数学手段和强大的分析工具实现技术支持.简而言之, 就是规范语言加形式推理[19].形式化方法遍历搜索协议在运行过程中所有可能的状态, 往往能够挖掘出安全协议中难以发现的细微漏洞, 是目前非常流行的安全协议分析方法.
本文参考了Krawczyk等人[17]关于OPTLS的工作, 使用形式化分析工具Scyther分析了CK模型下对Early Data的具体攻击.一方面, Early Data不具有PFS安全, 数据可能被攻击者窃取; 另一方面, Early Data无法抵抗KCI攻击.根据分析结果, 本文对TLS1.3协议进行了优化, 有效提高了协议的安全性.
本文第1节介绍TLS1.3和Syther等预备知识.第2节为使用Scyther工具对TLS1.3协议进行分析的过程和结论.第3节基于TLS1.3中的1-RTT semi-static模式设计一种优化的协议, 在CK安全模型下从安全性证明和形式化分析的角度证明优化协议能够抵抗KCI攻击, 并进行效率分析.第4节对本文的工作进行小结, 进一步明确后续研究方向.
1 预备知识 1.1 Scyther简介Scyther是一款形式化分析安全协议的工具, 该工具由牛津大学的Cremers教授及其团队[20]所开发.这款工具综合运用了定理证明以及模型检测等分析技术, 具有如下特点.
(1) 能够多协议并行分析;
(2) 能够通过无限会话来验证协议;
(3) 能够通过描述协议, 产生所有协议可能行为的有限表示;
(4) 能够通过组合敌手能力构造各种安全模型.
Scyther对协议分析者最友好的一面是其基于按钮的使用界面以及可视化的分析结果, 这使得协议的研究过程能够更加方便和直观.除此之外, Scyther通过控制主体执行轮数和约束状态空间对搜索状态进行双重限制, 与之前仅通过约束状态空间的方法相比, 减少了攻击漏报的可能性, 而且不会因为状态爆炸而出现无分析结果的情况.Scyther的协议形式化语言SPDL简单易学, 尽可能分割我们在安全协议形式化分析中的要点, 即明确区分了协议的静态描述、动态行为以及敌手模型.更进一步讲, 该语言模型实现了多方协议并行运作的直观掌控、安全声明的局部化、局部常量与角色实例的绑定以及初始敌手知识集合的简明定义.
Scyther曾经被用来分析过许多著名协议, 除了Cremers[21, 22]曾经用其分析过IKEv1和IKEv2协议套件和ISO/IEC 9798系列认证协议, Yang和Oleshchuk等人[23, 24]还使用Scyther分析了群认证协议, Ray和Chowdhury等人[25]则使用Scyther分析了物联网协议.该工具最新的版本为Scyther v1.1.3(标准版本, 如果需要支持更多敌手模型, 可以选择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问题设
(1) CDH问题: 输入g, gx, gy, 输出gxy;
(2) DDH问题: 输入gx, gy, gz, 判定gxy=gz是否成立.
在此基础上, 定义GDH(gap diffie-hellman)问题[30]: 在假定拥有解决DDH问题的有效方法的前提下, 求解CDH问题.即: 输入g, gx, gy和一个解决了DDH问题的PPT算法, 输出gxy.
2 TLS1.3协议的形式化分析 2.1 TLS握手协议绝大多数的安全协议都采用了“认证密钥协商+对称加密传输”的结构, TLS也是如此.因此, TLS的主体就是使用对称加密传输信息的记录协议, 以及为记录协议生成双方共享密钥的握手协议.除此之外, TLS还有两个比较简单的辅助协议: 用来报错和安全断连的警告协议和用来通知对方从握手协议切换到记录协议的更改密码规范协议.其中, 后者因为作用不大, 已经在TLS1.3草案中被删除.以上的4个协议构成了图 1的TLS协议分层框架.以TCP为例, 记录协议在TCP流上提供分包, 其他协议都封装在记录协议的包里, 然后在TCP层传输.
|
Fig. 1 TLS protocol stack 图 1 TLS协议栈 |
在TLS的协议栈中, 握手协议是最关键的部分, 也是TLS1.3主要修改的部分.因此, 本文针对TLS1.3的分析主要是对TLS1.3握手协议的分析.对于TLS1.3握手协议的细节, 后面将在第2.3节中进行详细的介绍, 这里只对基本的TLS握手协议流程进行描述.
建立TCP连接之后, 开始进入TLS的握手阶段.在这个阶段, 客户端和服务器交换参数并进行密钥协商, 传统的握手协议流程如图 2所示(图中白底框表示可选的消息, 或者在某些情况可能会发送的消息).
|
Fig. 2 Basic handshake protocol flow 图 2 基本握手协议流程 |
2.2 1-RTT握手和0-RTT数据
TLS1.3在TLS1.2的基础上做了许多重大改进, 比如在记录协议层禁用AEAD之外的其他算法、在握手协议层去除静态RSA和DH密钥协商以及去除更改密码规范协议等等.上述这些改进的目的同之前TLS的升级一样, 都是为了增强TLS的安全性.除此之外, IETF还考虑了一个更现实的问题, 那就是提升协议的运行速度.在互联网普及的今天, Web服务的成功与否与网页加载速度的快慢有着密切联系, Amazon公司曾在实验中发现: 如果网页加载延迟100ms, 销售量就会随之减少1%.而对于服务器在地理位置上相距很远的用户来说, 网络的延迟则更加不能忽略.因此, 人们希望既不牺牲安全性又能够尽量地降低协议的运行时间.针对这一需求, TLS1.3做出了如下改进.
(1) RTT握手支持;
(2) RTT数据支持.
RTT是Round Trip Time的缩写, 即消息的往返时间.对于TLS1.2来说, 完成一次握手需要两个RTT: 第1个是ClientHello和ServerHello, 用于协商密钥交换算法以及各种不同的密码参数; 第2个是ClientKeyExchange和ServerKeyExchange, 也就是使用前一个RTT协商的算法和参数进行密钥交换.TLS1.3为了减少RTT, 决定取消第1个RTT, 让客户端缓存最近服务器使用的算法和参数, 直接使用该缓存的算法和参数, 与服务器进行密钥交换.如果客户端使用的算法和参数错误, 则服务器返回HelloRetryRewuest消息, 告知正确的算法和参数, 让客户端重启握手, 这就是1-RTT握手.该握手方式的可行性来源于TLS1.3对算法的削减, 许多不安全的算法被抛弃, 剩下的密钥协商算法其实只有屈指可数的几种.而可用的密钥协商算法越少, 那么1-RTT握手成功的可能性就越高; 并且即使客户端使用了错误的算法, 也只需要增加一个RTT的代价, 和TLS1.2相比没有增加额外的RTT.这样, TLS1.3基本没有副作用, 便大大降低了TLS握手协议所需要的平均时长.
除了上述的1-RTT握手, TLS1.3还借鉴了Google的QUIC协议[31], 设计了一个0-RTT数据的解决方案.所谓0-RTT, 是指在握手协议的第1条消息中就允许客户端发送一些数据而不必等到握手协议结束.具体的解决方法是: 允许客户端缓存服务器的长期公钥, 在第1条消息中直接利用该长期公钥生成一个会话密钥发送部分应用层数据, 另一部分应用层数据则等到完整的握手协议之后发送.在现实应用中, 对于近期曾经访问过的网站, 用户可以在第1次向服务器发送消息时就带上一部分应用数据, 从而达到提高网页加载速度的目的.
值得注意的是: 0-RTT数据只是在1-RTT握手的基础上添加的数据, 这个数据也被称为Early Data, 握手的其他部分依然保持1-RTT原有的消息.另外, 这些数据不能抵抗重放攻击, 该漏洞可通过一些独立于密钥交换的其他机制解决, 如果想要利用0-RTT机制, 则应该在应用层提供重放保护.
2.3 支持0-RTT数据的模式TLS1.3有3种模式支持0-RTT数据: 1-RTT semi-static, PSK, PSK-DHE.图 3为包含0-RTT数据的消息交互过程, 表 1表示各部分交互消息的意义, 表 2为3种模式所使用的密钥导出表.
|
Fig. 3 Handshake process that contains 0-RTT data flow 图 3 包含0-RTT数据的握手流程 |
|
Table 1 Protocol notation 表 1 符号定义 |
|
|
Table 2 Key derivation table 表 2 密钥导出表 |
由图可知, 客户端Client通过chello消息传递密钥协商的参数, 通过ceks传递密钥协商过程中的临时公钥gx, 并利用服务器的长期公钥加密(或客户端临时私钥和服务器长期公钥计算得出的eadk=gxs)保护Early Data发送给服务器Server, 服务器端接收到消息后, 向客户端Client回复密钥协商的参数shello、临时公钥gy以及用共享密钥gxy保护的消息, 该消息包括服务器的长期公钥和对协议传递消息的确认.
2.3.1 1-RTT semi-static模式首先分析1-RTT semi-static模式.在使用Scyther引擎提供的SPDL语言进行描述时, 为了区别临时私钥和长期私钥, 本文采用在临时密钥生成时加入随机数tempx和tempy的方法, 即用(sk(c), tempx), (sk(s), tempy)表示客户端、服务器的临时私钥, 用g1(sk(c), tempx), g1(sk(s), tempy)表示客户端、服务器的临时公钥.因为tempx和tempy是保密的, 这样在长期私钥被泄露时, 能够保证临时私钥仍然是安全的.此外, 本文使用CK模型作为安全模型, 这种模型允许攻击者显示一方测试会话时的静态私钥(长期私钥)或显示一方的临时私钥, 能帮助敌手获得更强的攻击条件和能力.Scyther工具在Settings标签里面提供了强安全模型的设置面板, 根据Cas Cremers[32, 33]对CK等强安全模型的研究, CK模型允许敌手得知通信方长期私钥和协议执行过程的中间状态, 用以解释CK模型下的前向保密性Long-term Key Reveal after claim(PFS)、密钥泄露伪装攻击Actor(KCI[34])和状态泄露攻击State Reveal.此外, 双方协商的共享密钥还要求抵抗已知会话密钥泄露攻击Session-Key Reveal.因此, 敌手模型的设置如图 4所示.最后点击“Verify automatic claims”进行自动验证, 结果如图 5所示.
|
Fig. 4 Setting attacker model 图 4 设置敌手模型 |
|
Fig. 5 Attack paths of 1-RTT semi-static mode 图 5 1-RTT semi-stati模式的攻击路径 |
从运行结果可以看出: Scyther工具分别在客户端和服务器的角度对协议执行过程中所有参数的机密性进行了验证, 并对双方的双向认证过程中的一致性Niagree和同步性Nisynch进行验证.关于Early Data参数的机密性验证, 结果是不安全的(fail), 分别在客户端和服务器端存在两种攻击, 点击“1 attack”按钮可查看详细的攻击路径, 分别如图 6和图 7所示.此外, Scyther还分析出了一些其他的攻击, 如随机数rc/rs和协议参数negotc/ negots的机密性, 这些参数在协议交互过程中本就是明文通信的, 它们的泄露并不影响认证密钥协商过程的安全性, 所以它们的安全性不在考虑范围之内.而关于认证方面, Niagree和Nisynch所展示的攻击则与图 7中的攻击路径完全相同, 这也说明密钥泄露伪装攻击KCI破坏的是双方的认证安全.
|
Fig. 6 Early Data leaked in 1-RTT semi-static mode 图 6 1-RTT semi-static模式下的Early Data泄露 |
|
Fig. 7 KCI attack in 1-RTT semi-static mode 图 7 1-RTT semi-static模式下的KCI攻击 |
图 6中的攻击描述的是1-RTT semi-static模式下Early Data的泄露过程, 两个run之间交互的路径表示正常的协议交互流程.可以观察到: 在扮演客户端角色的Bob(C)向扮演服务器角色的Alice(S)发送消息M7(即Bob的公钥)时, 敌手可以截获这条消息, 再通过CK模型腐化Alice获得Alice的长期私钥, 从而计算出用于加密Early Data的密钥eadk.这时再截获M11消息, 即可对其中加密的Early Data进行解密.
具体攻击描述如下.
(1) 客户端C与服务器S正常通信, C使用自己的私钥和S中的长期公钥计算出密钥eadk, 用eadk加密在第1条消息中发送的Early Data.此外, C还需要向S发送自己的公钥;
(2) 攻击者A截获C向S发送的C的公钥以及加密后的Early Data密文;
(3) A使用C的公钥和通过腐化参与者获取的S的长期私钥计算出密钥eadk;
(4) A使用eadk解密Early Data, 获得明文.
图 7中的攻击路径描述的是1-RTT semi-static模式下KCI攻击的流程.攻击者在扮演客户端的角色Bob(C)向扮演服务器的角色Alice(S)发送消息M7(即Bob的公钥)时将其截获, 再通过CK模型腐化Alice获得Alice的长期私钥, 从而计算出密钥eadk.此时, 攻击者可以自己伪造一个新的Early Data, 用eadk加密发送给Alice, 则Alice会将这条伪造的消息当作是Bob发送的Early Data, 并继续进行之后正常的协议流程.这样, 攻击者就能够成功冒充Bob向Alice发送消息.
具体攻击描述如下.
(1) 客户端C与服务器S正常通信, C使用自己的私钥和S中的长期公钥计算出密钥eadk, 用eadk加密在第1条消息中发送的Early Data.此外, C还需要向S发送自己的公钥;
(2) 攻击者A截获C向S发送的C的公钥;
(3) A使用C的公钥和通过通过腐化参与者获取的S的长期私钥计算出密钥eadk;
(4) A可以任意伪造Early Data, 使用eadk加密发送给S, S则会认为这条消息来自于C.
综上所述, 根据Scyther分析的结果, 1-RTT semi-static模式下的0-RTT数据存在如下漏洞.
(1) 0-RTT数据没有PFS安全;
(2) 无法抵抗KCI攻击, 即: 如果服务器的长期私钥被攻击者窃取了, 则攻击者可以伪装成任意客户端向服务器发送任意伪造的Early Data.当然, 攻击者拥有服务器的长期私钥, 模拟服务器与客户端通信也是平凡的;
(3) 0-RTT中的数据能够被跨连接重放.
2.3.2 PSK模式如表 2所示, 在PSK模式中, 所有的密钥都由一个预共享密钥psk导出.因此, 在用SPDL语言描述时, 将psk定义为const常量, 表示敌手有获取它的能力.点击“Verify automatic claims”进行自动验证, 得到如图 8所示结果.
|
Fig. 8 Attack paths of PSK mode 图 8 PSK模式的攻击路径 |
从运行结果中可以看出: 如果psk被泄露, 则Early Data和Application Data都将失去安全性, 即二者均没有达到PFS安全的要求.这是由于PSK模式下, 双方没有临时私钥和临时公钥参与密钥协商过程, 在强安全模型下, 整个协议仅使用一个psk导出密钥会导致攻击者能够伪造协议中的任何消息, 包括Finished消息中的MAC, 攻击路径如图 9所示.
|
Fig. 9 MAC forged in PSK mode 图 9 PSK模式下的MAC伪造 |
在该攻击中, 一个已知psk的攻击者可以截获扮演客户端的角色Bob(C)的ClientHello(图中表示为chello)消息, 并伪造一个ServerHello(图中表示为shello)消息返回给Bob; 最后计算出对应的MAC, 加密发送给Bob, 其中, 计算MAC的密钥sfk和握手密钥htk都由psk导出.
具体攻击描述如下.
(1) 攻击者A通过一定方法获取客户端C与服务器S的预共享密钥psk;
(2) A劫持C与S的会话, 拦截所有C向S发送的消息;
(3) A伪造一个ServerHello消息返回给C;
(4) A使用psk计算一个MAC, MAC的内容包括C发送的ClientHello消息、A伪造的ServerHello消息以及psk的值;
(5) A将MAC用psk加密发送给C, 完成1-RTT握手, 伪装成服务器与C建立会话.
可以说, 这种模式的安全性完全取决于psk的保密性, 一旦psk被攻击者获取, 整个协议流程都将变得极其不安全.
2.3.3 PSK-DHE模式PSK-DHE在PSK模式的基础上增加了一轮DH交换, 使Application Data满足PFS安全的要求.为了区分临时私钥和长期私钥, 采用与第2.3.1节相同的方式表示客户端与服务器的临时私钥.运行结果如图 10所示.
|
Fig. 10 Attack paths of PSK-DHE mode 图 10 PSK-DHE模式的攻击路径 |
从图 10中可以看出: Data的Secret属性为OK, 即Application Data满足PFS安全.由于PSK-DHE模式的架构与1-RTT semi-static模式类似, 只是把使用服务器长期密钥进行的一轮DH交换改为使用预共享密钥机制, 因此可以看到: PSK-DHE模式中, Early Data的安全性类似1-RTT semi-static模式, 仍然没有达到PFS安全, 也不能抵抗KCI攻击.攻击路径如图 11(a)和图 11(b)所示, 攻击流程与1-RTT semi-static模式下攻击相同.
|
Fig. 11 Early Data leaked and KCI attack in PSK-DHE mode 图 11 PSK-DHE模式下的Early Data泄露和KCI攻击 |
3 优化协议方案
从上述结果可以看出: 对于一个能够获取服务器长期私钥的敌手来说, 0-RTT数据将变得不再安全.事实上, 这一问题对于Google的QUIC协议同样存在, 但是因为QUIC协议主要应用在谷歌浏览器上, 在访问网站时, 通常使用GET作为建立连接的第1个请求, 所以0-RTT中的数据敏感性可能并不是很高, 故其安全性可以选择忽视.然而对于使用POST作为第1个请求的连接, 比如微信的短连接, 发送给服务器端的都是上层安全性要求很高的业务数据, 在这种情况下, 0-RTT数据的安全问题必须考虑.对此, 服务器长期私钥对应的公钥其缓存时间必须严格限制.通常, 服务器通过ServerConfiguration消息将长期公钥发送给客户端.ServerConfiguration的数据结构如下.
| $ \begin{array}{l}\begin{array}{l}\rm{struct }\{ \\ \rm{\hspace{1em}}\rm{\hspace{1em}}\rm{opaque configuration\_id }\langle 1, \mathrm{...}, 2^16-1\rangle ; \\ \rm{\hspace{1em}}\rm{\hspace{1em}}u\mathrm{int}32\rm{ expiration\_date}; \\ \rm{\hspace{1em}}\rm{\hspace{1em}}\rm{NamedGroup group}; \\ \rm{\hspace{1em}}\rm{\hspace{1em}}\rm{opaque server\_key }\langle 1, \mathrm{...}, 2^16-1\rangle ; \\ \rm{\hspace{1em}}\rm{\hspace{1em}}\rm{EarlyDataType early\_data\_type}; \\ \rm{\hspace{1em}}\rm{\hspace{1em}}\rm{ConfigurationExtension extensions }\langle 1, \mathrm{...}, 2^16-1\rangle ; \end{array}\\ \}\rm{ ServerConfiguration};\end{array}$ |
其中, expiration_date就是该ServerConfiguration的有效使用期限, 被设定为小于7天.也就是说, 客户端缓存服务器半静态公钥的时间不得超过7天.
3.1 优化协议的结构从ServerConfiguration的有效使用期限可以看出, 客户端需要频繁地缓存半静态公钥.这对于握手协议的效率来说造成了一定的影响, 并且也无法从根本上解决0-RTT数据的安全性问题.关于0-RTT数据的安全性问题, 根据第2节中形式化分析的结果, 主要包括没有PFS安全和无法抵抗KCI攻击.本文基于1-RTT semi-static模式设计了一种新的支持0-RTT数据的协议, 该协议可以有效抵抗KCI攻击, 提高了0-RTT数据的安全性.协议的消息交互过程如图 12所示, 由图可见: 相比原协议传输, 优化后的协议在原Early Data消息的基础上, 添加了客户端对Early Data和时间戳的签名.
|
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攻击.
● 正确性
假设一个诚实的协议参与者拥有抗重放机制来产生chello, 那么chello唯一识别ceks=gs.也就是说, 对于一对匹配的会话, 协议双方的chello, ceks, ssks都相同, 因此计算出相同的eadk.
● 安全性
接下来定义一系列Game.
(1) Game 0:优化协议的真实执行过程;
(2) Game 1:服务器证书不可伪造.游戏规则与Game 0相同, 在该游戏中, 攻击者使用随机值ssks*代替gs, 因为签名或者其他任何用于认证ssks的方案是安全的, 因此攻击者无法赢得Game 1.也就是说, 攻击者不能随意伪造服务器的证书;
(3) Game 2:eadk的安全性.该游戏发生在s被泄露之前, 游戏规则与Game 0相同, 但是攻击者不能使用party corruption查询.在该游戏中, 攻击者查询gxs, 或者从随机值和gxs中区分出gxs.根据Gap-DH困难性假设: 在给出g, gx, gs和DDH查询的前提下, 计算gxs是困难的.即, 攻击者赢得Game 2的概率等同于求解Gap-DH难题;
(4) Game 3:eadk的安全性.该游戏发生在s被泄露之前, 游戏规则与Game 0相同, 但是攻击者不能使用party corruption查询.在该游戏中, 攻击者在一个会话完成后, 用随机值代替另一个会话的eadk*.因为密钥导出函数是安全的.
➢ 对eadk的session-key query查询不影响eadk*, 因为chello*≠chello;
➢ atk, sfk甚至atk*的泄露, 都不会影响eadk*.
因此, 攻击者无法赢得Game 3.
(5) Game 4:Earlydata的真实性和可靠性.该游戏规则与Game 0相同, 攻击者在该游戏中用随机值代替Sigsk(c)(Hash(Earlydata)).因为用于签名Earlydata的密钥sk(c)和算法是安全的, 所以攻击者无法赢得Game 4.也就是说, 攻击者可以通过party corruption使s泄露, 并计算出eadk, 进一步得到Earlydata的内容, 但是伪造Sigsk(c)(Hash(Earlydata))是困难的, 因此保证了Early Data消息来源的真实性和可靠性.
综上所述, 优化协议能够防止攻击者伪装成任意客户端伪造Early Data消息, 从而有效抵抗KCI攻击.
3.3 优化协议的形式化分析利用Scyther工具对优化后的协议进行分析, 这里在编写形式化语言时需要特别注意对签名密钥的描述.
签名的公私钥对必须具备两条基本属性.
(1) 在CK模型下用于签名的私钥仍然是保密的;
(2) 签名的公钥是公开的.
因为Scyther对于角色C来说只有一个私钥就是sk(c), 为了区分临时私钥和长期私钥, 之前在第2.3.1节中提到了在sk(c)后加一个随机数的解决方案, 也就是用(sk(c), sigx)的形式来表示签名密钥(sigx为随机数).但是这里因为公钥是公开的, 那么也就是说敌手必须要知道(pk(c), sigx), 而pk(c)是已知的, 所以这种表达方式会让敌手得到sigx, 再加上设置了CK模型的前提下, C的私钥sk(c)也是已知的, 那么(sk(c), sigx)同样能够被敌手得知.因此, 本文使用sk(c, sigx)来表示签名私钥.经过实验证明: 在敌手已知pk(c, sigx)和pk(c), 并且设置CK模型使得sk(c)也是不安全的前提下, sk(c, sigx)仍然是安全的.
根据之前的实验发现: 使用“Verify automatic claims”会分析出很多不影响实验结果的攻击路径, 不仅降低了工具的分析效率, 而且很多攻击路径对实验也没有帮助, 因此, 针对性地在SPDL语言中加入claim语句.
● claim(c, Secret, Earlydata);
● claim(s, Secret, Earlydata);
● claim(s, Niagree);
● claim(s, Nisynch);
在搜索攻击的设置选项里, 选择“Find all attacks”而不是“Find best attack”, 以防漏报.观察运行结果, 发现所有的攻击路径描述的都是同一种攻击, 如图 13所示.
|
Fig. 13 Raplay attack to Early Data in the optimized protocol 图 13 优化协议中Early Data的重放攻击 |
在一次运行过程中, 攻击者截获客户端Bob(C)的公钥并腐化服务器Alice(S)得到其长期私钥, 计算出这一次通信的eadk, 从而得到Early Data和对应的签名; 在另一次运行过程时, 攻击者可以将这两条消息作为0-RTT里面的数据, 用这一次通信的eadk加密发送给客户端Bob, 完成对Early Data的重放攻击.
具体攻击如下.
(1) 客户端C与服务器S正常通信, C使用此次通信C的私钥和S的长期公钥计算出密钥eadk, 用eadk加密在第1条消息中发送的Early Data以及Early Data摘要的签名; 此外, C还需要向S发送此次通信C的公钥;
(2) 攻击者A截获C向S发送的此次通信C的公钥以及加密后的Early Data和Early Data摘要的签名;
(3) A使用C此次通信的公钥和通过腐化参与者获取的S的长期私钥计算出加密此次通信的eadk;
(4) A使用eadk解密获得Early Data和Early Data摘要的签名;
(5) 在C和S的另一次通信中, A可以用步骤(4)中获得的Early Data和Early Data摘要的签名替换本次通信中的Early Data和Early Data摘要的签名, 完成消息的重放.
对比1-RTT semi-static模式中claim(s, Niagree)所描述的KCI攻击(如图 14所示)可以发现: 优化协议中, 攻击者发送的Early Data数据仍然为合法客户端所发送的数据, 攻击者只能够对其简单重放; 而1-RTT semi-static模式中的Early Data数据为IntruderString, 即攻击者自己定义的消息, 在这种情况下, 攻击者不仅可以重放消息, 甚至可以对重放的消息进行任意篡改, 其风险显然远大于优化协议中的重放攻击.
|
Fig. 14 KCI attack in 1-RTT semi-static mode 图 14 1-RTT semi-static模式下的KCI攻击 |
综上所述, 相比之前的1-RTT semi-static模式, 该优化协议能够有效抵抗KCI攻击, 验证了之前的证明结果. PSK-DHE模式与1-RTT semi-static模式类似, 同样可以运用该优化协议的思路, 在Early Data上加一层签名, 即可保证0-RTT中的数据能够抵抗KCI攻击.表 3总结了1-RTT semi-static模式和优化协议的安全性对比.
|
|
Table 3 Security comparison 表 3 安全性对比 |
可以看出: 优化协议有效提高了0-RTT数据的安全性, 防止了攻击者冒充合法用户与服务器建立非法链接.对于重放攻击的问题, 在签名中添加时间戳, 有效防止了敌手对时间戳的篡改和伪造, 服务器通过对时间戳的验证实现了抗重放机制.
3.4 优化协议的效率分析为了分析优化协议的效率, 表 4对比了1-RTT semi-static模式和优化协议所需要的主要密码工具.
|
|
Table 4 Main password tools comparison 表 4 主要密码工具对比 |
从表中可以看出: 优化协议与1-RTT semi-static模式相比, 多使用了一个签名(在传输服务器的长期公钥证书的时候还需要另一个签名, 这个签名是二者都必需的), 并且为Early Data增加一个签名没有增加发送的消息数, 仍然在0-RTT发出, 因此不会增加协议的运行时间.此外, 增加的签名也不会影响到其他消息, 特别是Finished消息, 因为签名的数据不包括在MAC的内容中, 因此不会影响到MAC的计算效率.需要注意的是: 优化协议使用的签名算法建议采用固定的算法, 这样就不需要再增加chello消息中协议参数的内容, 从而防止增加MAC计算的内容.
综上所述, 优化协议只增加了一个签名的代价, 对于现代计算机的处理速度以及网络的传输速度来说, 这个代价是非常小的, 然而换来的却是能够抵抗KCI攻击的安全性提升.
4 结束语针对TLS1.3协议中3种支持0-RTT数据的模式, 本文使用形式化分析工具Scyther对其进行了分析, 找到了0-RTT数据的泄露和KCI攻击两种攻击, 进一步提出了一种优化协议, 该优化协议相比原来的3种模式能够抵抗KCI攻击和重放攻击, 通过增加一个签名的微小代价, 有效提高了0-RTT数据的安全性, 特别在使用POST作为第1个请求的连接时, 这样的安全性提升是必要的.
| [1] |
Freier A, Karlton P, Kocher P. The secure sockets layer (SSL) protocol version 3.0. IETF RFC-6101, 2011.
|
| [2] |
Dierks T, Allen C. The TLS protocol version 1.0. IETF RFC-2246, 1999.
|
| [3] |
Dierks T, Rescorla E. The transport layer security (TLS) protocol version 1.2. IETF RFC-5246, 2008.
|
| [4] |
Alfardan N, Bernstein D, Paterson K, et al. On the security of RC4 in TLS. In: Proc. of the Usenix Conf. on Security. USENIX Association, 2013. 305-320.
|
| [5] |
Fardan N, Paterson K. Lucky thirteen: Breaking the TLS and DTLS record protocols. In: Proc. of the IEEE Symp. on Security & Privacy. IEEE Computer Society, 2013. 526-540.
|
| [6] |
Möller B, Duong T, Kotowicz K. This POODLE bites: Exploiting the SSL 3.0 fallback. Security Advisory, 2014.
|
| [7] |
Adrian D, Bhargavan K, Durumeric Z, et al. Imperfect forward secrecy: How diffie-hellman fails in practice. In: Proc. of the ACM Sigsac Conf. on Computer and Communications Security. ACM, 2015. 5-17.
|
| [8] |
Bhargavan K, Lavaud A, Fournet C, et al. Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS. In: Proc. of the IEEE Symp. on Security & Privacy. IEEE Computer Society, 2014. 98-113.
|
| [9] |
Gujrathi S. Heartbleed bug: An OpenSSL heartbeat vulnerability. Int'l Journal of Computer Sciences and Engineering, 2014, 2(5): 61-64.
|
| [10] |
Beurdouche B, Bhargavan K, Delignat-Lavaud A, et al. A messy state of the union: taming the composite state machines of TLS. In: Proc. of the IEEE Symp. on Security & Privacy, 2015. 535-552.
|
| [11] |
Rescorla E. The transport layer security (TLS) protocol version 1.3. IETF draft-ietf-tls-tls13-20, 2017.
|
| [12] |
Bhargavan K, Leurent G. Transcript collision attacks: breaking authentication in TLS, IKE and SSH. British Journal of Psychiatry the Journal of Mental Science, 2016, 41(7): 8-13.
http://www.researchgate.net/publication/316906828_Transcript_Collision_Attacks_Breaking_Authentication_in_TLS_IKE_and_SSH |
| [13] |
Jager T, Schwenk J, Somorovsky J. On the security of TLS 1.3 and QUIC against weaknesses in PKCS#1 v1.5 encryption. In: Proc. of the ACM Sigsac Conf. on Computer and Communications Security. ACM, 2015. 1185-1196.
|
| [14] |
Paar C, Adrian D, Kasper E, et al. DROWN: Breaking TLS using SSLv2. In: Proc. of the Usenix Security Symp. USENIX Association, 2016. 689-706.
|
| [15] |
Cremers C, Horvat M, Hoyland J, et al. A comprehensive symbolic analysis of TLS 1.3. In: Proc. of the 2017 ACM SIGSAC Conf. on Computer and Communications Security. ACM, 2017. 1773-1788.
|
| [16] |
Bhargavan K, Blanchet B, Kobeissi N. Verified models and reference implementations for the TLS 1.3 standard candidate. In: Proc. of the 2017 IEEE Symp. on Security and Privacy (SP). IEEE, 2017. 483-502.
|
| [17] |
Krawczyk H, Wee H. The OPTLS protocol and TLS1.3. In: Proc. of the IEEE Symp. on Security & Privacy. IEEE Computer Society, 2016. 81-96.
|
| [18] |
Somorovsky J. Systematic fuzzing and testing of TLS libraries. In: Proc. of the ACM Sigsac Conf. on Computer and Communications Security. ACM, 2016. 1492-1504.
|
| [19] |
Xue R, Feng DG. The approaches and technologies for formal verification of security protocols. Chinese Journal of Computers, 2006, 29(1): 1-20(in Chinese with English abstract).
[doi:10.3321/j.issn:0254-4164.2006.01.001] |
| [20] |
Cremers C. Scyther: Semantics and verification of security protocols. Netherlands: Eindhoven University of Technology, 2006.
|
| [21] |
Cremers C. Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2. In: Proc. of the European Symp. on Research in Computer Security (ESORICS 2011). Berlin: Springer-Verlag, 2011. 315-334.
|
| [22] |
Basin D, Cremers C, Meier S. Provably repairing the ISO/IEC 9798 standard for entity authentication. Journal of Computer Security, 2013, 21(6): 817-846.
[doi:10.3233/JCS-130472] |
| [23] |
Yang H, Prinz A, Oleshchuk V. Formal analysis and model checking of a group authentication protocol by Scyther. In: Proc. of the Euromicro Int'l Conf. on Parallel, Distributed, and Network-based Processing. IEEE Computer Society, 2016. 553-557.
|
| [24] |
Yang H, Oleshchuk V, Prinz A. Verifying group authentication protocols by scyther. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA), 2016, 7(2): 3-19.
http://doi.ieeecomputersociety.org/10.1109/PDP.2016.27 |
| [25] |
Ray B, Chowdhury M, Abawajy J. Secure object tracking protocol for the Internet of things. IEEE Internet of Things Journal, 2016, 3(4): 1-10.
[doi:10.1109/JIOT.2016.2591763] |
| [26] |
Meier S, Cremers C, Basin D. Strong invariants for the efficient construction of machine-checked protocol security proofs. In: Proc. of the IEEE Computer Security Foundations Symp. IEEE Computer Society, 2010. 231-245.
|
| [27] |
Meier S, Schmidt B, Cremers C, et al. The TAMARIN prover for the symbolic analysis of security protocols. In: Proc. of the Int'l Conf. on Computer Aided Verification. Berlin: Springer-Verlag, 2013. 696-701.
|
| [28] |
Canetti R, Krawczyk H. Analysis of key-exchange protocols and their use for building secure channels. In: Proc. of the Advances in Cryptology (EUROCRYPT 2001). Berlin: Springer-Verlag, 2001. 453-474.
|
| [29] |
Günther C. An identity-based key-exchange protocol. In: Proc. of the Workshop on the Theory and Application of of Cryptographic Techniques. Berlin: Springer-Verlag, 1989. 29-37.
|
| [30] |
Cha J, Cheon J. An identity-based signature from gap diffie-hellman groups. In: Proc. of the Int'l Workshop on Theory and Practice in Public Key Cryptography: Public Key Cryptography. Berlin: Springer-Verlag, 2002. 18-30.
|
| [31] |
Fischlin M, Günther F. Multi-stage key exchange and the case of Google's QUIC protocol. In: Proc. of the 2014 ACM SIGSAC Conf. on Computer and Communications Security. ACM, 2014. 1193-1204.
|
| [32] |
Cremers C. Formally and practically relating the CK, CK-HMQV, and eCK security models for authenticated key exchange. Cryptology Eprint Archive, 2009.
http://www.researchgate.net/publication/220334325_Formally_and_Practically_Relating_the_CK_CK-HMQV_and_eCK_Security_Models_for_Authenticated_Key_Exchange |
| [33] |
Cremers C. Examining indistinguishability-based security models for key exchange protocols: The case of CK, CK-HMQV, and eCK. In: Proc. of the ACM Symp. on Information, Computer and Communications Security. ACM, 2011. 80-91.
|
| [34] |
Gorantla M, Boyd C, Nieto J. Modeling key compromise impersonation attacks on group key exchange protocols. ACM Trans. on Information & System Security, 2009, 14(4): 1-24.
http://dl.acm.org/citation.cfm?id=2043629 |
| [19] |
薛锐, 冯登国. 安全协议的形式化分析技术与方法. 计算机学报, 2006, 29(1): 1-20.
[doi:10.3321/j.issn:0254-4164.2006.01.001] |