1. um modelo de transição de estado formal de uma política de segurança de computador que descreve um conjunto formal de controles de acesso com base em autorizações de sensibilidade e objecto de informação. . 2. um modelo de transição de estado formal da política de segurança de computador que descreve um conjunto de regras de controle de acesso. Neste modelo formal, as entidades em um sistema de computador são divididas em conjuntos abstratos de sujeitos e objetos. A noção de um estado seguro é definida e está provado que cada transição de estado preserva segurança movendo do estado seguro para seguro estado; Provando assim, indutivamente que o sistema é seguro. Um estado do sistema é definido para ser "seguro", se o único permitido acesso modos de assuntos para objetos estão em conformidade com uma política de segurança específicos. A fim de determinar se ou não um modo de acesso específico é permitido, o afastamento de um sujeito é comparado com a classificação do objeto e uma determinação é feita como se o assunto é autorizado para o modo de acesso específico. O regime de autorização/classificação é expressa em termos de uma treliça. Veja também: estrutura, propriedade de segurança simples, *-propriedade.