传统的基于角色的访问控制(Role-Based Access Control,RBAC)模型具有策略无关、自管理和便于实施信息系统安全策略的优点,但RBAC模型仍存在一些潜在的安全缺陷和冲突,比如RBAC模型缺乏信息流控制机制,存在非法信息流安全隐患等;而多域环境下的IRBAC(Interoperable Role-Based Access Control)模型因未定义静态职责分离和冲突处理方法,会造成域中静态互斥角色约束冲突;另外,具有时间约束的TRBAC(Temporal RBAC)和GTRBAC(Generalized TRBAC)模型的形式化定义也存在安全漏洞。随着分布式系统和网络技术,特别是电子商务的飞速发展,RBAC模型中安全问题迫切需要解决。Petri网是一种形式化的图形语言,可用于安全模型的形式化验证和安全性分析。为此,本文基于Petri网对RBAC模型及其扩展模型中存在的一些安全问题进行了研究,主要研究内容包括四个方面:一是基于Petri网的RBAC非法信息流的检测和控制。RBAC模型没有定义非法信息流,也没有提供信息流控制机制,由此带来了严重的非法信息流安全隐患。针对这一问题,本文提出一种基于经典Petri网的RBAC非法信息流检测方法,该方法可以利用单托肯经典Petri网的可达标识和可达标识图非常方便地可视化和分析RBAC中的非法信息流,并能利用可达标识状态对非法信息流进行有效地检测。此外,因需要在安全系统存在RBAC非法信息流的情况下仍然提供安全的访问控制,所以必须在RBAC系统中实现信息流控制。为此,本文提出一种基于有色Petri网的RBAC信息流控制方法,该方法使用颜色token代表不同对象的信息,通过变迁守卫函数有效地控制非法信息流,从而实现尽可能多的数据流动并保证信息流的安全。二是基于Petri网的IRBAC域间静态互斥角色约束冲突检测。IRBAC模型没有考虑静态职责分离(Static Separation of Duties,SSoD),会造成域中静态互斥角色(Statically Mutually Exclusive Roles,SMER)约束冲突。分析显示外域中的用户/角色分配是引起SMER约束冲突的根本原因,本文提出一种基于Petri网的方法解决IRBAC模型中由于用户/角色分配引起的SMER约束冲突检测问题。该方法把该SMER约束冲突检测问题转化为Petri网的状态空间搜索问题,可以有效地检测SMER约束冲突。为了判定IRBAC模型是否存在SMER约束冲突,本文基于Petri网给出了IRBAC模型存在SMER约束冲突的充要条件并进行了证明,提出了添加角色关联和用户/角色分配保证IRBAC模型SMER约束安全的先决条件,为IRBAC模型的角色关联和用户/角色分配动态操作提供了安全保证机制。三是面向隐私保护的IRBAC域间静态互斥角色约束冲突检测。已有的SMER约束冲突检测方法的研究没有考虑检测过程中RBAC策略的隐私安全问题。本文研究了面向隐私保护的IRBAC域间SMER约束冲突检测问题,提出了基于矩阵乘积的SMER约束冲突检测方法,并分别基于OT1n茫然传输协议和Paillier同态加密模式提出了三方安全矩阵乘积协议。在此基础上,提出了面向隐私保护的IRBAC域间SMER约束冲突检测协议。通过实验和比较分析显示,基于Paillier同态加密模式的方案效率更高。四是TRBAC和GTRBAC模型的安全分析、改进和形式化验证。GTRBAC模型在TRBAC模型基础上扩展了角色激活事件,该事件可通过依赖触发器触发管理事件,但GTRBAC模型未定义该事件违反角色激活约束冲突的处理方法,因此GTRBAC模型定义的安全充分条件并不能保证其安全性。本文提出了保证GTRBAC模型安全的处理方法,同时,本文在周期性时间概念的基础上定义了周期时刻概念,并基于周期时刻提出周期性时间约束的新表达方式,从而消除了TRBAC和GTRBAC两个模型中周期性时间约束定义上的歧义性。在此基础上,提出了一个改进的时间约束RBAC模型,详细定义了模型语义、执行语义和执行模型,为了保证执行模型的一致性定义了六种冲突及其对应的冲突处理方法。基于时间有色Petri网对该时间约束RBAC模型进行了形式化验证,保证了时间约束RBAC模型的安全性。