SPVT:一个有效的安全协议验证工具
作者:
基金项目:

Supported by the National Natural Science Foundation of China under Grant Nos.60073001, 60473057, 90104026 (国家自然科学基金); the National High-Tech Research and Development Plan of China under Grant No.2002AA144040 (国家高技术研究发展计划(863))


SPVT: An Efficient Verification Tool for Security Protocol
  • 摘要
  • | |
  • 访问统计
  • |
  • 参考文献 [19]
  • |
  • 相似文献
  • |
  • 引证文献
  • | |
  • 文章评论
    摘要:

    描述了基于Objective Caml开发的一个安全协议验证工具SPVT(security protocol verifying tool).在SPVT中,以扩展附加项的类(演算作为安全协议描述语言,以扩展附加项的Horn逻辑规则描述协议攻击者的Dolev-Yao模型,通过一组抽象规则将安全协议的类(演算模型转换为逻辑程序模型,基于安全协议逻辑程序的不动点计算验证安全性质,从安全协议逻辑程序的不动点计算和安全性质的验证过程中构造不满足安全性质的安全协议反例.以简化的Needham-Schroeder公钥认证协议为例,描述了使用SPVT自动验证安全协议的过程,表明了SPVT用于安全协议验证的有效性.

    Abstract:

    This paper describes the security protocol verifier SPVT developed by Objective-Caml. In SPVT (security protocol verifying tool), the specification language is the π-like calculus extended with three appendixes, the Dolev-Yao model is described with Horn logic rules, the π-like calculus model of security protocol is transformed into the logic program model by abstract rules, the security properties are verified based on the calculus of the logic program’s fixpoint, and the counter-examples on security properties are constructed from the process of the fixpoint calculus and the process of the property verification. The simplified Needham-Schroeder public-key authentication protocol is used to exemplify the automatic verification process of security protocol with SPVT, and the results show the validity of the verifier.

    参考文献
    [1]Abadi M,Blanchet B.Analyzing security protocols with secrecy types and logic programs.In:Jones ND,Leroy X,eds.Proc.of the 29th ACM SIGPLAN-SIGACT Symp.on Principles of Programing Languages (POPL 2002).Portland:ACM Press,2002.33-44.
    [2]Blanchet B.An efficient cryptographic protocol verifier based on prolog rules.In:Pandya P,Radhakrishnan J,eds.Proc.of the 14th Computer Security Foundation Workshop (CSFW14).Cape Breton:IEEE Computer Society Press,2001.82-96.
    [3]Blanchet B.From secrecy to authenticity in security protocols.In:Cousot P,ed.Proc.of the 9th Int'l Static Analysis Symp.(SAS 2002).LNCS 2477,Madrid:Springer-Verlag,2002.242-259.
    [4]Clark J,Jacob J.A survey of authentication protocol literature,Web draft version 1.0.1997.http://www.cs.york.uk/~jac
    [5]Lowe G.Breaking and fixing the needham-schroeder public-key protocol using FDR.In:Steffen M,ed.Proc.of the Tools and Algorithms for the Construction and Analysis of Systems (TACAS).LNCS 1055,Passau:Springer-Verlag,1996.147-166.
    [6]Abadi M,Gordon AD.A calculus for cryptographic protocols:The spi calculus.In:Matsumoto T,ed.Proc.of the 4th ACM Conf.on Computer and Communications Security.Zurich:ACM Press,1997.36-47.
    [7]Heather J,Lowe G,Schneider S.How to prevent type attacks on security protocols.In:Syverson P,ed.Proc.of the 13th Computer Security Foundation Workshop.IEEE Computer Society Press,2000.255-268.
    [8]Boreale M.Symbolic trace analysis of cryptographic protocols.In:Orejas F,Spirakis PG,Van Leeuwen J,ed.Proc.of the 28th Int'l Conf.on Automata,Language and Programming (ICALP 2001).LNCS 2076,Geneva:Springer-Verlag,2001.667-681.
    [9]Mitchell JC,Mitchell M,Stern U.Automated analysis of cryptographic protocols using mur (.In:Proc.of the 1997 IEEE Symp.on Security and Privacy.Okland:IEEE Computer Society Press,1997.141-153.
    [10]Song DX.Athena:A new efficient automatic checker for security protocol analysis.In:Gorrieri R,ed.Proc.of the 12th IEEE Computer Security Foundation Workshop (CSFW12).Mordano:IEEE Computer Society Press,1999.192-202.
    [11]Dolev D,Yao AC.On the security of public-key protocols.IEEE Trans.on Information Theory,1983,29(2):198-208.
    [12]Zhang YQ,Wang L,Xiao GZ,Wu JP.Model checking analysis of Needham-Schroeder public-key protocols.Journal of Software,2000,11(10):1348-1352 (in Chinese with English abstract).
    [13]Liu DX,Bai YC.Study on the proof method of authentication protocols based on Strand space.Journal of Software,2002,13(7):1313-1317 (in Chinese with English abstract).http://www.jos.org.cn/1000-9825/13/1313.htm
    [14]Li MJ,Li ZJ,Chen HW.A survey of security protocol verification based on process algebra.Journal of Computer Research and Development,2004,41(7):1093-1103 (in Chinese with English abstract).
    [15]Li MJ,Li ZJ,Chen HW.Verifying security protocol based on logic programming.Chinese Journal of Computers,2004,27(10):1361-1368 (in Chinese with English abstract).
    [12]张玉清,王磊,肖国镇,吴建平.Needham-Schroeder公钥协议的模型检测分析.软件学报,2000,11(10):1348-1352.
    [13]刘东喜,白英彩.基于Strand空间的认证协议证明方法研究.软件学报,2002,13(7):1313-1317.http://www.jos.org.cn/1000-9825/ 13/1313.htm
    [14]李梦君,李舟军,陈火旺.基于进程代数安全协议验证的研究综述.计算机研究与发展,2004,41(7):1093-1103.
    [15]李梦君,李舟军,陈火旺.基于逻辑程序的安全协议验证.计算机学报,2004,27(10):1361-1368.
    相似文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

李梦君,李舟军,陈火旺. SPVT:一个有效的安全协议验证工具.软件学报,2006,17(4):898-906

复制
分享
文章指标
  • 点击次数:4550
  • 下载次数: 5463
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2004-09-28
  • 最后修改日期:2005-11-08
文章二维码
您是第19868341位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号