基于Horn扩展逻辑的非否认协议建模与验证研究
非否认协议应该具有非否认性.具体说,消息的发送方不能对其发送过消息进行否认,而消息的接收方不能够对其接收过消息进行否认.此外,非否认协议需要具有公平性,即协议的一方不能够比另一方多以任何优势。本文首先使用Horn逻辑扩展模型的逻辑规则来描述非否认协议中消息的传输过程.我们基于Horn逻辑扩展模型对协议的非否认性、公平性进行建模,对参与协议的诚实主体、恶意主体、仲裁进行建模,提出了具体的针对非否认协议的验证算法.通过对ZG协议进行验证,说明了验证算法的可行性,并在对协议进行验证的过程中,对不动点计算过程进行了优化.
计算机技术 信息安全 逻辑扩展模型 协议验证
徐畅 李舟军 郭华 张帆
北京航空航天大学软件开发环境国家重点实验室,北京100191
国内会议
上海
中文
237-250
2012-12-06（万方平台首次上网日期，不代表论文的发表时间）