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

Security analysis of eXtended Triple Diffie-Hellman protocol

作　　者：刘佳路 刘璟 杨佳宁[1,2] 宋恒贤 雷欣雨 陈慧 LIU Jialu;LIU Jing;YANG Jianing;SONG Hengxian;LEI Xinyu;CHEN Hui(School of Software,Yunnan University,Kunming Yunnan 650504,China;Engineering Research Center of Cyberspace(Yunnan University),Kunming Yunnan 650504,China;School of Mathematics and Computers,Panzhihua University,Panzhihua Sichuan 617000,China)

机构地区：[1]云南大学软件学院,昆明650504 [2]跨境网络安全教育部工程研究中心(云南大学),昆明650504 [3]攀枝花学院数学与计算机学院,四川攀枝花617000

出　　处：《计算机应用》2022年第S01期160-165,共6页journal of Computer Applications

基　　金：国家自然科学基金资助项目(61363084)。

摘　　要：针对X3DH(eXtended Triple Diffie-Hellman)协议安全性的问题,使用形式化分析工具OFMC(On-the-Fly Model-Checker)和协议建模语言AnB对协议进行验证。首先,在Types部分对协议涉及到的通信实体进行了建模;然后,在Knowlegde部分规定了各通信实体的先验知识;其次,在Actions部分对协议的协商流程进行了建模;最后,在Goals部分对协议的机密性、完整性、双向鉴别性等安全目标进行了建模。实验结果表明,X3DH协议作为Signal协议的核心,实现了密钥协商协议所要求的机密性、完整性、双向鉴别性等安全目标,并且形式化分析工具既可以减少工作量,又可以发现人工不易发现的协议漏洞,从而更加全面、高效地验证协议的安全性。To verify the security of X3DH(eXtended Triple Diffie-Hellman)protocol,a formal analysis tool called OFMC(On-the-Fly Model-Checker)and protocol modeling language AnB were proposed.Firstly,in the Types part,the communication entities involved in the protocol were modeled.Then,in the Knowlegde part,the prior knowledge of each communication entity was specified.Secondly,in the Actions part,the negotiation process of the protocol was modeled.Finally,in the Goals part,the security objectives such as confidentiality,integrity,and two-way authentication of the protocol were modeled.The experimental results show that as the core of the Signal protocol,X3DH(Extended Triple Diffie-Hellman)protocol realizes the security goals of confidentiality,integrity,and two-way authentication required by the key agreement protocol are realized.And formal analysis tools can reduce the workload and find protocol vulnerabilities that are not easy to find by humans.Analysis tools can verify the security of the protocol more comprehensively and efficiently.

关 键 词：X3DH协议 形式化分析工具 OFMC Signal协议 

分 类 号：TP309.7[自动化与计算机技术—计算机系统结构]