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

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

Abstract

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

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.

Figures/Tables 1

References 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.

Metrics

Recommended 0

No Suggested Reading articles found!

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

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

RichHTML

PDF

Knowledge

Abstract

Cite this article

share this article

Figures/Tables 1

References 29

Related Articles 11

Metrics

Recommended 0

[1]	Xiang GONG, Tao FENG, Jinze DU. Formal modeling and security analysis method of security protocol based on CPN [J]. Journal on Communications, 2021, 42(9): 240-253.
[2]	Bo MENG,Xudong HE,Jinli ZHANG,Lili YAO,Jintian LU. Security analysis of security protocol Swift implementations based on computational model [J]. Journal on Communications, 2018, 39(9): 178-190.
[3]	Li-li YAN,Dai-yuan PENG,Yue-xiang GAO. Analysis and improvement of sensor networks security protocol [J]. Journal on Communications, 2011, 32(5): 139-145.
[4]	Chao YANG,Jun-wei ZHANG,Jian-feng MA,Yong ZENG. Analysis and amendment of 3G authentication access mechanism [J]. Journal on Communications, 2011, 32(11A): 163-168.
[5]	Dong-mei LIU,Si-han QING,Peng-fei LI,Shang-jie LI. Analysis and improvement of ZG off-line TTP non-repudiation protocol [J]. Journal on Communications, 2009, 30(11A): 44-51.
[6]	Li-qiang MAO,Jian-feng MA,Xing-hua LI. Analysis of provably secure on-demand source routing in MANET [J]. Journal on Communications, 2009, 30(1): 38-44.
[7]	Zhi-geng HAN,Jun-zhou LUO,Liang-min WANG. Extended-CSP based analysis of non-repudiation protocols [J]. Journal on Communications, 2008, 29(10): 8-18.
[8]	Jun LIU,Jian-xin LIAO,Feng ZHU,Chun WANG. Correcting the security definition of the Bellare-Rogaway 3PKD model [J]. Journal on Communications, 2007, 28(9): 1-6.
[9]	Ming-sheng ZHANG,Ming-yi ZHANG. Formal analysis on implementing LBAC policy in RBAC [J]. Journal on Communications, 2007, 28(11A): 1-7.
[10]	Li-ping LI,Si-han1 QING,Zhou-yi ZHOU,EJian-bo H,ENHong-zi W. Research on formal security policy model specification and its formal analysis [J]. Journal on Communications, 2006, 27(6): 94-101.
[11]	Chun-ling WANG,Zhi-jian TANG,Yu-qing ZHANG,Ji-wen XUE. Using running modes for cryptographic protocol analysis: a case study [J]. Journal on Communications, 2005, 26(1A): 129-132.