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

Modeling and verifying non-repudiation protocols using extended Horn logic

作　　者：徐畅[1] 李舟军[1] 郭华[1] 张帆[1] 

机构地区：[1]北京航空航天大学软件开发环境国家重点实验室,北京100191

出　　处：《清华大学学报（自然科学版）》2012年第10期1488-1495,共8页Journal of Tsinghua University(Science and Technology)

基　　金：国家自然科学基金资助项目(60973105;90718017;61170189);高等学校博士学科点专项科研基金资助项目(20111102130003);软件开发环境国家重点实验室自主研究课题资助项目(SKLSDE-2011ZX-03;SKLSDE-2012ZX-11)

摘　　要：该文首次提出使用Horn逻辑扩展模型验证非否认协议的非否认性和公平性的方法;使用Horn逻辑扩展模型的逻辑规则描述非否认协议中消息的传输过程,并基于Horn逻辑扩展模型对协议的非否认性、公平性进行了建模,同时对参与协议的诚实主体、恶意主体、仲裁进行了建模,提出了针对非否认协议的验证算法;通过使用Horn逻辑扩展模型对Zhou-Gollmann协议进行验证,得到Witness和Request事实并不匹配的结论,说明了Zhou-Gollmann协议并不具有公平性;该文对不动点计算过程进行了优化,通过将规则分为解形式规则和非解形式规则,避免了进行X-消解时对规则的逐条比较。This paper presents a method to verify the non-repudiation property and fairness of a non-repudiation protocol based on an extended Horn logic model.The authors describe the message communications in non-repudiation protocols using the logic rules of the extended Horn logic model,then model the fairness,the non-repudiation property,and the actions of honest users,malicious users and the authorities based on the extended Horn logic model in an algorithm to verify non-repudiation protocols.The authors verify the Zhou-Gollman protocol based on the extended Horn logic model show that Witness facts and Request facts are not matched,and show that the Zhou-Gollman protocol does not provide fairness.For real time operation,the system can not compare with every rule when X-revolution is executed.Thus,the fixed point computation was accelerated by dividing the rules into UnSolvedForm rules and SolvedForm rules.

关 键 词：非否认性 公平性 Horn逻辑扩展模型 解形式不动点 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]