3X协议一致性测试组织研究与设计

协议一致性测试是验证计算机网络协议实现与其国际标准是否一致的关键技术。３Ｘ协议是公用分组交换数据网中一组应用十分广泛的协议标准，对其进行一致性测试是十分重要的。本文首先对３Ｘ协议及其应用进行介绍，然后从测试角度对被测系统进行分析。

IDACOM3X协议一致性测试集的研究与分析

在计算机网络协议一致性测试中，形式化技术是一种重要的理论发展方向。本文在介绍形式化的测试集描述技术的基础上，对加拿大ＩＤＡＣＯＭ的３Ｘ协议一致性测试集进行了分析，指出它在形式化方面的不足和改进的方向。

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

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