Abstract: 就刻画安全的性质而言，基于非演绎信息流的安全模型较基于访问控制的安全模型更为确切和本质。在基于迹语义对非演绎信息流安全模型进行分析的基础上，基于安全进程代数给出非演绎模型的形式化描述，然后基于系统的安全进程代数表达式给出非演绎模型的验证算法且开发了相应的验证工具，最后通过实例说明该算法的正确性和验证工具的方便适用性。

Key words: Trace semantics,Security process algebra,Information flow security modcl,Non-deducibility model