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

Using SPIN to Model and Analyze Web Services Secure Conversation Protocol

作　　者：魏昭[1] 董荣胜[1] 

机构地区：[1]桂林电子科技大学计算机与控制学院,541004

出　　处：《微计算机信息》2010年第9期81-83,共3页Control & Automation

基　　金：广西研究生教育创新计划资助项目;基金申请人:高三海;魏昭;项目名称:安全协议的结构化操作语义模型研究与应用(No.2007105950812M17)

摘　　要：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.

关 键 词：Web SERVICES SECURE Conversation协议 XML SPIN 

分 类 号：TP393[自动化与计算机技术—计算机应用技术]