一种基于状态空间演化的网络安全协议执行验证技术
摘要
文章提出一种基于状态空间演化的网络安全协议执行验证技术,实现对全局安全协议执行的验证。经分析表明,该技术可以做到及时发现入侵者的攻击,阻止入侵者欺骗参与者或盗取秘密信息。
二级参考文献30
-
1M Boreale.Symbolic trace analysis of cryptographic protocols.In:Proc of the 28th Int'l Conf on Automata,Language and Prograing (ICALP'01),LNCS 2076.Geneva,Switzerland:Springer-Verlag,2001.667～681
-
2G Lowe.Breaking and fixing the Needham-Schroeder public-key protocol using FDR.In:Proc of Tools and Algorithms for the Construction and Analysis of Systems (TACAS),LNCS 1055.Passau,Germany:Springer-Verlag,1996.147～166
-
3L C Paulson.Proving properties of security protocols by induction.In:Proc of the 10th Computer Security Foundation Workshop (CSFW10).Massachusetts:IEEE Computer Society Press,1997.70～83
-
4F Javier,T Fabrega,J C Herzog,et al.Strand space:Proving security protocols correct.Journal of Computer Security,1999,7(2/3):191～230
-
5C Boyd,W Mao.On a limitation of BAN logic.In:Advances in Cryptology-EUROCRYPT'93,LNCS 765.Lofthus,Norway:Springer-Verlag,1993.240～247
-
6M Burrows,M Abadi,R Needham.A logic of authentication.In:Proc of the Royal Society of London,LNCS 426.London:Springer-Verlag,1989.233～271
-
7L Gong,R Needham,R Yahalom.Reasoning about belief in cryptographic protocols.In:IEEE Symp on Research in Security and Privacy.Oakland:IEEE Computer Society Press,1990.234～248
-
8P Syverson,C Meadows,I Cervesato.Dolev-Yao is no better than machiavelli.The 1st Workshop on Issues in the Theory of Security (WITS'00),Geneva,Switzerland,2000
-
9D Dolev,A C Yao.On the security of public-key protocols.IEEE Trans on Information Theory,1983,2(29):198～208
-
10D Sangiorgi,D Walker.The π Calculus:A Theory of Mobile Processes.England:Cambridge University Press,2001.20～50
共引文献32
-
1吴立军,苏开乐.安全协议认证的形式化方法研究[J].计算机工程与应用,2004,40(17):152-155. 被引量：5
-
2苏开乐,吕关锋,陈清亮.基于知识结构的认证协议验证[J].中国科学（E辑）,2005,35(4):337-351. 被引量：7
-
3周倜,李梦君,刘万伟,李舟军.安全协议的进程代数规约到逻辑程序的自动转换[J].计算机工程与科学,2006,28(1):22-24.
-
4李梦君,李舟军,陈火旺.SPVT:一个有效的安全协议验证工具[J].软件学报,2006,17(4):898-906. 被引量：18
-
5顾永跟,傅育熙.基于进程演算和知识推理的安全协议形式化分析[J].计算机研究与发展,2006,43(5):953-958. 被引量：7
-
6李梦君,王桢珍,李舟军,陈火旺.ACUN理论一般合一化问题的合一化算法[J].计算机工程与科学,2006,28(5):61-65.
-
7李梦君,李舟军,陈火旺.安全协议的扩展Horn逻辑模型及其验证方法[J].计算机学报,2006,29(9):1666-1678. 被引量：7
-
8苏开乐,陈清亮,Abdul Sattar,岳伟亚,吕关锋,郑锡忠.Verification of Authentication Protocols for Epistemic Goals via SAT Compilation[J].Journal of Computer Science & Technology,2006,21(6):932-943. 被引量：1
-
9顾永跟,傅育熙,朱涵.基于可达关系的安全协议保密性分析[J].计算机学报,2007,30(2):255-261. 被引量：4
-
10周清雷,赵琳,赵东明.基于串空间模型的Andrew RPC协议的分析与验证[J].计算机工程与应用,2007,43(13):153-155. 被引量：2
-
1张慧,郑超美.安全协议的形式化验证方法概述[J].计算机安全,2007(1):36-37.
-
2刘庆华,周小燕.安全协议的形式化分析方法[J].光盘技术,2008(3):32-33. 被引量：2
-
3王涛.跨域客户间口令认证的密钥交换协议[J].计算机工程与设计,2012,33(7):2546-2549. 被引量：1
-
4李梦君,李舟军,陈火旺.基于进程代数安全协议验证的研究综述[J].计算机研究与发展,2004,41(7):1097-1103. 被引量：25
-
5叶凯.电子支付也需要协议[J].互联网天地,2007(2):47-47.
-
6刘佳,王建东,庄毅.基于矢量空间的属性基签密方案[J].电子学报,2013,41(4):776-780. 被引量：5
-
7关洁.互联网信息安全的控制技术及应用[J].无线互联科技,2012,9(3):39-39. 被引量：3
-
8王海艳.校园网网络安全现状分析与解决[J].太原城市职业技术学院学报,2009(11):93-94.
-
9李文.网络安全新主张:安全与性能的双效融合——锐捷网络推出七大系列新品[J].中国金融电脑,2007(10):52-52.
-
10杨晋吉,苏开乐.电子商务中安全协议的验证方法[J].计算机工程与应用,2003,39(19):146-148.
