【作者】 刘密霞；

【导师】 洪毅； 冯涛；

【作者基本信息】 兰州理工大学 ， 通信与信息系统， 2004， 硕士

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

【Abstract】 Security model, which aims at improving understanding of security requirement realization, precisely describe main aspects of security and its relationship with system action. Security policy plays an important role in confirming the content of security model. Therefore successfully developing a perfect security model needs clear and comprehensive policies. In particular, the composition of systems must consistently assure security policies that are supposed to enforce. However, there is currently no rigorous and systematic way to predict and assure such critical properties in security system design.This paper starts at information system and network security, and focuses on formal developing method of security system and security model. First, after analyzing deeply current security model, policy-based information security model is educed. In formal description, proper mathematics methods are usually needed to insure precise description and analysis. Second, a methodoly, which aims at modeling security architecture and verifying whether required security constraints are assured by the composition of the components, is introduced in this paper. Through the concept of security constraint patterns, the generic form of security policies are formally specified that the system architecture must enforce. Then, temporal logic and Petri net are applied to describe and verify access control in policy-based security model. TL, as a popular descriptive formalism, is best suited for describing rules and constraints. By contrast, Petri net is a well-known operational model well suited for modeling the control and composition of distributed system. Last, the resultant architectural model is verified against the systemwide security constraint patterns using Petri net’s analysis techniques--reachabilityanalysis, which not only ensures the integrity of early design decisions, but also provides a framework to guide correct implementations of the security system design.更多还原