典型文献
不可否认协议分析的扩展ZQZ逻辑方法
文献摘要：
不可否认协议必须满足存活性、不可否认性、公平性和时限性,但当前大多数形式化方法只能分析该类协议的部分性质,证明或证伪协议逻辑的部分正确性.本文通过向ZQZ逻辑添加时间表达式,提出了一种适用于不可否认协议建模与分析的扩展ZQZ逻辑方法,包括推理规则和安全性质模型.展示新方法的应用时,使用其分析了ZG和KPB这两个局部逻辑正确性已知的两方不可否认协议,以及YLL这个逻辑正确性尚在讨论的基于区块链的多方不可否认协议.实验显示,对前两个协议的分析结果与既有事实相符,对第三个协议的分析发现其无法为收方提供设计者所宣称的时限性.以上结论从逆向工程角度佐证了扩展ZQZ逻辑方法是一种行之有效的不可否认协议分析新方法.
文献关键词：
不可否认协议;形式化分析;ZQZ逻辑;时限性;时间表达式;逆向工程
中图分类号：
作者姓名：
韩志耕;石青山;杨鹏;陈耿;范远哲
作者机构：
南京审计大学 信息工程学院, 南京 211815;江苏省审计信息工程重点实验室 (南京审计大学), 南京 211815
文献出处：
引用格式：
[1]韩志耕;石青山;杨鹏;陈耿;范远哲-.不可否认协议分析的扩展ZQZ逻辑方法)[J].密码学报,2022(01):60-75
A类：
不可否认协议,ZQZ,KPB
B类：
协议分析,逻辑方法,不可否认性,公平性,时限性,形式化方法,证伪,添加时间,时间表达式,建模与分析,推理规则,ZG,YLL,个协,有事,实相,第三个,收方,设计者,宣称,逆向工程,佐证,形式化分析
AB值：
0.236518
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
