王精明，江怡顺

（1.滁州学院 计算机与信息工程学院，安徽 滁州239012；2.华东理工大学 计算机科学与工程系，上海 200237）

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

王精明1，2，江怡顺1

（1.滁州学院 计算机与信息工程学院，安徽 滁州239012；2.华东理工大学 计算机科学与工程系，上海 200237）

就刻画安全的本质而言，基于非演绎信息流安全模型较之与基于访问控制的安全模型更为确切。文章在基于迹语义对非演绎信息流安全模型进行分析的基础上，给出了基于扩展Petri网的非演绎模型的形式化描述，进一步基于Petri网的形式化描述给出非演绎模型的验证算法且开发相应的验证工具，最后通过实例说明该算法的正确性和验证工具的方便适用性。

迹语义；Petri网；信息流安全模型；非演绎模型

信息的机密性是分级安全系统研究的核心问题之一，安全模型的两个主要分支是基于信息流的安全模型和基于访问控制安全模型［1］。基于访问控制安全模型主要侧重于定义怎样做才能保证系统是安全的，而信息流安全模型侧重于安全是什么，从这点上说，就刻画安全的性质而言，基于信息流的安全模型较基于访问控制的安全模型更为确切和本质［2］。自Sutherland于1986年首次提出非演绎（non－deducibility）信息流安全模型以来，基于非演绎模型的研究不断深入，且其应用也越来越广泛，如［3－6］。

本文第一个工作在介绍相关概念和定义基础上以Petri网作为工具来形式化描述非演绎安全模型。因为Petri网在表示真并发方……