eXtended Triple Diffie-Hellman协议的安全性分析

作者：刘佳路; 刘璟^*; **宁; 宋恒贤; 雷欣雨; 陈慧

来源：计算机应用, 2022, 42(S1): 160-165.

• X3DH协议
• 形式化分析工具
• OFMC
• Signal协议

针对X3DH(eXtended Triple Diffie-Hellman)协议安全性的问题，使用形式化分析工具OFMC(On-the-Fly Model-Checker)和协议建模语言AnB对协议进行验证。首先，在Types部分对协议涉及到的通信实体进行了建模；然后，在Knowlegde部分规定了各通信实体的先验知识；其次，在Actions部分对协议的协商流程进行了建模；最后，在Goals部分对协议的机密性、完整性、双向鉴别性等安全目标进行了建模。实验结果表明，X3DH协议作为Signal协议的核心，实现了密钥协商协议所要求的机密性、完整性、双向鉴别性等安全目标，并且形式化分析工具既可以减少工作量，又可以发现人工不易发现的协议漏洞，从而更加全面、高效地验证协议的安全性。

• 单位
  云南大学; 攀枝花学院