基于安全进程代数的非演绎安全模型的分析与验证  

Security Process Algebra-based Analysis and Verification of Non-deducibility Security Model

作　　者：王精明[1,2] 虞慧群[1] 

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

出　　处：《计算机科学》2012年第2期56-58,共3页Computer Science

基　　金：国家自然科学基金(61173048;60773094;60473055);上海市曙光计划(07SG32);安徽省高校省级自然科学研究基金项目(KJ2011Z279);安徽省滁州市滁州学院重点自然科学基金项目(2010kj008Z)资助

摘　　要：就刻画安全的性质而言,基于非演绎信息流的安全模型较基于访问控制的安全模型更为确切和本质。在基于迹语义对非演绎信息流安全模型进行分析的基础上,基于安全进程代数给出非演绎模型的形式化描述,然后基于系统的安全进程代数表达式给出非演绎模型的验证算法且开发了相应的验证工具,最后通过实例说明该算法的正确性和验证工具的方便适用性。In characterizing security,non-deducibility security model is more essential and accurate than access control security model.This paper described and formally defined non-deducibility information flow security model based on trace semantics and security process algbra.Furthermore,this paper provided the verification algorithm for non-dedu-cibility security model based on security process algebra and offered the verification tools,whose use was illustrated with several examples.

关 键 词：迹语义 安全进程代数 信息流安全模型 非演绎模型 

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