Computer security models are specifications designed, among other things, to limit the damage caused by Trojan Horse programs such as computer viruses. Recent work in such models has revealed limitations of the widely accepted model of Bell and LaPadula. This paper provides an introduction to computer security modeling in general, the Bell and LaPadula model in particular, and the limitations of the model. Many of the issues raised are of interest not simply to the security community, but for the software specification community as a whole. We then construct a framework for security models that address these limitations. The result is a model that not only better addresses government security policies, but nongovernment security policies as well.