计算机科学 ›› 2018, Vol. 45 ›› Issue (7): 143-149.doi: 10.11896/j.issn.1002-137X.2018.07.024
苑博奥,刘军
YUAN Bo-ao, LIU Jun
摘要: 多方不可否认协议需要满足不可否认性、公平性和时限性三大安全目标,但是现有的对多方不可否认协议的形式化分析方法大多是对两方协议分析方法的简单扩展,单一方法不能完整覆盖所有的安全目标分析;同时,对单一安全目标的分析能力有限,分析结果不可靠。首先,综合比较现有的分析技术,选定SVO逻辑进行扩展,显式引入时间因素,给出对应的语法定义和时间演算公理。然后,对改进逻辑的语义模型进行介绍,并证明了逻辑系统的可靠性,使得改进后的逻辑系统支持对多方不可否认协议三大安全目标的分析。最后,选取一个典型的多方不可否认协议,分别对其时限性和公平性进行分析,发现了其中存在的时限性和公平性缺陷,并给出了对应的攻击方法。其中,公平性缺陷是首次被发现。
中图分类号:
[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. |
|