安全模型(Security model)准确描述安全的重要方面及其与系统行为的关系，建立安全模型的主要目的是提高对成功实现关键安全需求的理解层次。安全策略在确定安全模型的内容上扮演了非常重要的角色，所以成功开发一个好的安全模型需要一个清晰的、全面的安全策略。尤其重要的是，系统的构成必须确保它所支持的安全策略的一致。但是当前并没有严格的和系统的方法来预测和保证安全系统设计中这些重要的特性。本论文以信息系统的安全和网络安全为出发点，对安全系统的形式化开发方法、信息安全模型展开了深入的研究。首先对现有的安全模型进行了深入的分析后，得出了基于策略的信息安全模型。在模型的正式描述中，往往需要通过适当的数学方法来达到准确描述和分析的目的。本文提出了一个模拟安全系统体系结构并验证所需的安全限制是否与组件的构成得到保证的一个方法，通过安全限制模式的概念，形式化的说明系统所执行的安全策略的一般形式。然后通过时序逻辑(TemporalLogic，TL)和Petri网这两个形式化描述的工具，对基于策略的安全模型中的访问控制进行了形式化的描述与验证。TL是一个很流行的形式化描述，最适合描述结果和限制，而Petri网是很好的操作模型，非常适合分布式系统的建模构成与控制。最后通过Petri网的性质--可达性分析，验证了安全系统体系下的整体限制模式与组件限制模式之间的一致性，从而保证早期设计决定的完整性，并为安全系统的正确执行提供了一个导向的框架。