公平交换协议的信道可信度形式化验证方法
|
摘要
公平交换协议是一种重要的电子商务安全协议,已有的针对公平交换协议进行的形式化验证只能定性分析协议是否满足给定性质,本文提出基于信道可信度的公平交换协议的形式化验证方法,重点对信道问题进行定量分析.以一个电子合同签署协议为例,通过概率模型检测的方法对协议建立离散时间马尔可夫链模型,用概率计算树逻辑对协议属性进行描述,通过PRISM概率模型检测工具对协议进行定量的验证和分析.实验结果表明公平交换协议各实体间信道可信度对协议的公平性、有效性和时限性有不同程度的影响,对相应信道进行控制或改善可以提高协议安全性.
Fair exchange protocol is an important e-commerce security protocol. The existing formal verification for the fair exchange protocol can only qualitatively analyze whether the protocol satisfies the given property. This paper presents a formal verification method for fair exchange protocol based on channel confidenceand focus on the quantitative analysis of channel problems. Taking an electronic contract signing protocol as an example,this paper establishes the discrete-time Markov Chain for the protocol by probabilistic model detection method,describes the attribute of the protocol by probabilistic computation tree logic,verifies the protocol quantitatively by PRISM probabilistic model checking tool. Experimental results show that the channel reliability of the entities of the fair exchange protocol has different influence on the fairness,effectiveness and timeliness of the protocol. Control or improvement of the corresponding channel can improve protocol security.
Fair exchange protocol is an important e-commerce security protocol. The existing formal verification for the fair exchange protocol can only qualitatively analyze whether the protocol satisfies the given property. This paper presents a formal verification method for fair exchange protocol based on channel confidenceand focus on the quantitative analysis of channel problems. Taking an electronic contract signing protocol as an example,this paper establishes the discrete-time Markov Chain for the protocol by probabilistic model detection method,describes the attribute of the protocol by probabilistic computation tree logic,verifies the protocol quantitatively by PRISM probabilistic model checking tool. Experimental results show that the channel reliability of the entities of the fair exchange protocol has different influence on the fairness,effectiveness and timeliness of the protocol. Control or improvement of the corresponding channel can improve protocol security.
引文
[1]Asokan N.Fairness in electronic commerce[M].University of Waterloo,1998.
[2]Xu Jing-fang,Cui Guo-hua,Cheng Qi,et al.Security analysis and improvement of fair exchange protocols using the theory of cross validation[J].Journal of Chinese Computer Systems,2009,30(2):345-348.
[3]Li Qun,Chen Qing-liang.Formal verification of fair exchange protocols based on alternating-time temporal logic[J].Computer Engineering and Applications,2015,51(19):32-36.
[4]Norman G,Shmatikov V.Analysis of probabilistic contract signing[C].Formal Aspects of Security,First International Conference,FASec 2002,London,UK,DBLP,2002:81-96.
[5]Alrabaee S,Bataineh A,Khasawneh F A,et al.Using model checking for trivial file transfer protocol validation[C].Fourth International Conference on Communications and Netw orking,2014:1-7.
[6]Bella G,Paulson L C.Accountability protocols:formalized and verified[J].Acm Transactions on Information&System Security,2006,9(2):138-161.
[7]Huo Yan-yan,Guan Yong,Li Xiao-juan,et al.Formal verification of distributed real-time operating system task scheduling based on PRISM[J].Journal of Chinese Computer Systems,2015,36(9):2125-2129.
[8]Clarke E M,Emerson E A.Design and synthesis of synchronization skeletons using branching time temporal logic[C].DBLP,2008:196-215.
[9]Baier C,Katoen J P.Principles of model checking(representation and mind series)[M].The M IT Press,2008.
[10]Liu Yang,Li Xuan-dong,Ma Yan,et al.Survey for stochastic model checking[J].Chinese Journal of Computers,2015,38(11):2145-2162.
[11]Wang Zhi-ling,Zhang Yu-qing,Yang Bo.Design of a fair contract signing protocol[J].Computer Engineering,2006,32(19):159-161.
[12]Kwiatkowska M,Norman G,Parker D.PRISM 4.0:verification of probabilistic real-time systems[C].In Ganesh Gopalakrishnan,Shaz Qocleer,Computer Aided Verification,Proceeding of 23rd International Conference,CAV2011,Snow bird,UT,USA,2011:585-591.
[13]Kremer S.Formal analysis of optimistic fair exchange protocols[D].Brussels:UniversitéLibre de Bruxelles,2004.
[2]许静芳,崔国华,程琦,等.关于公平交换协议中使用正交验证理论的安全性分析及改进[J].小型微型计算机系统,2009,30(2):345-348.
[3]李群,陈清亮.基于ATL的公平交换协议的形式化验证[J].计算机工程与应用,2015,51(19):32-36.
[7]霍燕燕,关永,李晓娟,等.基于PRISM的分布式实时操作系统任务调度的形式化验证[J].小型微型计算机系统,2015,36(9):2125-2129.
[10]刘阳,李宣东,马艳,等.随机模型检验研究[J].计算机学报,2015,38(11):2145-2162.
[11]王芷玲,张玉清,杨波.一个公平电子合同签署协议的设计[J].计算机工程,2006,32(19):159-161.
[2]Xu Jing-fang,Cui Guo-hua,Cheng Qi,et al.Security analysis and improvement of fair exchange protocols using the theory of cross validation[J].Journal of Chinese Computer Systems,2009,30(2):345-348.
[3]Li Qun,Chen Qing-liang.Formal verification of fair exchange protocols based on alternating-time temporal logic[J].Computer Engineering and Applications,2015,51(19):32-36.
[4]Norman G,Shmatikov V.Analysis of probabilistic contract signing[C].Formal Aspects of Security,First International Conference,FASec 2002,London,UK,DBLP,2002:81-96.
[5]Alrabaee S,Bataineh A,Khasawneh F A,et al.Using model checking for trivial file transfer protocol validation[C].Fourth International Conference on Communications and Netw orking,2014:1-7.
[6]Bella G,Paulson L C.Accountability protocols:formalized and verified[J].Acm Transactions on Information&System Security,2006,9(2):138-161.
[7]Huo Yan-yan,Guan Yong,Li Xiao-juan,et al.Formal verification of distributed real-time operating system task scheduling based on PRISM[J].Journal of Chinese Computer Systems,2015,36(9):2125-2129.
[8]Clarke E M,Emerson E A.Design and synthesis of synchronization skeletons using branching time temporal logic[C].DBLP,2008:196-215.
[9]Baier C,Katoen J P.Principles of model checking(representation and mind series)[M].The M IT Press,2008.
[10]Liu Yang,Li Xuan-dong,Ma Yan,et al.Survey for stochastic model checking[J].Chinese Journal of Computers,2015,38(11):2145-2162.
[11]Wang Zhi-ling,Zhang Yu-qing,Yang Bo.Design of a fair contract signing protocol[J].Computer Engineering,2006,32(19):159-161.
[12]Kwiatkowska M,Norman G,Parker D.PRISM 4.0:verification of probabilistic real-time systems[C].In Ganesh Gopalakrishnan,Shaz Qocleer,Computer Aided Verification,Proceeding of 23rd International Conference,CAV2011,Snow bird,UT,USA,2011:585-591.
[13]Kremer S.Formal analysis of optimistic fair exchange protocols[D].Brussels:UniversitéLibre de Bruxelles,2004.
[2]许静芳,崔国华,程琦,等.关于公平交换协议中使用正交验证理论的安全性分析及改进[J].小型微型计算机系统,2009,30(2):345-348.
[3]李群,陈清亮.基于ATL的公平交换协议的形式化验证[J].计算机工程与应用,2015,51(19):32-36.
[7]霍燕燕,关永,李晓娟,等.基于PRISM的分布式实时操作系统任务调度的形式化验证[J].小型微型计算机系统,2015,36(9):2125-2129.
[10]刘阳,李宣东,马艳,等.随机模型检验研究[J].计算机学报,2015,38(11):2145-2162.
[11]王芷玲,张玉清,杨波.一个公平电子合同签署协议的设计[J].计算机工程,2006,32(19):159-161.