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

Web服务安全会话协议的SPIN建模与分析

Using SPIN to Model and Analyze Web Services Secure Conversation Protocol
在线阅读 下载PDF
导出
摘要 Web Services Secure Conversation是基于XML的安全协议.本文对该协议进行了形式化的分析,并使用模型检验工具SPIN验证了协议的安全性,结果表明该协议存在认证性缺陷。为此,修改了协议的消息结构并对用户口令进行了数字签名。对改进后协议的安全性进行分析,结果表明改进后的协议不存在原协议的缺陷,协议满足认证性要求。 Web Services Secure Conversation protocolis a security protocol based on XML .In this paper , We analyze and verify security property for this protocol with formal analysis method and a model checking tool SPIN.The result shows that the protocol has a authentication flaw.For the flaw, the message structure of the protocol is amended and a user password is signed.Then, the security of the improved protocol is analyzed ,which can guarantee authentication.
作者 魏昭 董荣胜
机构地区 桂林电子科技大学计算机与控制学院
出处 《微计算机信息》 2010年第9期81-83,共3页 Control & Automation
基金 广西研究生教育创新计划资助项目 基金申请人:高三海 魏昭 项目名称:安全协议的结构化操作语义模型研究与应用(No.2007105950812M17)
关键词 Web SERVICES SECURE Conversation协议 XML SPIN Web Services Secure Conversation protocol XML SPIN
分类号 TP393 [自动化与计算机技术—计算机应用技术]
  • 相关文献

参考文献10

  • 1王惠斌,祝跃飞.一种快速安全认证协议及其形式化分析[J].微计算机信息,2008,24(27):68-70. 被引量：1
  • 2IBM, B. Systems, Microsoft, C. Associates, Actional,VeriSign, L . Technologies, Oblix, O. Technologies, P. Identity,Reactivity, and R. Security. Web services secure conversation language, February 2005.
  • 3G.J.Holzmann. the Model checker SPIN. IEEE Transaction on Software Engineering, Vol.23, 1997,pp76-95.
  • 4IBM and Microsoft. Security in a web services world: a proposed architecture and roadmap, April 2002.
  • 5Simple Object Access Protocol (SOAP) 1.1. W3C Note 08, May 2000. http://www.w3.org/TR/SO AP/.
  • 6IBM, B. Systems, Microsoft, C. Associates, Actional,VeriSign, L . Technologies, Oblix, O. Technologies, P. Identity, Reactivity, and R. Security. Web services trust language(ws-trust), February 2005.
  • 7Gregorio Diaz , Juan-Jos'e Pardo , Mar'la-Emilia Cambronero , Valent'ln Valero, Fernando Cuartero .Verification of Web Services with Timed Automata. 1st Int'l Workshop on Automated Specification and Verifieation of Web Sites, 2005.
  • 8K. Bhargavan, C. Foumet, A. Gordon, and R.Corin. "Secure Sessions for Web Services", Augus 2004 [Online]. http://research. mierosoft.com/projeets/samoa/seeuresessions-with-scripts.pdf.
  • 9K. Bhargavan, C. Fournet, A. D. Gordon, and R. Pucella. Tulafale: A security tool for web services. In Formal Methods for Components and Objects: Second International Symposium, FMCO 2003, volume 3188 of Lecture Notes in Computer Science, pages 197 - 222. Springer, November 2003.
  • 10Rongsheng Dong, Zhao Wei, Xiangyu Luo. Model Checking Behavioral Specification of BPEL Web Services. The 2008 International Conference of Computer Science and Engineering, London, U.K.SCI 收录.

二级参考文献5

  • 1蔡利民,孔力.信息家电身份认证系统的实现[J].微计算机信息,2007(03X):46-47. 被引量：1
  • 2ZHANG H-J. Research and Design of Authentication Security Infrastructure of WLAN. [D]. Information Engineering University. ZhengZhou.2006:69-126
  • 3Burrows M,Abadi M,Needham R.A logic of authentication. ACM Transactionson Computer Systems[J]. 1990,8(1): 18 - 36
  • 4Paulson L C. Proving properties of security protocols by induction. In 10th IEEE Computer Security Foundations Workshop[C]. 1997:70 - 83
  • 5Datta A, Derrick A, Mitchell J.C,Roy A, Protocol composition logic (PCL). In Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin, ed. L. Cardelli, M. Fiore and G. Winskel, Electronic Notes in Theoretical Computer Science, 2007.
微计算机信息
2010年 第9期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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