基于事件的群组密钥协商协议形式化分析研究

群组密钥协商协议应用于物联网、无线通信、区块链、视频会议等领域，是当前的一个研究热点。该协议的交互消息较多，且消息认证、加密所使用的密码算法也复杂，这就给密码协议的形式化描述与安全性分析带来一定的困难。文章基于串空间理论，提出了相关概念以及基于事件的形式化分析方法。该方法直观、简洁、有效，易于对复杂的密码协议进行形式化描述，并能简化密码协议的安全性分析过程。文章基于事件的形式化分析方法对簇间非对称群组密钥协商协议进行形式化描述和分析，发现该协议不能满足一致性，即不能认证参与协议交互节点的身份。通过对该协议的分析，也证明了文章所提形式化分析方法的有效性与正确性。