基于事件逻辑的改进型Helsinki协议的形式化分析

来源：计算机应用与软件杂志2026年第1期北京时间：

作者：肖美华，罗运先，钟小妹, ,

摘要：安全协议是现代网络通信的基础，证明协议的安全性问题是当今研究热点之一。事件逻辑是一种基于事件系统证明协议安全属性的形式化方法，结合事件类以及事件序语言，利用原子类型表示随机数、密钥等不可猜测的数据，能有效刻画协议系统。针对改进型Helsinki协议的安全性问题，对事件逻辑扩充谓词Fresh和FirstSend及其推理规则，利用扩充后的事件逻辑对协议进行形式化分析，首先对协议构建基本序列，然后通过事件逻辑对协议的认证性以及秘密性进行形式化规约，最后利用公理系统和推理规则证明改进型Helsinki协议满足认证性和秘密性。结果表明事件逻辑理论能有效证明安全协议的认证性和秘密性。

关键词：安全协议, 事件逻辑, 形式化方法, Helsinki协议