[本文摘要]

提出一种密码学可靠的Zhou-Gollmann不可否认协议辅助验证方法。首先建立了计算模型下协议的执行语义模型，构造了一种基于密码学算法的证据伪造攻击。其次，指出目前对协议公平性建模方面的缺陷，并结合辅助工具证明：在加密算法满足选择明文攻击下的不可区分性和明文完整性，且数字签名算法满足选择消息攻击的不可伪造性的条件下，Zhou-Gollmann协议具有公平性和不可否认性。与现有方法相比，既能有效利用辅助工具的自动验证能力，又能弥补其验证能力的不足，提高了验证效率和验证结果的可靠性。