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

基于Horn逻辑扩展模型的时间敏感安全协议验证

Verification of Time Sensitive Security Protocols Based on the Extended Horn Logic Model
下载PDF
导出
摘要 分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法,针对它们在验证时间敏感安全协议时的不足,提出了带时间约束的安全协议的Horn逻辑扩展模型和修改版本的安全协议验证方法,并给出了相应的定义和定理,使得带时间约束的安全协议的Horn逻辑扩展模型和修改版本的安全协议验证能够分析依赖时间的安全协议的安全性质.通过在验证中加入时间约束条件,得到了大嘴青蛙协议的攻击序列,并可从约束条件中导出避免攻击的条件.
作者 周倜 李梦君 李舟军 陈火旺
机构地区 国防科学技术大学计算机学院
出处 《计算机研究与发展》 EI CSCD 北大核心 2006年第z2期534-540,共7页 Journal of Computer Research and Development
基金 国家自然科学基金项目(90104026,60473057,90604007)
关键词 安全协议 扩展的Horn逻辑模型 时间敏感 约束条件 形式化验证
分类号 TP309 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献17

  • 1[1]J Clark,J Jacob.A survey of authentication protocol literature:Version 1.0.http://www.cs.york.ac.uk/～jac/papers/drareview.ps.gz,1997
  • 2薛锐,冯登国.安全协议的形式化分析技术与方法[J].计算机学报,2006,29(1):1-20. 被引量：60
  • 3[4]M Abadi,B Blanchet.Analyzing security protocols with secrecy types and logic programs.In:Proc of 29th ACM Symposium on Principles of Programming Languages(POPL'02).New York:ACM Press,2002.33-44
  • 4[5]B Blanchet.An efficient cryptographic protocol verifier based on Prolog rules.In:Proc of the 14th Computer Security Foundation Workshop(CSFW14).Los Alamitos,CA:IEEE Computer Society Press,2001.82-96
  • 5[6]B Blanchet.From secrecy to authenticity in security protocols.In:Proc of the 9th Int'l Static Analysis Symposium(SAS'02),LNCS 2477.Berlin:Springer-Verlag,2002.242-259
  • 6李梦君,李舟军,陈火旺.SPVT:一个有效的安全协议验证工具[J].软件学报,2006,17(4):898-906. 被引量：18
  • 7[8]Danny Dolev,Andrew C Yao.On the security of public-key protocols.IEEE Trans on Information Theory,1983,29(2):198-208
  • 8[9]Cervesato,N A Durgin,P D Lincoln,et al.A meta-notation for protocol analysis.In:Proc of the 12th IEEE Computer Security Foundations Workshop.Los Alamitos,CA:IEEE Computer Society Press,1999.55-69
  • 9[10]R Corin,S Etalle,P H Hartel,et al.Timed model checking of security protocols.In:Proc of the 2004 ACM Workshop on Formal Methods in Security Engineering.New York:ACM Press,2004.23-32
  • 10[11]Denning,Sacco.Timestamps in key distribution protocols.Communications of the ACM,1981,24(8):533-536

二级参考文献5

共引文献74

计算机研究与发展
2006年 第z2期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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