Формальная автоматная модель политики безопасности, описывающая множество правил управления доступом. В этой модели компоненты системы делятся на объекты и субъекты. Вводится понятие безопасного состояния и доказывается, что если каждый переход сохраняет безопасное состояние (то есть переводит систему из безопасного состояния в безопасное), то согласно принципу индукции система является безопасной.
Состояние системы считается безопасным, если в соответствии с политикой безопасности субъектам разрешены только определенные типы доступа к объектам (в том числе отсутствие доступа). Для определения, разрешен субъекту доступ к объекту или нет, его уровень прозрачности сравнивается с меткой объекта (уровнем безопасности объекта) и для запрашиваемого типа доступа принимается решение - разрешить доступ или нет. Принятие решения осуществляется на основе двух правил: простого условия безопасности (simple security condition) и *свойства (*-property или star property). Простое условие безопасности разрешает доступ, если уровень прозрачности субъекта не ниже метки критичности объекта.
*-условие разрешает доступ, если:
- для чтения или выполнения - текущий уровень субъекта не ниже метки критичности объекта;
- для записи или модификации - текущий уровень субъекта не выше метки критичности объекта.