安全策略的一种正式模型，用于制定一套访问控制规则。在遵循一套原则的基础上，该模型逐一证明该系统是安全。在该模型中，计算机系统中的实体被分成抽象的对象。安全状态得到了详细地说明，而且通过从一个安全状态转到另一个安全状态的方式来证明状态转移过程仍然是安全的，进而规纳地证明了该系统是安全的。