中文摘要：

由于BLP模型的基本安全公理不能完全证明模型的安全性，因此，在分析BLP改进模型的安全性时，如果模型的安全策略十分复杂而不能直接判断其安全性，或者模型由于改变了安全属性定义等而动摇了基本安全公理的推理基础时，应从其他角度证明改进模型的安全性．利用基于系统动作的不干扰模型，从信息流的角度给出一种对多级安全模型的形式化分析方法，为多级安全模型的安全性验证提供了一种新的途径．该不干扰模型把不干扰关系扩展到系统动作之间，提出了新的单步展开定理，可描述多级安全模型中的动态策略．通过以ABLP与DBLP模型为实例进行分析，说明了该分析方法的实用性．

英文摘要：

Some variants of BLP model can not prove whether their security policies match multilevel security requirements due to the limitation of security proof method of BLP model. It is pointed out that basic security theorem can only show whether a model match its security properties. So it is necessary to find a new way to formally analyze the improved BLP models instead of using basic security theorem as the original BLP, especially when the security of their improved rules is too complicated to judge directly or when the definition of security properties has been modified, which is considered as the reasoning basics of basic security theorem. In order to accomplish this, a security proof method is developed which takes advantages of a new noninterference model and provides a way to prove the security of multilevel security models from the point of view of information flow. The new noninterference model reclaims the definition of transitive noninterference relationship between system actions, presents a new unwinding theorem, and offers a great help in expressing dynamic policies of multilevel security models. To show practicability of the new noninterference model and the formal method, the security properties of ABLP and DBLP models are examined as examples.