基于Pi演算的SOAP安全性分析与验证

论文摘要

基于XML技术的Web服务体系是一种新兴的分布式计算模型,其核心的消息交换协议为SOAP（Simple Object Access Protocol,简单对象访问协议）。在分布式环境中,Web服务之间通过传递SOAP消息进行通信。尽管WS-Security、WS-Policy等标准在理论上保证了端对端的消息层安全,但由于SOAP可扩展机制的灵活性,依然使Web服务容易受到一些特定攻击的威胁,如XML重写攻击等。通过对典型实例的分析得知,由于WS-Security缺少对SOAP拓扑结构的描述,XML重写攻击可以在不被数字签名技术侦测到的情况下,恶意修改SOAP消息的拓扑结构（例如插入含有有害代码的伪元素）,然后重新发送出去。针对这个问题的解决方案为,由发送端向即将发出的SOAP消息中额外加入记录消息拓扑的信息,并由接收端在策略驱动验证之前进行验证。除此之外,有必要建立一个端对端的消息层安全模型,用于批量处理应用了上述解决方案的SOAP消息。此解决方案的性能分析结果是理想的。一方面,扩展的XML安全元素无论是在发送方还是在接收方,都没有占用更多的网络带宽和CPU资源;另一方面,借助Pi演算从理论上证明了该模型具有安全性和认证性。从而可知,由上述解决方案和安全模型相结合的安全体系将成为Web服务中防御XML重写攻击的有效手段。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 引言
• 1.2 研究与发展现状
• 1.3 论文主要研究内容
• 1.4 论文的组织
• 第二章 Web 服务及 SOAP 概述
• 2.1 Web 服务
• 2.1.1 Web 服务协议栈
• 2.1.2 Web 服务的调用过程
• 2.1.3 Web 服务的三个基本角色和操作
• 2.2 SOAP
• 2.2.1 SOAP 规范
• 2.2.2 SOAP 的核心技术
• 2.3 本章小结
• 第三章 Web 服务及 SOAP 安全性分析
• 3.1 网络安全技术概述
• 3.1.1 网络安全需求
• 3.1.2 防火墙
• 3.1.3 SSL/TLS
• 3.1.4 HTTP 身份验证
• 3.1.5 加密技术
• 3.1.6 数字签名技术
• 3.2 Web 服务安全规范
• 3.2.1 WS-Security
• 3.2.2 XML 数字签名
• 3.2.3 XML 加密
• 3.3 SOAP 安全性
• 3.3.1 SOAP 安全解决方案
• 3.3.2 SOAP 安全性分析
• 3.3.3 SOAP 安全缺陷
• 3.4 本章小结
• 第四章 XML 重写攻击分析与防御
• 4.1 XML 重写攻击
• 4.1.1 问题提出
• 4.1.2 实例分析
• 4.2 XML 重写攻击防御原理
• 元素规范'>4.2.1 防御原理及元素规范
• 元素的自我防御'>4.2.2元素的自我防御
• 4.2.3 处理效率分析
• 4.3 反XML 重写攻击模型
• 4.4 本章小结
• 第五章 基于Pi演算的安全模型验证
• 5.1 Spi 演算
• 5.1.1 Spi 演算语法
• 5.1.2 自由与限制
• 5.1.3 反应关系
• 5.1.4 测试等价
• 5.2 基于Spi 演算的模型分析
• 5.3 HML、不动点理论与μ演算
• 5.3.1 HML
• 5.3.2 不动点理论
• 5.3.3 μ演算
• 5.4 移动工作台MWB（Mobility Workbench）
• 5.4.1 MWB 简介
• 5.4.2 MWB 的语法
• 5.5 基于Spi 演算的反XML 重写攻击模型形式化验证
• 5.5.1 CXMLRAM 模型的形式化
• 5.5.2 CXMLRAM 模型有效性、认证性和安全性验证
• 5.6 本章小结
• 结论
• 参考文献
• 攻读硕士学位期间取得的学术成果
• 致谢