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

作     者：韩志耕 石青山 杨鹏 陈耿 范远哲 HAN Zhi-Geng;SHI Qing-Shan;YANG Peng;CHEN Geng;FAN Yuan-Zhe

作者机构：南京审计大学信息工程学院南京211815 江苏省审计信息工程重点实验室(南京审计大学)南京211815 

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

出 版 物：《密码学报》 (Journal of Cryptologic Research)

年 卷 期：2022年第9卷第1期

页      码：60-75页

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

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

学科分类：0839[0839] 08[工学] 081201[081201] 0812[工学-测绘类] 

核心收录：

D　O　I：10.13868/j.cnki.jcr.000503

馆 藏 号：203108284...