基于安全进程代数的信息流安全模型的分析与验证  

Security Process Algebra-Based Analysis and Verification of Information Flow Security Model

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

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

出　　处：《华东理工大学学报（自然科学版）》2012年第1期102-106,115,共6页Journal of East China University of Science and Technology

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

摘　　要：基于信息流的安全模型相对于基于访问控制的安全模型就刻画安全的性质而言更为本质。在安全进程代数统一框架下描述并形式化定义6种信息流安全模型,并且基于迹语义分析其逻辑蕴含关系,进一步对基于安全进程代数的6种信息流安全模型给出验证算法,并开发出验证工具,最后通过实例说明了该验证工具的使用。In characterizing security, the information flow security models capture more essence than the access control security models. Within the unified framework of security process algebra, this paper describes and formally defines six types of information flow security models and analyzes their relationship of logical implication based on trace semantics. Furthermore, both the verification algorithm and the verification tools are developed for the six information flow security models based on security process algebra. Finally, several examples are presented for their utilization.

关 键 词：安全进程代数 信息流安全模型 非推断模型 非干扰模型 分离模型 

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