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网的非演绎模型的形式化描述,进一步基于Petri网的形式化描述给出非演绎模型的验证算法且开发相应的验证工具,最后通过实例说明该算法的正确性和验证工具的方便适用性。
展开▼
