期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

基于ATL的公平交换协议的形式化验证 被引量：3

Formal verification of fair exchange protocols based on Alternating-Time Temporal Logic
下载PDF
导出
摘要 如何对电子商务协议进行分析与验证一直是研究的热点,基于ATL(交替时态逻辑)对电子商务协议中的公平交换协议(Fair Exchange Protocols)进行形式化分析与验证,并选取了其中的一个电子合同签署协议进行形式化验证。用ATL语言来形式化描述公平交换协议,并使用ATS(Alternating Transition Systems,交替转移系统)来为公平交换协议进行形式化建模,再用形式化验证工具MOCHA对公平交换协议的公平性(Fairness)、及时性(Timeliness)和不可滥用性(Abuse-Freeness)进行有效的验证;对验证结果进行分析与讨论,发现了该协议不满足公平性和不可滥用性,不符合设计的要求。 How to analyze and verify the e-commerce protocols has been a hot research. This paper bases on ATL （Alter- nating-Time Temporal Logic） to formal analyze and verify the fair exchange protocol, and chooses a electronic contract signing protocol for formal verification. It describes the fair exchange protocol by using the ATL language, and formal model of the fair exchange protocol by using ATS （Alternating Transition Systems）, and verifies the fairness, timeliness and abuse-freeness of the fair exchange protocol effective by using the formal verification tool MOCHA. The paper analyzes and discusses the result of the verification in the end, and finds that this protocol does not satisfy the fairness and abuse-freeness.
作者 李群 陈清亮
机构地区 暨南大学计算机科学系
出处 《计算机工程与应用》 CSCD 北大核心 2015年第19期32-36,共5页 Computer Engineering and Applications
基金 国家自然科学基金(No.61003056 No.61272415) 国家重点基础研究发展规划(973)(No.2010CB328103)
关键词 形式化验证 交替时态逻辑(ATL) MOCHA工具 公平交换协议 formal verification Alternating-Time Temporal Logic （ATL） MOCHA fair exchange protocol
分类号 TP301.2 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献13

  • 1Alur R,Henzinger T A,Kupferman O.Alternating-time temporal logic[J].Journal of the ACM(JACM),2002,49(5):672-713.
  • 2El-Menshawy M,Bentahar J,Dssouli R.Symbolic model checking commitment protocols using reduction[M]//Declarative Agent Languages and Technologies VIII.Berlin Heidelberg:Springer,2011:185-203.
  • 3Bauland M,Mundhenk M,Schneider T,et al.The tractability of model-checking for LTL:The good,the bad,and the ugly fragments[J].Electronic Notes in Theoretical Computer Science,2009,231:277-292.
  • 4Alrabaee S,Bataineh A,Khasawneh F A,et al.Using model checking for trivial file transfer protocol validation[C]//Proceedings of International Conference on Communications and Networking(Com Net),2014:1-7.
  • 5Armando A,Carbone R,Compagna L.LTL model checking for security protocols[J].Journal of Applied Non-Classical Logics,2009,19(4):403-429.
  • 6Jiang Y,Gong H.Modeling and formal analysis of communication protocols based on game[J].Information Technology Journal,2013,12(3):470-473.
  • 7Jamroga W,Mauw S,Melissen M.Fairness in non-repudiation protocols[M]//Security and Trust Management.Berlin Heidelberg:Springer,2012:122-139.
  • 8Zhang Y,Zhang C,Pang J,et al.Game-based verification of multi-party contract signing protocols[M]//Formal Aspects in Security and Trust.Berlin Heidelberg:Springer,2010:186-200.
  • 9Browne M C,Clarke E M,Grümberg O.Characterizing finite Kripke structures in propositional temporal logic[J].Theoretical Computer Science,1988,59(1):115-131.
  • 10王芷玲,张玉清,杨波.一个公平电子合同签署协议的设计[J].计算机工程,2006,32(19):159-161. 被引量：4

二级参考文献5

  • 1Asokan.Optimistic Protocols for Fair Exchange[C].Proc.of the 4th Conference on Computer and Communication Security,1997:8-17.
  • 2Micali S.Simple and Fast Optimistic Protocols for Fair Electronic Exchange[C].Proc.of Symposium on Principles of Distributed Computing,2003:12-19.
  • 3Feng Bao.Analysis and Improvement of Micali's Fair Contract Signing Protocol[C].Proc.of ICANN'04,Sydney,2004:176-187.
  • 4Pagnia H.On the Impossibility of Fair Exchange Without a Trusted Third Party[R].Darmstadt University of Technology,Technical Report:TUD-BS-1999-02,1999.
  • 5Abadi M.Prudent Engineering Practice for Cryptographic Protocols[R].Digital Equipment Corporation Systems Research Center,Research Report:125,1994.

共引文献3

同被引文献34

引证文献3

二级引证文献2

计算机工程与应用
2015年 第19期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部