1. Gasser, M., Building a Secure Computer System, Van Nostrand Reinhold, New York, 1988. Pages 3-90. A general introduction to Computer Security, multi-level security, access control, design considerations, Trojan horses, and covert channels.

2. Abrams, M., and H. Podell, and S. Jajodia, Information Security-An Integrated Collection of Essays, IEEE Computer Society Press, 1995. Pages 11-96. Comprises a general treatment and classification of computer security threats, and a detailed, but conceptual, reading about multi- level security, mandatory and discretionary access control, the reference monitor concept, TCB, TCSEC, security policy, security model, etc.

3. Bell, D., and L. LaPadula, "Secure Computer Systems: A Mathematical Model", Vol. II, MITRE Technical Report 2547, The MITRE Corporation, Bedford, MA 1973/74. The original presentation of the widely known Bell and LaPadula security model. Theorem proofs have been deliberately omited.

4. McLean, J., "The specification and modeling of computer security"; IEEE Computer, january 1990. A deep study of BLP security model. It shows the limitations of the model, and proposes a new and more general approach to the Trojan horse problem. This paper contains very clear examples about malicious code, covert channels and the pros and cons of BLP in this context.

5. Denning, D., "A lattice model of secure information flow", Communication of the ACM, 19(5):236-243, may 1976. A declarative approach to model multi-level security. The author defines a mathematical representation of MLS but without states, her model simply follows the flow of information across objects. Covert channels are also treated. Most of the paper applies the model to program variables, instead to operating system objects.

6. Goguen, J. and J. Meseguer, "Security policies and security models", Proceedings of the 1982 IEEE Symp. on Security and Privacy, 1982. This paper, as Bell and LaPadula's one, is one of the milestones on computer security research. It generalizes the problem of security to a level unknown until that time. In fact, BLP is just an special case of the theory developed by Goguen and Meseguer. The paper also clarifies, how to model and verify computer security problems. The theory concentrates in input and output rather than on states, which gives a very abstract view of security.

7. Clark, D. and D. Wilson, "A comparison of commercial and military computer security policies", Proceedings of the IEEE Symposium on Security and Privacy, april 1987. This is other mandatory reading for computer security. In this paper, the authors show that confidentiality it is of secondary importance in the commercial world, being integrity the most important property. This statement implies that MLS models and policies are not applicable for commercial instalations. For this reason, the authors ropose a new model which protect systems from integrity attacks.

8. Harrison, M., and W. Ruzzo, and J. Ullman, "Protection in operating systems", Communication of the ACM, 19(8):461-471, august 1976. This is an optional paper. It shows that the general safety problem for protection is, under surprisingly weak assumptions, undecidable. They prove this result by showing that their model (which is a very general one) is equivalent to a universal Turing machine, and the problem to solve it is equivalent to the Turing machine entering a final state.

9. McCullough, D. and et. al., "Romulus: a computer security properties modeling enviroment. The theory of security", Technical Report RL-TR-91-36, Vol IIa, Rome Laboratory (Air Force Sys. Command), april 1991. Pages 3-20. A detailed and deep treatment of the paper by Goguen and Meseguer, combined with a deep study of cover channels and composition of (nondeterministic) MLS systems.

10. Zakinthinos, A. and E. S. Lee, "A general theory of security properties", Proceedings of the IEEE Symposium on Security and Privacy, may 1997. Another general approach to computer security theory. Here, the author's objective is to define what a security property is in the sense of the Alpern-Schneider safety-liveness framework (next paper). Particularly, they give a definition for security properties in terms of traces (much like CSP) and show that, under this definition, a security property is not a liveness nor a safety property. Also, they show that the most important properties of security (noninference, noninterference, etc.) fall into their definition.

11. Alpern, B. and F. Schneider, "Defining liveness", Information Processing Letters, 21:181-185, october 1985. An optional paper. A foundational paper about the theory of system specification.

12. Abrams, M., and H. Podell, and S. Jajodia, Information Security-An Integrated Collection of Essays, IEEE Computer Society Press, 1995. Pages 672-732. A glossary of commonly used terms of computer secuirty.