计算机科学 ›› 2018, Vol. 45 ›› Issue (7): 143-149.doi: 10.11896/j.issn.1002-137X.2018.07.024

• 信息安全 • 上一篇    下一篇

一种可靠的多方不可否认协议的逻辑分析方法

苑博奥,刘军   

  1. 陆军工程大学指挥信息系统学院 南京210007
  • 收稿日期:2017-05-29 出版日期:2018-07-30 发布日期:2018-07-30
  • 作者简介:苑博奥(1992-),男,硕士生,主要研究方向为安全协议、信息安全,E-mail:yuanboao1201@sina.com;刘 军(1969-),男,教授,主要研究方向为信息安全、软件工程,E-mail:13914735588@139.com(通信作者)。

Reliable Logic Analysis Method of Multi-party Non-repudiation Protocol

YUAN Bo-ao, LIU Jun   

  1. College of Command Information Systems,Army Engineering University of PLA,Nanjing 210007,China
  • Received:2017-05-29 Online:2018-07-30 Published:2018-07-30

摘要: 多方不可否认协议需要满足不可否认性、公平性和时限性三大安全目标,但是现有的对多方不可否认协议的形式化分析方法大多是对两方协议分析方法的简单扩展,单一方法不能完整覆盖所有的安全目标分析;同时,对单一安全目标的分析能力有限,分析结果不可靠。首先,综合比较现有的分析技术,选定SVO逻辑进行扩展,显式引入时间因素,给出对应的语法定义和时间演算公理。然后,对改进逻辑的语义模型进行介绍,并证明了逻辑系统的可靠性,使得改进后的逻辑系统支持对多方不可否认协议三大安全目标的分析。最后,选取一个典型的多方不可否认协议,分别对其时限性和公平性进行分析,发现了其中存在的时限性和公平性缺陷,并给出了对应的攻击方法。其中,公平性缺陷是首次被发现。

关键词: SVO逻辑, 多方不可否认协议, 公平性, 时限性

Abstract: Multi-party non-repudiation protocol needs to meet three main security goals of non-repudiation,fairness and timeliness,but the existing formal analysis methods for multi-party non-repudiation proctocol are just simple extensions of those applied to two-party protocols.At the same time,each method can not cover all three security goals and has limited ability to analyze one goal with result unreliable.In this paper,the existing analysis methods were compared and the SVO logic was chosen for further study.Time factor was introduced in the logic system with relevant syntax definition and deduction axioms brought in explicitly.Then,the semantic model of the improved logic was stated and the soundness of logic system was proved,causing that the improved logic system can support the analysis of all three secu-rity goals of multi-party non-repudiation protocol.In the end,a typical multi-party non-repudiation protocol was analyzed with the improved logic and the defects of timeliness and fairness were found with corresponding attacks stated.Among the defects,the defect of fairness was discovered for the first time.

Key words: Fairness, Multi-party non-repudiation protocol, SVO logic, Timeliness

中图分类号: 

  • TP309
[1]FENG D G,FAN H.Survey on Theories and Methods of Formal Analysis for Security Protocols[J].Journal of the Graduate School of the Chinese Academy of Sciences,2003,20(4):389-406.(in Chinese)
冯登国,范红.安全协议形式化分析理论与方法研究综述[J].中国科学院研究生院学报,2003,20(4):389-406.
[2]ZHOU J,GOLLMAN D.A fair non-repudiation protocol[C]∥Proceedings of the 1996 IEEE Symposium on Security and Privacy.Oakland:IEEE Computer Society Press,1996:55-61.
[3]KREMER S,MARKOWITCH O.A multi-party non-repudiation protocol[C]∥15th International Conference on Information Security(SEC 2000).Beijing:Kluwer,2000:271-280.
[4]KREMER S,MARKOWITCH O.Fair multi-party non-repudiation protocols[J].International Journal of Information Security,2003,1(4):223-235.
[5]ONIEVA J A,ZHOU J,CARBONELL M,et al.A Multi-Party Non-Repudiation Protocol for Exchange of Different Messages[M].Boston:Springer,2003:37-48.
[6]HAN Z G,LUO J Z.Analysis and Improvement of Timeliness ofa Multi-Party Non-Repudiation Protocol[J].Acta Electronica Sinica,2009,37(2):377-381.(in Chinese)
韩志耕,罗军舟.多方不可否认协议时限性分析与改进[J].电子学报,2009,37(2):377-381.
[7]WANG X,WANG X.Formal Analysis Of Multi-party Non-repudiation Protocols Without TTP[C]∥International Conference on Communications and Intelligence Information Security.Nanning:IEEE Computer Society Press,2010:96-99.
[8]WANG X M,WENG L C.Analysis and Improvement of A Fair Multi-party Non-repudiation Protocol Based on ATL Logic[J].Information Security and Technology,2011,2(9):21-25.(in Chinese)
汪学明,翁立晨.基于ATL逻辑的公平多方不可否认协议的分析与改进[J].信息安全与技术,2011,2(9):21-25.
[9]LI L,WANG L,CHEN J,et al.Fairness Analysis for Multiparty Nonrepudiation Protocols Based on Improved Strand Space[J].Discrete Dynamics in Nature & Society,2014,17(1):1-7.
[10]SYVERSON P F,VAN O P C.A Unified Cryptographic Protocol Logic[R].Washington:Naval Research Lab,1996.
[11]LEI X F,XUE R.The Logic Methods of Cryptographic Protocol Analysis[M].Beijing:Science Press,2013:154-159.(in Chinese)
雷新锋,薛锐.密码协议分析的逻辑方法[M].北京:科学出版社,2013:154-159.
[12]WANG Y M.The Application Study on Formalism of Multi-Party Non-Repudiation Protocols on SVO Logic[D].Guiyang:Guizhou University,2009.(in Chinese)
王远敏.基于SVO逻辑的多方不可否认协议的形式化分析与研究[D].贵阳:贵州大学,2009.
[13]HE B,LI X J,XIA C H,et al.A Fair Multi-Party Non-Repudiation Protocol[J].Computer Engineering and Applications,2005,41(27):120-122.(in Chinese)
何冰,李肖坚,夏春和,等.公平的多方不可否认协议[J].计算机工程与应用,2005,41(27):120-122.
[14]HAN Z G,LUO J Z.A Fair Multi-Party Non-Repudiation Protocol[J].Chinese Journal of Computers,2008,31(10):1705-1715.(in Chinese)
韩志耕,罗军舟.一个公平的多方不可否认协议[J].计算机学报,2008,31(10):1705-1715.
[1] 卫宏儒, 李思月, 郭涌浩.
基于智能合约的秘密重建协议
Secret Reconstruction Protocol Based on Smart Contract
计算机科学, 2022, 49(6A): 469-473. https://doi.org/10.11896/jsjkx.210700033
[2] 彭冬阳, 王睿, 胡谷雨, 祖家琛, 王田丰.
视频缓存策略中QoE和能量效率的公平联合优化
Fair Joint Optimization of QoE and Energy Efficiency in Caching Strategy for Videos
计算机科学, 2022, 49(4): 312-320. https://doi.org/10.11896/jsjkx.210800027
[3] 郭利娟, 吕晓琳.
线性拓扑结构的乐观认证邮件
Optimistic Certified Email for Line Topology
计算机科学, 2018, 45(8): 156-159. https://doi.org/10.11896/j.issn.1002-137X.2018.08.028
[4] 刘海,彭长根,张 弘,任祉静.
一种理性安全协议的博弈逻辑描述模型
Game Logic Formal Model of Rational Secure Protocol
计算机科学, 2015, 42(9): 118-126. https://doi.org/10.11896/j.issn.1002-137X.2015.09.023
[5] 施洲琪,丁志军,陈闳中.
Petri网弱公平性和公平性关系的进一步研究
Further Study of Relationship between Weak Fairness and Fairness of Petri Nets
计算机科学, 2014, 41(7): 49-51. https://doi.org/10.11896/j.issn.1002-137X.2014.07.009
[6] 孙月,于炯,朱建波.
云计算中一种多DAG工作流可抢占式调度策略
Preemptive Scheduling for Multiple DAGs in Cloud Computing
计算机科学, 2014, 41(3): 145-148.
[7] 冯云芝,张恩.
基于博弈论的百万富翁协议
Millionaires’ Protocol Based on Game Theory
计算机科学, 2014, 41(12): 129-132. https://doi.org/10.11896/j.issn.1002-137X.2014.12.027
[8] 刘桂开,高蕾.
基于弹性定额值的分组轮询调度算法
RQRR:A New Fair and Efficient Packet Scheduling Algorithm
计算机科学, 2013, 40(8): 72-78.
[9] 张斌,王曦.
面向Web服务的SAML路径验证协议及其性能分析
SAMI. Path Verification Protocol for Web Service and its Performance Analysis
计算机科学, 2013, 40(3): 192-196.
[10] 王东,冯文江,衡玉龙.
OFDMA协同通信系统资源分配算法
Resource Allocation Algorithm for OFDMA-based Cooperative Communication Systems
计算机科学, 2012, 39(5): 86-90.
[11] 高悦翔 彭代渊.
一个多方认证邮件协议的分析与改进
Improvement and Formal Analysis of a Fair Multi-party Certified Mail Protocol
计算机科学, 2012, 39(11): 58-61.
[12] 廖盛斌,朱晓亮.
IEEE 802. 11无线局域网中基于最优窗口的退避算法
Optimal Window Based Backoff Algorithm for IEEE 802. 1 1 WLANs
计算机科学, 2012, 39(1): 82-84.
[13] 程杰仁,蔡志平,殷建平,张玲.
一种基于智能卡的匿名公平移动支付系统
Fair and Anonymous Mobile Payment System Utilizing Smart Card
计算机科学, 2011, 38(2): 50-54.
[14] 武航星,郑雪峰,潘文平.
基于跳数的公平性增强RED及其分类器实现
Hop-counts-based Fairness Enhancement RFD and its Classifier Implementation
计算机科学, 2011, 38(11): 62-66.
[15] 王鹃,刘珺,张焕国.
基于扩展CS逻辑的非否认协议形式化分析方法
Extended CS Logic for Analyzing Non-repudiation Protocols
计算机科学, 2010, 37(5): 49-52.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!