This paper presents a clarification of the role that the Basic Security Theorem (BST) of Bell and LaPadula plays in the security model developed by those authors [1]. The major point made is that this role is essentially independent of notions of security. The BST gives conditions by which a system is secure, based on a definition of a secure state. The author shows that the proof of the BST can be carried out for any definition of secure state that permits indexing of states and an inductive proof. Consequently, the BST itself gives no assurance of security beyond the basic definition of secure state.

The author’s objective is to make clear that the proof of the BST does not enhance the definition of secure state and that work in security should address the basic problems of formalizing notions of security rather than reproving the BST for new models. The author acknowledges that, although some others have, Bell and LaPadula did not ascribe more significance to the BST than is warranted.