学位论文 > 优秀研究生学位论文题录展示

基于策略的信息安全模型及形式化建模的研究

作　者: 刘密霞
导　师: 洪毅；冯涛
学　校: 兰州理工大学
专　业: 通信与信息系统
关键词: 信息安全安全策略访问控制形式化描述形式化建模形式化验证 Petri网时序逻辑
分类号: TP309
类　型: 硕士论文
年　份: 2004年
下　载: 267次
引　用: 6次
阅　读: 论文下载

内容摘要

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

全文目录

第一章绪论  6-9
  1.1 课题研究的背景  6-7
  1.2 信息安全研究的现状和存在的问题  7-8
  1.3 课题研究的内容  8
  1.4 论文的组织  8-9
第二章信息安全模型的研究  9-20
  2.1 安全模型的概念  9-11
    2.1.1 安全模型的性质和作用  9-10
    2.1.2 信息安全模型的类型  10-11
  2.2 Bell-Lapadula Model(BLP)  11-15
    2.2.1 BLP模型的形式化描述  11-14
    2.2.2 BLP模型的评估  14-15
  2.3 Biba模型  15-17
    2.3.1 Biba模型的元素  15
    2.3.2 完整性策略  15-17
    2.3.3 Biba的分析  17
  2.4 Chinese-Wall模型  17-20
    2.4.1 系统结构  17-18
    2.4.2 安全属性  18-19
    2.4.3 安全访问定理  19-20
第三章基于策略的信息安全模型  20-27
  3.1 PPDR模型  20-22
  3.2 基于策略的信息安全系统参考模型  22-27
    3.2.1 信息安全需求  23
    3.2.2 信息安全服务  23
    3.2.3 基于策略的信息安全模型  23-27
第四章信息安全系统形式化建模的方法及应用  27-40
  4.1 安全系统建模的方法  27
  4.2 形式化的工具  27-30
    4.2.1 时态逻辑  27-28
    4.2.2 Petri网的形式化描述  28-29
    4.2.3 Petri网的图形表示  29-30
  4.3 建模和分析的过程  30-32
  4.4 访问控制的形式化建模与分析  32-40
    4.4.1 RAD的框架与授权过程  32-33
    4.4.2 RAD的高级体系模型  33-35
    4.4.3 体系限制模式和它们的一致性验证  35-40
第五章模型的仿真与分析  40-42
  5.1 模型的可达性仿真  40
  5.2 导出数据文件的分析  40-42
结论  42-43
参考文献  43-45
致谢  45-46
攻读硕士学位期间发表的论文  46

基于策略的信息安全模型及形式化建模的研究

内容摘要

全文目录

相似论文