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

不可否认协议必须满足存活性、不可否认性、公平性和时限性,但当前大多数形式化方法只能分析该类协议的部分性质,证明或证伪协议逻辑的部分正确性.本文通过向ZQZ逻辑添加时间表达式,提出了一种适用于不可否认协议建模与分析的扩展ZQZ逻辑方法,包括推理规则和安全性质模型.展示新方法的应用时,使用其分析了ZG和KPB这两个局部逻辑正确性已知的两方不可否认协议,以及YLL这个逻辑正确性尚在讨论的基于区块链的多方不可否认协议.实验显示,对前两个协议的分析结果与既有事实相符,对第三个协议的分析发现其无法为收方提供设计者所宣称的时限性.以上结论从逆向工程角度佐证了扩展ZQZ逻辑方法是一种行之有效的不可否认协议分析新方法.

Extended ZQZ Logic Method for Analysis of Non-repudiation Protocols

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.