基于Petri网的非演绎安全模型的分析与验证  

Petri Net-based Analysis and Verification of Non-deducibility Security Model

作　　者：王精明[1,2] 江怡顺[1] 

机构地区：[1]滁州学院计算机与信息工程学院,安徽滁州239012 [2]华东理工大学计算机科学与工程系,上海200237

出　　处：《滁州学院学报》2012年第2期21-23,49,共4页Journal of Chuzhou University

基　　金：安徽省高校省级自然科学研究基金项目(KJ2011Z279);滁州学院重点自然科学基金项目(2010kj008Z)

摘　　要：就刻画安全的本质而言,基于非演绎信息流安全模型较之与基于访问控制的安全模型更为确切。文章在基于迹语义对非演绎信息流安全模型进行分析的基础上,给出了基于扩展Petri网的非演绎模型的形式化描述,进一步基于Petri网的形式化描述给出非演绎模型的验证算法且开发相应的验证工具,最后通过实例说明该算法的正确性和验证工具的方便适用性。In characterizing security, non--deducibility security model captures more essence than access control security models. This paper describes and formally defines non--dedueibility model based on trace semantics and Petri net. Furthermore, this paper provides the verification algorithm for non--de- ducibility security model based on Petri net and offers the verification tools with several examr^les.

关 键 词：迹语义 PETRI网 信息流安全模型 非演绎模型 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]