伴随着科学技术的飞速发展,信息已成为推动社会前进的巨大动力。利用计算机和网络对信息进行收集、加工、存储以及交换等,越来越成为各行各业必不可少的手段,计算机已经渗透到了社会生活的各个方面,各种信息系统的建立和使用造成我们对计算机系统事实上的依赖。但是,由于各系统中存储的数据、网络上传输和交换的数据都是具有一定价值的信息,对这些信息的非法访问、窃取、篡改等行为必然导致计算机安全问题的出现。当前,系统的庞大和复杂化使得系统安全性能分析与验证问题变得越来越复杂并越来越引起人们的重视。提供有效的数学理论工具、直观的模型描述方法和有效的模型分析方法以及实用的辅助分析软件,是系统安全性能分析与验证所面临的迫切需要解决的问题,这也正是基于Petri网的安全策略分析与验证技术的核心。从计算机系统、Web服务以及安全协议的安全需求和现实基础出发,对相关理论、协议、关键技术以及具体实现进行了广泛深入的研究。主要研究工作包括以下几个方面:保密性策略和完整性策略是重要的安全策略,在许多军用和商用系统中得到广泛的应用。其代表模型分别是Bell-LaPadula模型和Biba模型,这两个模型是数学上的对偶。保密性策略用于防止信息的非授权泄漏,而完整性策略则是防止信息被非授权更改。对采用了特定安全模型的具体实用系统需要一个严格有效的方法对其保密性和完整性进行分析和验证。安全策略研究的一个关键问题是:用易于理解的和精确的形式表达策略。因此,提出了利用Petri网对安全策略进行描述,Petri网不仅适合策略的表达,而且可用于系统分析,以确定所定义的机制是否符合策略定义。对于一个安全策略,首先建立基于Petri网的形式化描述,然后就可以根据形式化的描述对实施了特定安全模型的进程或系统进行分析与验证。分别对Bell-LaPadula保密性模型和Biba完整性模型进行了描述。给出了这两个模型基于Petri网的形式化定义,并对实施了这两个安全模型的相应示例进程进行了分析和验证。显示出Petri网不仅能够用用易于理解的和精确的形式表达安全策略,而且可用于系统分析和验证。Petri网的覆盖图则在自动分析大型复杂系统方面很有用处。为了对实施了中国墙模型的系统进行分析与验证,提出了一种基于有色Petri网的混合安全策略分析方法。中国墙模型是一种兼顾保密性和完整性的混合安全模型。中国墙模型的显著特征是自由选择和强制性访问控制的结合。首先,对中国墙模型进行了非形式化的描述,并且将中国墙模型与其他安全模型进行了比较。然后,给出了中国墙模型基于有色Petri网的形式化定义。其突出特征在于,引入了“控制库所”的概念以解决跟踪主体访问记录的问题。并且“控制库所”代替访问控制矩阵,与单个主体关联,不需要集中存储,更加适合在分布式环境下部署。最后,根据中国墙模型基于有色Petri网的定义,通过对一个实施了中国墙模型的示例进程进行分析与验证,阐述了如何通过基于有色Petri网的形式化定义和覆盖图分析和验证实施了中国墙模型的系统的行为。当前的互联网正在经历着一些重要的变化,它已经成为了一个Web服务的载体,而不仅仅是一个信息的容器。Web服务提供了一个语言中立,连接松散,独立于平台的方式,使得散布在互联网上的各组织和企业内部的应用程序可以连接起来。Web服务合成可以让我们将许多现有的Web服务结合起来,形成一个新的,增值的Web服务。可靠的Web服务合成需要建模的技术和工具。因此,提出了一个基于有色Petri网的Web服务合成模型。这个模型为Web服务合成提供了充分的表达能力,能够直接变换为可执行的合成定义,并且独立于可执行的合成语言。基于Petri网的Web服务合成模型还可以利用Petri网的分析和验证能力对合成服务进行安全分析和验证。首先,对Web服务建立了有色Petri网模型(服务网),然后在此定义的基础上给出了四种基本Web服务合成结构:顺序结构,并发结构,选择结构,和循环结构以及一种高级合成结构置换结构的形式化定义。并且还定义了一个具有封闭性的Web服务合成算法。最后,根据基于Petri网的形式化验证方法对此Web服务合成模型的可用性,保密性,完整性以及混合安全性进行了分析和验证,得出了一些有用的结论。20年来,安全协议研究的进展十分可喜,取得了丰富的研究成果。特别是20世纪90年代以来,研究取得突破性进展,对安全协议若干本质性的问题有了更为深刻的认识。但是,这一领域还有许多问题有待解决。特别是形式化分析领域。因此,提出了一种基于有色Petri网的安全协议分析验证方法,该方法分为4个步骤:建立安全协议的Petri模型,建立入侵模型,找出不安全状态,验证不安全状态的可达性。并且通过对STS协议在特定攻击模式下的分析演示了该方法的工作原理和流程。