1。アクセスの正式なセットを記述するコンピュータのセキュリティポリシーの正式な状態遷移モデルは、情報感度や被写体権限に基づいて制御します。 。 2。アクセス制御ルールのセットを記述するコンピュータのセキュリティポリシーの正式な状態遷移モデル。この正式なモデルでは、コンピュータシステム内のエンティティは、サブジェクトとオブジェクトの抽象的なセットに分かれています。安全な状態の概念が定義され、それが各状態の遷移は、状態を確保するためにセキュリティで保護された状態から移動することによってセキュリティを維持することが証明され、したがって、誘導システムが安全であることを証する。システムの状態は、オブジェクトに対するサブジェクトのアクセスモードを許可されていれば"安全"であると定義されている特定のセキュリティポリシーに従うものとします。特定のアクセスモードが許可されているかどうかを判断するためには、対象のクリアランスは、オブジェクトの分類と比較される判定は、対象が特定のアクセスモードのために認可されているかどうかが行われます。クリアランス/分類スキームは、格子の面で表現されます。も参照してください：ラティス、簡単なセキュリティのプロパティ、*-プロパティ。