PICSI

Le théorème de la sécurité qui est le fondement du modèle de Bell Lapadula affirme qu'un système est sécurisé si et seulement si l'état initial est un état sécurisé et que toutes les transitions d'état du système sont sécurisées, alors chaque état intermédiaire sera également sécurisé et cela indépendamment des accès au système. Selon cette théorie, pour démontrer qu'un système est sécurisé, il suffit de le modéliser par une machine à états dont dont on démontre que l'état initial et les états de transition sont sécurisés.