不可否认协议分析的扩展ZQZ逻辑方法OACSTPCD
不可否认协议必须满足存活性、不可否认性、公平性和时限性,但当前大多数形式化方法只能分析该类协议的部分性质,证明或证伪协议逻辑的部分正确性.本文通过向ZQZ逻辑添加时间表达式,提出了一种适用于不可否认协议建模与分析的扩展ZQZ逻辑方法,包括推理规则和安全性质模型.展示新方法的应用时,使用其分析了ZG和KPB这两个局部逻辑正确性已知的两方不可否认协议,以及YLL这个逻辑正确性尚在讨论的基于区块链的多方不可否认协议.实验显示,对前两个协议的分析结果与既…查看全部>>
韩志耕;石青山;杨鹏;陈耿;范远哲
南京审计大学信息工程学院,南京211815 江苏省审计信息工程重点实验室(南京审计大学),南京211815南京审计大学信息工程学院,南京211815 江苏省审计信息工程重点实验室(南京审计大学),南京211815南京审计大学信息工程学院,南京211815 江苏省审计信息工程重点实验室(南京审计大学),南京211815南京审计大学信息工程学院,南京211815 江苏省审计信息工程重点实验室(南京审计大学),南京211815南京审计大学信息工程学院,南京211815 江苏省审计信息工程重点实验室(南京审计大学),南京211815
信息技术与安全科学
不可否认协议形式化分析ZQZ逻辑时限性时间表达式逆向工程
《密码学报》 2022 (1)
P.60-75,16
评论