[an error occurred while processing this directive] [an error occurred while processing this directive]

A Formal Security Model for Message Handling Systems

Master Thesis, University of Kaiserslautern, 1993

Extended abstract:

Information has become a pervasive. Exchanging information is a necessity for most businesses. One way of tranporting information is through electronic mail in Message Handling Systems (MHS). Prototypes of such systems exist since the beginning of the DARPA project. Initially these systems have been used primarily within the academic community. Due to the continuing growth of digital networks individuals and commercial groups gain access to a MHS.

The need for standardization of a MHS had been recognized since the early eighties. Accordingly in 1984 a standard was published by the CCITT (Comite Consultatif International de Telegraphique et Telephonique) known as the X.400 recommendations. Despite the broad acceptance of the X.400 recommendations, the lack of approriate security mechanisms, like the warranty of the privacy of messages, has been viewed as a major drawback. In 1988 a revised version of X.400 was published which introduced a variety of security service elements.

To insure security of service elements the complexity of systems for the exchange of electronic messages plays an important role. Providers of communication systems have to prove the quality of their products through certificates, which are given out by independant and trustworthy institutions. In 1989 the Bundesamt für Sicherheit in der Informationstechnik (BSI) has published criteria for the evaluation of the security of information systems. With the help of those security criteria an information system can be evaluated and assigned one of eight quality levels called Q0 to Q7. The higher levels of quality reflect increased demands on the required security of information systems. For the quality level Q7 the BSI requires a formal security model as well as a proof of the consistency of that model (see [BSI89], page 93).

A security model provides an abstract model of the security functions of a system. The informal representation of such a model corresponds to a list of requirements, which serve as a foundation for the implementation of the system. An informal notation has several drawbacks. Firstly, an informal notation results in inter-vendor problems due to the unprecise semantics of natural language descriptions. Secondly, such informal descriptions are not machine readable. For those reasons the BSI requires a formal notation for quality level Q7. The BSI defines a formal model as follows (see [BSI89], page 101):

Definition: ``A formal model consists of a set of abstract objects with functions, which adhere to a set of axioms. The predicate calculus may serve as a foundation for a formal model. A model is derived through the process of abstraction from reality. A model is accessible to mathematical manipulations.''

Up to now a formal security model for MHS does not exist. Discussions in recent publications are limited to informal security models (see e.g. [BRAN90], [FORD89] or [WHYM90]). Formal security models have only been developed for certain kinds of communication protocols. E.g. as part of the SIS-project a formal security model for the transport layer of the OSI-protocol stack was developed (see [SIS92]). In [CHENG90] a similar model is presented for a multiparty session protocol.

The goal of this thesis is to develop a formal security model for a MHS and to prove the consistency of this model. In chapter 2 an introduction to electronic mail system is given and an informal, generic model of a MHS is presented. This generic model serves as a basis for the subsequent chapters. It should be noted that the use of the term MHS differs from that in the X.400 recommendations. The case studies of existing MHS provide further insights in the properties of the generic model. In chapter 3 the threats that a MHS is being exposed to are examined. The informal security model presented in chapted 4 is an immediate result of this analysis.

The generic model as well as the threat analysis form the basis for the main part of this thesis. In chapter 5 the term security is examined and a formal representation of this term based on a generic sercurity model is given. The generic security model is derived from the Bell-LaPadula model (see [BLP76]), which is independant of the characteristics of an underlying physical system.

In chapter 6 a formal security model for a MHS is developed. This is done by defining certain restrictions on the generic model of a MHS presented in chapter 2. This in necessary to reduce the complexity of the formal security model. The main restriction results in the requirement of a physical protection layer which encapsulates the computings nodes in a network. Afterwards a formal notation is introduced which stems on a typed first order predicate calculus. Addendum A and B contain a precise definition of this formal notation.

In the remaining part of chapter 6 the formal security model is developed systematically. The informal descriptions of chapters 2 to 4 serve as a basis for this formal security model. It should be noted that the transformation from an informal to a formal notation is a creative process which leaves a certain amount of freedom in the design of the model. In that sense the resulting formal security model is not to be regarded as the model but rather one possible explication of the model. Addendum C contains the formal security model as a whole. Finally in chapter 7 the consistency of the model is proven.


[BLP76] D.E. Bell and L.J. LaPadula, ``Secure Computer System: Unified Exposition and Multics Interpretation'', MTR-2997, MITRE Corp., Bedford, MA, March 1976
[BRAN90] M. Branstad, W.C. Barker and P. Cochrane, ``The Role of Trust in Protected Mail'', Proceedings 1990 IEEE Symposium on Research in Security and Privacy, May 1990
[BSI89] Bundesamt für Sicherheit in der Informationstechnik (BSI), ``IT-Sicherheitskriterien: Kriterien für die Bewertung der Sicherheit von Systemen der Informationstechnik'', Bundesanzeiger, January 1989
[CHENG90] P.C. Cheng and V.D. Gligor, ``On the Formal Specification and Verification of a Multiparty Session Protocol'', Proceedings 1990 IEEE Symposium on Research in Security and Privacy, May 1990
[FORD89] W.S. Ford, ``Standards for Security in Open Systems'', Proceedings IEEE GLOBECOM, 1989
[SIS92] D. Maaß, ``SIS - Security Interoperability Sublayer'', Technical Report, University of Kaiserslautern, Regionales Hochschulrechenzentrum, 1992
[WHYM90] T. Whyman, ``X.400 security features'', Proceedings IEEE Colloquium on Security and Networks (Digest No. 114), London, June 1990
[an error occurred while processing this directive]