不可否认协议分析的扩展ZQZ逻辑方法  

Extended ZQZ Logic Method for Analysis of Non-repudiation Protocols

作　　者：韩志耕 石青山[1,2] 杨鹏 陈耿 范远哲[1,2] HAN Zhi-Geng;SHI Qing-Shan;YANG Peng;CHEN Geng;FAN Yuan-Zhe(School of Information Engineering,Nanjing Audit University,Nanjing 211815,China;Jiangsu Key Laboratory of Audit Information Engineering(Nanjing Audit University),Nanjing 211815,China)

机构地区：[1]南京审计大学信息工程学院,南京211815 [2]江苏省审计信息工程重点实验室(南京审计大学),南京211815

出　　处：《密码学报》2022年第1期60-75,共16页Journal of Cryptologic Research

基　　金：国家自然科学基金(72072091);江苏省高校自然科学基金(21KJA520002,16KJB520021);审计信息工程与技术协同创新中心项目。

摘　　要：不可否认协议必须满足存活性、不可否认性、公平性和时限性,但当前大多数形式化方法只能分析该类协议的部分性质,证明或证伪协议逻辑的部分正确性.本文通过向ZQZ逻辑添加时间表达式,提出了一种适用于不可否认协议建模与分析的扩展ZQZ逻辑方法,包括推理规则和安全性质模型.展示新方法的应用时,使用其分析了ZG和KPB这两个局部逻辑正确性已知的两方不可否认协议,以及YLL这个逻辑正确性尚在讨论的基于区块链的多方不可否认协议.实验显示,对前两个协议的分析结果与既有事实相符,对第三个协议的分析发现其无法为收方提供设计者所宣称的时限性.以上结论从逆向工程角度佐证了扩展ZQZ逻辑方法是一种行之有效的不可否认协议分析新方法.Non-repudiation protocols must satisfy liveness,non-repudiation,fairness and timeliness.However,most formal methods can only analyze some properties of them,and prove or disprove the partial correctness of the logics.With adding time expression to ZQZ logic,this paper proposes an extended ZQZ logic method with reasoning rules and security property models for modeling and analysing non-repudiation protocols.Furthermore,the proposed logic is used to analyze the two-party non-repudiation protocols ZG and KPB,with known partial logic correctness,and a new blockchain based multi-party non-repudiation protocol YLL,whose logic correctness is still under discussion.Experiments show that the analysis results of the first two protocols are consistent with the accepted facts,and the analysis of the third protocol finds that it cannot provide the recipient with timeliness as claimed by the protocol designer.The results show from the perspective of reverse engineering that,the proposed method is an effective new method for analysis of non-repudiation protocols.

关 键 词：不可否认协议 形式化分析 ZQZ逻辑 时限性 时间表达式 逆向工程 

分 类 号：TP309.7[自动化与计算机技术—计算机系统结构]