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

2862 Journal of Software 软件学报 Vol.32, No.9, September 2021

密钥导出函数是安全的.
*
*
¾ 对 eadk 的 session-key query 查询不影响 eadk ,因为 chello ≠chello;
*
*
¾ atk,sfk 甚至 atk 的泄露,都不会影响 eadk .
因此,攻击者无法赢得 Game 3.
(5) Game 4:Earlydata 的真实性和可靠性.该游戏规则与 Game 0 相同,攻击者在该游戏中用随机值代替
Sig sk(c) (Hash(Earlydata)).因为用于签名 Earlydata 的密钥 sk(c)和算法是安全的,所以攻击者无法赢得
Game 4.也就是说,攻击者可以通过 party corruption 使 s 泄露,并计算出 eadk,进一步得到 Earlydata 的
内容,但是伪造 Sig sk(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 所示.
在一次运行过程中,攻击者截获客户端 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 摘要的签名,完成消息的重放.