Report on The Computer Security Foundations Workshop VI

                      James W. Gray, III 
                Department of Computer Science
        Hong Kong University of Science and Technology
             Clear Water Bay, Kowloon, HONG KONG

The Computer Security Foundations Workshop VI was held during June
15--17, 1993 in Franconia, New Hampshire.  This is an annual workshop
with the purpose of ``bring[ing] together researchers to explore
fundamental issues in computer security'' [13].  Every year since its
inception, the workshop has been limited to forty participants, the
majority of whom present papers or speak on panels.  The setting is
informal with plenty of time for technical discussion.

This year, the program chair was Catherine Meadows.  The program
included sessions on covert channel analysis, information flow,
integrity and aggregation, access control, and crypto protocol
analysis.  Also included were an invited talk by Gus Simmons, two
panel discussions, and a report on the Cambridge crypto protocols
workshop held earlier this year.

The proceedings of the workshop are available from:

  IEEE Computer Society Press
  10662 Los Vaqueros Circle
  PO Box 3014
  Los Alamitos, CA 90720-1264

The first morning of the workshop---Tuesday morning---started off with
the session on covert channel analysis.  (For a description of covert
channels, see [8] or [9].)  This session consisted of two papers.  The
first paper, ``On Analyzing the Bus-Contention Channel Under Fuzzy
Time'' by the present author, analyzes the bus-contention channel---a
covert channel that can be exploited at a rate exceeding 1000 bits per
second---under the fuzzy time countermeasure, which was developed at
DEC.  The analysis provides the best known upper bound on the capacity
of the bus-contention channel under fuzzy time (viz, 22 bits per
second) and also provides a tradeoff between clock accuracy and covert
channel capacity.

The second paper, ``The Concurrency Control and Recovery Problem for
Multilevel Update Transactions in MLS Systems'' by Amit G. Mathur and
Thomas F. Keefe, addresses the problem of providing both security and
correctness in a multilevel secure database management system.  In
particular, the authors show that no scheduler can ensure atomicity of
multilevel update transactions in the presence of transaction aborts
and at the same time be secure.  The authors go on to describe and
compare two possible approaches to this dilemma, both of which contain
covert channels.  The authors then analyze the two covert channels and
offer their analysis as a basis for comparison of the two approaches.

The second session of Tuesday morning was on information flow.  The
first paper was ``Modeling Restrictive Processes that Involve Blocking
Requests'' by David Rosenthal.  In this paper, the author considers
the problem of proving restrictiveness (see [10] for the definition of
restrictiveness) of the composition of a set of client processes and
server processes, where the clients block on their requests to the
servers.  He defines two properties, client restrictiveness and server
restrictiveness and proves that if all of the clients satisfy client
restrictiveness and all of the servers satisfy server restrictiveness,
then the composition (when the processes are hooked up in an
appropriate way) satisfies restrictiveness.

The next paper was ``Information Flow Control in a Parallel Language
Framework'' by Jean-Pierre Banatre and Ciaran Bryce.  In this paper,
the authors develop a logic for reasoning about information flow
between program variables in programs written in Hoare's Communicating
Sequential Processes (CSP) (viz, Hoare's original version of CSP [7]).
The authors also give an operational ``flow semantics'' for the
language, which they intend, in later work, to use to prove the
soundness and completeness of their logic.  A parallel language with
message passing, and in particular CSP, allows information to flow in
various indirect and subtle ways.  This paper brings these subtle
flows to light and provides an interesting approach to reasoning about
them.

The final paper in the information flow session was ``A Logical
Formalization of Secrecy'' by Frederic Cuppens.  In this paper,
Cuppens extends the work begun in [1].  He argues that a previous
definition, causality, is a pessimistic definition of security in that
it may rule out some systems that are secure, but every system that
satisfies it is covert channel free.  He also gives a new definition,
non-disclosure, and argues that it is an optimistic definition of
security in that it does not rule out any covert-channel-free systems,
but some systems that satisfy it may have insecure refinements or
noisy covert channels.  The paper also describes how the two
definitions could be used together.

Tuesday afternoon started off with the session on Integrity and
Aggregation, the first paper of which was ``A Lattice of Information''
by Jaisook Landauer and Timothy Redmond.  This paper pursues the idea
of defining information (about the state of a given system) as an
equivalance relation on the state of the system.  Knowing the
information represented by a given equivalence relation can be
intuitively regarded as knowing which equivalance class the system is
in.  This idea has been explored since as early as 1986 [14].  The
present paper takes the idea further by giving an ordering on the set
of all equivalence relations that yields a complete lattice.  The
paper then shows the relationship between this lattice and some issues
in multilevel security, including the Unwinding Theorem [6] and
certain aggregation problems (see e.g., [5] for a discussion of
aggregation problems).

The second paper of the Integrity and Aggregation session was
``Automated Support for External Consistency'' by James G. Williams
and Leonard J. LaPadula.  In this paper, the authors address the
difficult problem of ensuring that a given system's outputs are
consistent with the external environment.  For example, if an
automated teller machine outputs the statement that a certain account
contains $10, then that account should actually contain $10.  They
call such requirements external-consistency requirements.  Clearly,
there must be some informality in any proof that a system satisfies an
external-consistency requirement.  However, the authors make some
progress by focusing on the decomposition of external-consistency
requirements into system requirements and user responsibilities.  For
example, a system might satisfy the above external-consistency
requirement, given that all account transactions made via human
tellers are properly input to the system (i.e., given that the user
responsibilities are satisfied).

The first day of the workshop concluded with a panel organized by Mary
Ellen Zurko called ``What are the Foundations of Computer Security?''.
Panel participants were invited to give their views on the progress
that has been made since the first Computer Security Foundations
Workshop in 1988 and on what remains to be done.  The panel consisted
of John McLean, Jonathan K. Millen, Robert Morris, and Marv Shaefer.
Their position statements appear in the workshop proceedings [12].

The first session on Wednesday was on access control, the first paper
of which was ``A Petri Net Representation of the Take-Grant Model'' by
Marc Dacier.  This paper gives a Petri net representation of the
Take-Grant model [2].  Then the paper gives a linear time algorithm
(using the Petri net representation) for finding all rights that a
given subject can obtain with a given set of conspirators.

The next paper in this session was ``On Testing for Absence of Rights
in Access Control Models'' by Ravi S. Sandhu and Srinivas Ganta.  In
this paper, the authors show that augmenting the Typed Access Matrix
(TAM) model with the ability of subjects to test for the absence (as
well as the presence) of rights does not add any expressive power to
the model.  They do however argue that augmenting the model in this
way is useful in practice.

The next session on Wednesday morning started off with a report on the
Cambridge Cypto Protocols Workshop, by Mark Lomas, in which he
summarized the presentations and discussions of that workshop.  The
report does not appear in the proceedings of the present workshop.
Following Mark Lomas' report, Gus Simmons gave an invited talk on
``The Mathematics of Trust in Security Protocols''.  A paper
accompanying the talk ``An Introduction to the Mathematics of Trust in
Security Protocols'' appears in the proceedings [12].  In the paper,
Simmons describes a lattice of ``concurrence schemes'', where a
``concurrence'' is a set of users that are required to act jointly to
exercise some function (as in, e.g., the separation of duty
requirements of [4]).  This lattice has been explored previously by
McLean in [11], but Simmons describes some new applications of the
lattice including the analysis of the effects of trusts held by
cryptographic protocol participants.

The first session on Wednesday afternoon was on crypto protocol
analysis and consisted of three papers.  The first paper was Li Gong's
``Variations on the Themes of Message Freshness and Replay''.  This
paper informally surveys the various mechanisms that are used to
validate message freshness (i.e., to determine whether or not a given
message was recently generated) and the various forms of replay
attacks (i.e., attempts to subvert the protocol by replaying old
messages).  Gong also argues that due to the wide variety of such
mechanisms and attacks, it would be difficult to develop a single
formalism that could be used to reason about all of them.

The next paper was ``Abstract Machines for Communication Security'' by
Pierre Bieber, Nora Boulahia-Cuppens, Thomas Lehmann, and Erich van
Wickeren.  In this paper, the authors make use of a existing formal
language, B, and associated automated tools to specify and reason
about cryptographic protocols.  The main novelty of the paper is the
modular style in which they develop their specifications and proofs.
For example, there is one module that describes the way messages are
passed between subjects in the system; this includes actions for the
legitimate participants as well as actions that penetrators can
perform in an attempt to subvert the system.  Another module describes
the properties of the cryptosystem being used.  Still another module
describes the cryptographic algorithm under consideration.  The
authors claim that structuring the specification in this way allows
them to reuse specifications and proofs in the verification of
additional protocols.

The last paper in this session was ``Towards Formal Analysis of
Security Protocols'' by Wenbo Mao and Colin Boyd.  This paper
addresses two shortcomings of the BAN approach (see [3]) to
authentication protocol analysis: (1) the authors propose a method for
formalizing much of the ``idealization'' process (wherein an informal
statement of the protocol is transformed into a formal one); and (2)
the authors provide inference rules for reasoning about the
``confidentiality'' of cryptographic keys.  This latter concern is
crucial since a compromised key (i.e., one that is known to a
penetrator) is no longer usable for authentication purposes.

The final technical event of the workshop was a panel organized by
Paul Syverson on ``Cryptographic Protocol Models and Requirements''.
Panel participants were invited to give their views on questions such
as the following.  How are cryptographic protocol requirements
dependent on the model of computation?  Should we attempt to develop
formal languages to reason about requirements?  And what kinds of
models and requirements should we focus on?  The panel consisted of
Whitfield Diffie, Catherine Meadows, Michael Merritt, Gus Simmons, and
Einar Snekkenes.  Their position statements do not appear in the
workshop proceedings.

The workshop closed with a business meeting on Thursday morning at
which plans for next year's workshop were discussed.  For next year,
the general chair will be Ravi Sandhu and the program chair will be Li
Gong.  For further information about next year's workshop, contact
Ravi Sandhu (email preferred):

  ISSE Dept., George Mason U, Fairfax, VA 22033
  voice: 703-993-1659, fax: 703-993-1638
  email: sandhu@isse.gmu.edu or sandhu@sitevax.gmu.edu 

References

[1] P. Bieber and F. Cuppens.  A logical view of secure dependencies.
Journal of Computer Security, 1(1):99--129, 1992.

[2] M. Bishop and L. Snyder.  The transfer of information and
authority in a protection system.  In Proceedings of the 7th ACM
Symposium on Operating System Principles, pages 45--54, Pacific Grove,
CA, 1979.

[3] Michael Burrows, Martin Abadi, and Roger Needham.  A logic of
authentication.  ACM Transactions on Computer Systems, 8(1):18--36,
February 1990.

[4] David D. Clark and David R. Wilson.  A comparison of commercial
and military computer security policies.  In Proceedings of the 1987
IEEE Symposium on Security and Privacy, pages 184--194, Oakland, CA,
April 1987. IEEE Computer Society Press.

[5] Dorothy E. Denning, Selim G. Akl, Matthew Morgenstern, Peter G.
Neumann, Roger R. Schell, and Mark Heckman.  Views for multilevel
database security.  Proc. 1986 IEEE Symposium on Security and Privacy,
pages 156--172, April 1986.

[6] Joseph A. Goguen and Jose Meseguer.  Unwinding and inference
control.  In Proceedings of the 1984 IEEE Computer Society Symposium
on Security and Privacy}, Oakland, CA, 1984.

[7] C.A.R. Hoare.  Communicating sequential processes.  Communications
of the ACM, 21(8):666--676, August 1978.

[8] Richard A. Kemmerer.  Shared resource matrix methodology: An
approach to identifying storage and timing channels.  ACM Transactions
on Computer Systems, 1(3):256--277, August 1983.

[9] Butler W. Lampson.  A note on the confinement problem.
Communications of the ACM, 16(10), October 1973.

[10] Daryl McCullough.  A hookup theorem for multilevel security.
IEEE Transactions on Software Engineering}, 16(6):563--568, June 1990.

[11] John McLean.  The algebra of security.  In Proceedings of the
1988 IEEE Symposium on Security and Privacy, Oakland, CA, May 1988.
IEEE Computer Society Press.

[12] Proceedings of the Computer Security Foundations Workshop VI,
Franconia, NH, June 1993. IEEE Computer Society Press.

[13] Ravi Sandhu.  Preface.  In Proceedings of the Computer Security
Foundations Workshop VI, page v, June 1993.  Available from the IEEE
Computer Society Press.

[14] David Sutherland.  A model of information.  In Proceeding of the
9th National Computer Security Conference, Baltimore, MD, September
1986.

Note: conversion to text was done by Li Gong from LaTeX source
supplied by Jim Gray.