该文首次提出使用Horn逻辑扩展模型验证非否认协议的非否认性和公平性的方法；使用Horn逻辑扩展模型的逻辑规则描述非否认协议中消息的传输过程，并基于 Horn逻辑扩展模型对协议的非否认性、公平性进行了建模，同时对参与协议的诚实主体、恶意主体、仲裁进行了建模，提出了针对非否认协议的验证算法；通过使用Horn逻辑扩展模型对Zhou-Gollmann协议进行验证，得到Witness和 Request事实并不匹配的结论，说明了Zhou-Gollmann协议并不具有公平性；该文对不动点计算过程进行了优化，通过将规则
