基于时序逻辑的Web服务安全形式化描述与分析

发布时间：2021-04-02 21:54

　　随着Web服务应用的迅速发展,安全问题已成为制约其实际应用的障碍之一,而Web服务提供方的安全问题尤为重要。本文首先简要的介绍了Web服务。然后从Web服务面临的安全问题入手,分析了当前Web服务安全技术的研究现状,着重考虑了Web服务提供方所面临的安全问题。考虑到Web服务中安全策略的多样性,引入了一种基于安全策略与实现分离的信息安全解决模型,并根据Web服务的实际情况进行了改进。该模型采用一种类似于中间件的方法,使得它可以很容易的加入到现有的Web服务框架中。此外,本文所提倡的安全模型的体系结构使得它实现的时候可以方便Web服务提供方动态的制定安全策略,也可以灵活的实现策略指导下的各种安全措施。最后,为了帮助Web服务提供方的安全设计人员更好的理解、分析与实现该模型,本文用投影时序逻辑（PTL）形式化描述了该模型中资源访问决策部分的规范说明,并给出了自动机的上层实现。 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：68 页

【学位级别】：硕士

【部分图文】：

显示了完整的WS-Security安全框架，其中按箭头所指方向分别为框架的

等待策略状态完成等待策略的动作(Wait_pp，定义见 4.3 节)，一旦取得策略的命题(Get_pp)成立，则进行策略处理器的运算状态(State_Cal_pp)。State_Wait_pp halt(Get_pp)∧Wait_pp; if Get_pp then State_Cal_pp)策略处理器的运算状态进行策略是否得到满足的判断(Cal_pp，定义见 4.节)，判断结束后进入运算结果的综合状态(State_Com_res)。State_Cal_pp halt(all_cal_ed)∧Cal_pp; if all_cal_ed then State_Com_res策略处理器结果的综合状态完成运算结果的综合(Com_res，定义见 4.3 节)当有决策结果时(包括：决策结果为允许 dec_acc；决策结果为拒绝 dec_den)，发送决策结果(包括：将服务调用请求发给服务实现 Send_acc_req；拒绝请求并发送回执给服务方存根 Send_den_dec )并将 RADC 重新置为闲置状态，等待下一个服务调用请求的到来。定义如下：State_Com_res halt(dec_acc ∨d ec_den)∧ Com_res;(if dec_acc then Send_acc_req)∧ (if dec_den theSend_den_dec)∧State_RADC_idle其中策略处理器的运算状态(State_Cal_pp)又由两个状态组成，策略处理器正在运算状态(State_Cal_pp_ing)和等待系统动态属性状态(State_Wait_da)。

【参考文献】：
期刊论文
[1]W eb服务安全架构研究[J]. 白建坤.  计算机应用. 2005(11)
[2]Web服务核心支撑技术:研究综述[J]. 岳昆,王晓玲,周傲英.  软件学报. 2004(03)
[3]支持动态多策略的安全体系结构应用研究[J]. 赵志科,卿斯汉,李丽萍.  计算机工程. 2004(03)
[4]安全体系结构中的安全策略模型[J]. 黄新芳,李梁,赵霖.  计算机应用. 2003(10)



本文编号：3116028