[an error occurred while processing this directive]
[an error occurred while processing this directive]
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.
References:
| [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]