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

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

由图可知,客户端 Client 通过 chello 消息传递密钥协商的参数,通过 ceks 传递密钥协商过程中的临时公钥
x
xs
g ,并利用服务器的长期公钥加密(或客户端临时私钥和服务器长期公钥计算得出的 eadk=g )保护 Early Data 发
y
送给服务器 Server,服务器端接收到消息后,向客户端 Client 回复密钥协商的参数 shello、临时公钥 g 以及用共
xy
享密钥 g 保护的消息,该消息包括服务器的长期公钥和对协议传递消息的确认.
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 Fig.5 Attack paths of 1-RTT semi-static mode
图 4 设置敌手模型 图 5 1-RTT semi-stati 模式的攻击路径

从运行结果可以看出:Scyther 工具分别在客户端和服务器的角度对协议执行过程中所有参数的机密性进
行了验证,并对双方的双向认证过程中的一致性 Niagree 和同步性 Nisynch 进行验证.关于 Early Data 参数的机
密性验证,结果是不安全的(fail),分别在客户端和服务器端存在两种攻击,点击“1 attack”按钮可查看详细的攻击
路径,分别如图 6 和图 7 所示.此外,Scyther 还分析出了一些其他的攻击,如随机数 rc/rs 和协议参数 negotc/ negots
的机密性,这些参数在协议交互过程中本就是明文通信的,它们的泄露并不影响认证密钥协商过程的安全性,所
以它们的安全性不在考虑范围之内.而关于认证方面,Niagree 和 Nisynch 所展示的攻击则与图 7 中的攻击路径
完全相同,这也说明密钥泄露伪装攻击 KCI 破坏的是双方的认证安全.