多方不可否认协议的增广CSP建模与分析

doi:10.3969/j.issn.1000-436x.2012.z2.026

通信学报 ›› 2012, Vol. 33 ›› Issue (Z2): 189-195.doi: 10.3969/j.issn.1000-436x.2012.z2.026

多方不可否认协议的增广CSP建模与分析

韩志耕¹,陈耿¹,罗军舟²

¹ 南京审计学院信息科学学院，江苏南京 211815
² 东南大学计算机科学与工程学院，江苏南京 211189

出版日期:2012-11-25 发布日期:2017-08-03
基金资助:
国家自然科学基金资助项目;国家自然科学基金资助项目;国家自然科学基金资助项目;江苏省高校自然科学基金资助项目;江苏省高校自然科学基金资助项目;江苏省网络与信息安全重点实验室基金资助项目;江苏省高校科研成果产业化推进工程基金资助项目;江苏省六大人才高峰基金资助项目;南京审计学院人才引进基金资助项目

Modeling and analysis of multi-party non-repudiation protocols with extended-CSP approach

Zhi-geng HAN¹,Geng CHEN¹,Jun-zhou LUO²

¹ School of Information Science,Nanjing Audit University,Nanjing 211815,China
² School of Compute Science and Engineer,Southeast University,Nanjing 211189,China

Online:2012-11-25 Published:2017-08-03
Supported by:
The National Natural Science Foundation of China;The National Natural Science Foundation of China;The National Natural Science Foundation of China;The Natural Science Foundation of Jiangsu Educational Committee;The Natural Science Foundation of Jiangsu Educational Committee;Jiangsu Provincial Key Laboratory of Network and Information Security;The Scientific Research Promotion Industrialization Project of Jiangsu Educational Committee;The Jiangsu Provincial Six Talents Peak Project;Nanjing Audit University Talent Introduction Projec

摘要/Abstract

摘要：

基于逆向工程的思想，使用前期工作中提出的面向两方不可否认协议分析的增广CSP方法，对典型的Kremer-Markowitch多方不可否认协议的安全性进行了探索性建模与分析。借助该分析成功发现此协议在满足不可否认性和公平性的同时却不具备时限性。这表明在适用于两方不可否认协议安全性验证的同时，增广CSP方法也可作为多方不可否认协议安全性验证的新方法。

关键词: 形式化分析, 多方不可否认, 时限性, 增广CSP方法

Abstract:

Follow with the methodology of reverse engineering,an exploratory modeling and analysis of security of the typical Kremer-Markowitch multi-party non-repudiation protocol were carried out with a novel method named extended-CSP approach which had been proposed for two-party non-repudiation protocol in preliminary work.With the analysis,the inherent fact that this protocol statisfies not timeliness but non-repudiality and fairness was found successfully.The result of the analysis indicates that,as applying to two-party non-repudiation protocols,the extended-CSP approach can also be a new method for security verification of multi-repudiation protocols.

Key words: formal analysis, multi-party non-repudiation, timeliness, extended-CSP approach

韩志耕,陈耿,罗军舟. 多方不可否认协议的增广CSP建模与分析[J]. 通信学报, 2012, 33(Z2): 189-195.

Zhi-geng HAN,Geng CHEN,Jun-zhou LUO. Modeling and analysis of multi-party non-repudiation protocols with extended-CSP approach[J]. Journal on Communications, 2012, 33(Z2): 189-195.

图/表 1

参考文献 29

[1]	ISO/IEC JTC1 Information Technology-Open Systems Interconnection-Security Frameworks in Open Systems Part 4:Nonrepudiation[S]. ISO/IEC DIS 10181-4, 1995.
[2]	MILDREY C , JOSE M S , JAVIER L . Secure multi-party payment with an intermediary entity[J]. Computers ＆ Security, 2009,28(5): 289-300.
[3]	SJOUKE M , SASA R , MOHAMMAD T D . Minimal message complexity of asynchronous multi-party contract signing[A]. Proc of 2009 IEEE Computer Security Foundations Symposium[C]. New York,USA, 2009. 13-25.
[4]	ARNE T . A survey of certified mail systems provided on the internet[J]. Computers＆Security, 2011,30(6/7): 464-485.
[5]	HUANG X Y , MU Y , WILLY S ,et al. Optimistic fair exchange with strong resolution-ambiguity[J]. IEEE Journal on Selected Areas in Communication, 2011,29(7): 1491-1502.
[6]	HUANG X Y , MU Y , WILLY S ,et al. Preserving transparency and accountability in optimistic fair exchange of digital signatures[J]. IEEE Trans on Information Forensics and Security, 2011,6(2): 498-512.
[7]	FENG J , CHEN Y , KU W S ,et al. Analysis of integrity vulnerabilities and a non-repudiation protocol for cloud data storage platforms[A]. Proceeding of 39th International Conferena on Parallel Processing (ICPP 2010)[C]. San Diego,USA, 2010.
[8]	KREMER S , MARKOWITCH O , ZHOU J . An intensive survey of non-repudiation protocols[J]. Computer Communications, 2002,25(17): 1606-1621.
[9]	ZHOU J , GOLLMANN D . A fair non-repudiation protocol[A]. Proceedings of the IEEE Symposium on Research in Security and Privacy[C]. Oakland,CA,USA, 1996. 55-61.
[10]	ZHOU J , GOLLMANN D . Towards verification of non-repudiation protocols[A]. Proc of Int Refinement Work and Formal Methods Pacific[C]. Canberra,Australia, 1998. 370-380.
[11]	范红, 冯登国 . 一个非否认协议ZG的形式化分析[J]. 电子学报 2005,33(1): 171-173. FANG H , FENG D G . Formal analysis of a non-repudiation protocol ZG[J]. Acta Electronica Sinica, 2005,33(1): 171-173.
[12]	SCHNEIDER S . Formal analysis of a non-repudiation protocol[A]. Proc of The 11th Computer Security Foundations Work[C]. USA, 1998. 54-65.
[13]	BELLA G , PAULSON L C . Mechanical proofs about a non-repudiation protocol[A]. TPHOLs 2001[C]. Edinburgh,Scotland,UK, 2001. 91-104.
[14]	KREMER S , RASKIN J F . A game-based verification of non-repudiation and fair exchange protocols[A]. CONCUR 2001[C]. Aalborg,Denmark, 2001. 551-565.
[15]	GURGENS S RUDOLPH C . Security analysis of efficient (Un-)fair non-repudiation protocols[J]. Formal Aspects of Computing, 2005,17(3): 260-276.
[16]	黎波涛, 罗军舟 . 不可否认协议的Petri网建模与分析[J]. 计算机研究与发展, 2005,42(9): 1571-1577. LI B T , LUO J Z . Modeling and analysis of non-repudiation protocols by petri nets[J]. Journal of Computer Research and Development, 2005,42(9): 1571-1577.
[17]	WEI K , HEATHER J . A theorem-proving approach to verification of fair nonrepudiation protocols[A]. FAST 2006[C]. Hamiltor Ontario,Canad, 2007. 202-219.
[18]	ARMANDO A , CARBONE R , COMPAGNA L . LTL model checking for security protocols[A]. 20th IEEE Computer Security Foundations Symp.CSF[C]. Venice,Italy, 2007, 385-396.
[19]	FRANCIS K , LAURENT V . Automatic methods for analyzing non-repudiation protocols with an active intruder[A]. Formal Aspects in Security and Trust(FAST 2008)[C]. Malaga,Spain, 2009. 192-209.
[20]	MAYLA B , AGOSTINO C . Non-repudiation analysis with LYSA[A]. IFIP Advances in Information and Communication Technology Emerging Challenges for Security Privacy and Trust[C]. Pafos,Cyprus, 2009. 318-329.
[21]	KREMER S , RASKIN J F . A game-based verification of nonrepudiation and fair exchange protocols[J]. Journal of Computer Security, 2003,11(3): 399-429.
[22]	CHADHA R , KREMER S , SCEDROV A . Formal analysis of multi-party contract signing[A]. Proceedings of the 17th IEEE Computer Security Foundations Workshop(CSFW'04)[C]. Ztaly, 2004. 266-279.
[23]	MUKHAMEDOV A , KREMER S , RITTER E . Analysis of a multi-party fair exchange protocol and formal proof of correctness in the strand space model[A]. Financial Cryptography 2005[C]. Ztaly, 255-269.
[24]	韩志耕, 罗军舟 . 多方不可否认协议时限性分析与改进[J]. 电子学报, 2009,37(2): 377-381. HAN Z G , LUO J Z . Analysis and improvement of timeliness of a multi-Party non-repudiation protocol[J]. ACTA Electronica Sinica, 2009,37(2): 377-381.
[25]	韩志耕, 罗军舟, 王良民 . 不可否认协议分析的增广CSP方法[J]. 通信学报, 2008,29(10): 8-18. HAN Z G , LUO J Z , WANG L M . Extended-CSP based analysis of non-repudiation protocols[J]. Journal on Communications, 2008,29(10): 8-18.
[26]	KREMER S , MARKOWITCH O . Fair multi-party non-repudiation protocols[J]. International Journal of Information Security SpringerVerlag, 2003,1(4): 223-235.
[27]	ONIEVA J , ZHOU J , LOPEZ J . Multi-party non-repudiation:a survey[J]. ACM Computing Surveys, 2008,41(1): 1-43.
[28]	KIM K , PARK S , BAEK J . Improving fairness and privacy of zhou-gollmann’s fair non-repudiation protocol[A]. Proc of ICPP workshop on Security(IWSEC)[C]. Wakamatsum,Japan, 1999. 140-145.
[29]	韩志耕, 罗军舟 . 一个公平的多方不可否认协议[J]. 计算机学报, 2008,31(10): 1705-1715. HAN Z G , LUO J Z . A fair multi-party non-repudiation protocol[J]. Chinese Journal of Computers, 2008,31(10): 1705-1715.

多方不可否认协议分析典型方法	状态爆炸	事件描述	基本安全性质分析
逻辑推理类（如扩展SvO）^[24]	不存在	能力弱	不适合建模与分析公平性
状态检测类（如Mocha）^[21]	存在	能力中	未见关联分析
定理证明类（如串空间模型）^[23]	不存在	能力强	时限性分析未见讨论
增广CSP方法	不存在	能力强	可关联分析

多方不可否认协议的增广CSP建模与分析

Modeling and analysis of multi-party non-repudiation protocols with extended-CSP approach

在线阅读

PDF下载

可视化

摘要/Abstract

引用本文

使用本文

图/表 1

参考文献 29

相关文章 11

Metrics

推荐阅读 0

[1]	龚翔, 冯涛, 杜谨泽. 基于CPN的安全协议形式化建模及安全分析方法[J]. 通信学报, 2021, 42(9): 240-253.
[2]	孟博,何旭东,张金丽,尧利利,鲁金钿. 基于计算模型的安全协议Swift语言实施安全性分析[J]. 通信学报, 2018, 39(9): 178-190.
[3]	顾纯祥，王焕孝，郑永辉，辛丹，刘楠. 基于SAT的安全协议惰性形式化分析方法[J]. 通信学报, 2014, 35(11): 13-116.
[4]	顾纯祥,王焕孝,郑永辉,辛丹,刘楠. 基于SAT的安全协议惰性形式化分析方法[J]. 通信学报, 2014, 35(11): 117-125.
[5]	闫丽丽,彭代渊,高悦翔. 传感器网络安全协议的分析和改进[J]. 通信学报, 2011, 32(5): 139-145.
[6]	杨超,张俊伟,马建峰,曾勇. 3G网络认证机制的分析及改进[J]. 通信学报, 2011, 32(11A): 163-168.
[7]	毛立强,马建峰,李兴华. 可证明安全的MANET按需源路由协议分析[J]. 通信学报, 2009, 30(1): 38-44.
[8]	韩志耕,罗军舟,王良民. 不可否认协议分析的增广CSP方法[J]. 通信学报, 2008, 29(10): 8-18.
[9]	刘军,廖建新,朱峰,王纯. 对Bellare-Rogaway 3PKD模型安全性定义的修正[J]. 通信学报, 2007, 28(9): 1-6.
[10]	张明生,张明义. 基于格的访问控制策略在RBAC中实现的形式化分析[J]. 通信学报, 2007, 28(11A): 1-7.
[11]	王春玲,唐志坚,张玉清,薛纪文. 运行模式法分析密码协议实例研究[J]. 通信学报, 2005, 26(1A): 129-132.