1. un énoncé mathématiquement précis d'une politique de sécurité du système. Parmi les quelques techniques de modélisation formelle : indiquer les modèles de transition, modèles logiques temporelles, sémantique dénotationnelle des modèles et des modèles de spécifications algébriques. 2. un énoncé mathématiquement précis d'une politique de sécurité. Pour être suffisamment précis, ce modèle doit représenter l'état initial d'un système, la façon dont le système progresse d'un État à un autre et d'une définition d'un état de « sécurisation » du système. Pour être acceptable comme base pour une PTE, le modèle doit être étayée par une preuve formelle que si l'état initial du système conforme à la définition de s « sécurisé » État et si toutes les hypothèses, requis par le modèle sont, ensuite, tous les futurs États du système sera sécurisés. Des techniques de modélisation formelle incluent : Etat des modèles de transition, modèles logiques temporelles, modèles de la sémantique dénotationnelle, modèles de spécifications algébriques. Est un exemple du modèle décrit par Bell et LaPadula en référence. Voir aussi : modèle de Bell-LaPadula, modèle de politique de sécurité.