基于着色Petri网的GEO-RBAC策略验证

GEO-RBAC是一种能够处理空间信息的访问控制策略,其角色按照粒度分为角色模式和角色实例,按照维数分为空间角色和非空间角色。基于实例的角色分配与传统RBAC策略类似。使用着色Petri网对GEO-RBAC中基于模式的角色分配进行建模,并给出了可达性分析方法,通过对角色分配事件图可达状态的分析实现了GEO-RBAC策略的一致性验证。     

基于Petri网和抽象方法的工作流模型分解

Petri网是描述工作流的理想建模工具,本文介绍了一种基于抽象方法的工作流模型的分解过程,将工作流网分解为两个满足二元模拟关系的子网,其结果得到工作流模型,并举例说明了基于抽象的工作流模型分解可以减少原始模型Kripke结构的状态数目,为工作流的模型验证提供了一种有效的方法.     

基于Petri网的强制访问控制模型及其安全分析

强制访问控制模型(MAC)是一种重要的安全模型.在多级安全的格模型和Bell-LaPadula安全模型的基础上,对MAC安全模型进行了形式化描述,并给出了与其等价的着色Petri网模型.在Petri网状态可达图的基础上,对MAC模型的有关安全属性,如主体访问客体的时序关系,主体访问的可达性,因主体的动态安全级访问而存在的安全隐患以及因主体对客体的间接访问而导致敏感信息的可推测性等进行了较为详细地分析.通过对一个安全模型的范例分析,结果表明基于Petri网的安全模型的分析方法可以充分利用现有的可达图的分析方法来对系统安全模型的有关性质进行分析和验证,能够在安全模型的设计和实现阶段有效地改善系统的总体安全策略.