基于Horn扩展逻辑的非否认协议建模与验证

作者：徐畅; 李舟军; 郭华; 张帆

来源：清华大学学报(自然科学版), 2012, (10): 1488-1495.

DOI：10.16511/j.cnki.qhdxxb.2012.10.026

• 非否认性
• 公平性
• Horn逻辑扩展模型
• 解形式不动点 non-repudiation
• fairness
• extended Horn logic model
• solved-form fixed point

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

• 单位
  北京航空航天大学; 软件开发环境国家重点实验室