Summary of the 7th IEEE Computer Security Foundations Workshop Li Gong Program Chair of CSFW-7 SRI Computer Science Laboratory Menlo Park, California 94025, U.S.A. (gong@csl.sri.com) August 3, 1994 The 7th IEEE Computer Security Foundations Workshop (CSFW-7), as all previous workshops in this series, was held in the scenic mountain setting of Franconia, New Hampshire, U.S.A., June 14-16, 1994. This year, the number of paper submissions increased significantly from the past two years, and the number of participants was close to the conference capacity of the Franconia Inn. Such prosperity is no doubt due to the hard work on the part of the workshop organizers (Ravi Sandhu of George Mason University being the General Chair), the program committee members, the authors, and the participants. The general feeling was that this year's gathering was much more lively than previous years, and the presence of Bob Morris was instrumental. There were 7 technical sessions, including 2 panel discussions. The first session, ``Non-Interference and Composability'', was chaired by Ravi Sandhu, who stepped in to replace Jose Meseguer (SRI) who could not attend. Jonathan Millen (MITRE) presented his paper ``Unwinding Forward Correctability'', in which a state-machine formulation is given for forward correctability in event systems, an unwinding result is given for this type of information flow property, and regular-expression notation is shown to provide an easy tool for mechanical verification of small systems. Next, William Bevier (Computational Logic, Inc.) presented a paper entitled ``A State-Machine Approach to Non-Interference'' (coauthor William Young, CLI) in which a state-machine approach (as opposed to the traditional event-system approach) is used to model noninterference-style policies. The authors feel that this new approach is richer and more intuitive and provides a link to other research in the specification and verification of concurrent and distributed systems. Finally, George Dinolt (Loral Western Development Labs) presented ``Combining Components and Policies'' (coauthors Lee Benzinger and Mark Yatabe, Loral WDL), which proposes a mathematical model for describing both composable policies and system properties that can be obtained by composing components that individually may or may not satisfy a desired system property. After the initial rounds of the mandatory croquet tournament, efficiently organized by Ann Morris as in past years, we returned to the next session called ``Formal Models and Semantics'', chaired by Simon Foley (University College, Cork, Ireland). The first paper was by Carol Muehrcke (Secure Computing Corporation) entitled ``Formal Methods for the Informal World'', which gives examples of the necessity and benefits for formalizing concepts of the environment within which a secure system functions, in addition to applying formal methods to the secure system itself. Next, Adrian Spalka (University of Bonn) presented his paper ``Formal Semantics of Rights and Confidentiality in Definite Deductive Databases'' in which he gives four interpretations of secrecy and identifies conditions that guarantee that the introduction of rights and confidentiality requirements does not affect the database semantics. Lunch break and more croquet were followed by a ``Model(l)ing'' session, commanded by Stewart Lee (University of Toronto). Oliver Costich (Naval Research Laboratory) presented the work (coauthors John McLean and John McDermott, also of NRL) on ``Confidentiality in a Replicated Architecture Trusted Database System: A Formal Model'', which presents a model of the SINTRA architecture (single-level backend database systems with a multilevel front-end system) and demonstrates that a high level of assurance can be obtained solely from replication with virtually no change to the structure of the underlying database systems or the security kernel. Next, Roshan Thomas (GMU) presented ``Conceptual Foundations for a Model of Task-based Authorization'' (coauthor Ravi Sandhu), which addresses integrity issues in computerized information systems from an enterprise perspective where the motivation is that existing models are too low-level to be useful for specifying properties such as organization requirements and policy aspects. The last session of the day was a panel on the so-called ``write-up'' problem, moderated by John McDermott, with Roshan Thomas, Ira Moskowitz (NRL), and Oliver Costich as panelists. The basic problem is how to organize information flow from a low level to a high level while achieving some degree of reliability, performance, concurrency control, and other desirable measures. The main difficulty seems to be how, without introducing (large capacity) covert channels, to acknowledge to the low level that a write-up has succeeded. Thomas proposed a concurrent computation model with multi-version synchronization for supporting synchronous write-up, Moskowitz described his secure Pump (which uses a trusted subject with a finite buffer), and Costich suggested replacing write-up with read-down. These ideas were hotly contested and defended. I suggested that injecting external random sources, and/or using a magic pump (possibly with a buffer of a varying length), might result in a cleaner implementation. None of the proposed methods can achieve all the goals, which Bob Morris pointed out are beyond normal expectations anyway. He suggested that one must trust that his prayer is (always) heard by God, and it is quite unreasonable for one to demand an acknowledgment from God before he prays again. And that seems to have capped the whole discussion. The Canadian contingent (led by Professor Lee from Toronto) was relatively polite during the panel session, but carried the heat and light well into the evening when the Vancouver Canucks were beaten by the New York Rangers 4:3 in the Stanley Cup final (ice hockey). The first session on the second day was ``Cryptographic Protocol Analysis'', chaired by Virgil Gligor (University of Maryland). The first paper was by Catherine Meadows (NRL) on ``A Model of Computation for the NRL Protocol Analyzer'' in which she compares the new model with the Abadi-Tuttle model of the BAN logic and discusses issues with respect to integrating the BAN approach and the more traditional state-machine approach. Next, Volker Kessler (Siemens) presented a paper ``AUTLOG -- An Advanced Logic of Authentication'' (coauthor Gabriele Wedel, RWTH Aachen), which describes a modified version of the BAN logic that is implemented in Prolog. Finally, Aviel Rubin (Bellcore) presented ``Nonmonotonic Cryptographic Protocols'' (coauthor Peter Honeyman, University of Michigan), which describes a new method for analyzing protocols that depend on the (proper) deletion of information. The method was used to discover a previously unknown flaw in the {\em khat} protocol developed by the authors. The next session was on ``Security Policies'', chaired by John McLean. Ramesh Peri (University of Virginia) presented a paper ``Formal Specification of Information Flow Security Policies and Their Enforcement in Security Critical Systems'' (coauthor William Wulf, also of UV), where a semantic approach is proposed for incorporating the security specification in the functional specification of a system (by restricting the behaviors of entities in the system) and for proving that the resulting specification has the required security properties. Then, Roberto Gorrieri (coauthor Riccardo Focardi, both of Universit\`{a} di Bologna) spoke on ``A Taxonomy of Security Properties for CCS'' in which CCS is enriched with security notions so that several of the published information flow security properties can be interpreted and their relative merits compared. The first session in the afternoon was on Access Control, chaired by Joshua Guttman (MITRE). The first paper, ``One-Representative Safety Analysis in the Non-Monotonic Transform Model'', was presented by Paul Ammann (coauthor Ravi Sandhu, both of GMU) in which the authors have identified (within the NMT model whose safety problem is decidable) a class of schemes for which the safety problem is tractable in that the complexity depends (still exponentially) on the number of types (of subjects) in the system but not on the actual number of subjects. Then Simon Foley talked on ``Reasoning about Confidentiality Requirements'', which is about using reflexive flow policies to construct complex multilevel policies by specifying a precise relationship between a multilevel policy and the system entities (which can then be transformed into lattice-based policies). He argued that this approach is conceptually easier than directly developing lattices plus bindings, and also forms a basis to better reason about policies (especially policy change and composition). Energized by soft drinks, food, and more croquet, we returned to the second panel session, on ``Redrawing the Security Perimeter of a Trusted System'', moderated by Dan Sterne (Trusted Information Systems), with Len LaPadula (MITRE), Ravi Sandhu, Carl Landwehr (NRL), and Glenn Benson (TIS) as panelists. Benson started by expressing the view that between TCBs and totally untrusted application codes there should be a middle layer of software called Controlled Application Set (CAS) that is not as thoroughly vetted as the TCB but is nevertheless somewhat trustworthy, e.g., by the nature of its development environment (say by a trusted company). The discussion that followed was so frenetic (and complete with catcalls) that it is probably unsafe to attribute any view to any named individual without separate verification (which is impossible for this summary). Some people supported the CAS view. Some others thought that the CAS was merely an enlarged TCB, thus the approach offered no new insight. Still others thought although CAS and TCB were not the same thing, it was better to spend the limited amount of money on TCB instead of CAS, though some countered that we were not playing a zero-sum game. It was also suggested that similar things were all done before, but were prevented from publication. The panel served well as a preparation for the evening that was just as stormy when the Houston Rockets lost to the New York Knicks in the fourth game of the NBA finals. Peace and calm returned in the last morning, with a session on Protocol Security, chaired by Michael Merritt (AT\&T Bell Labs). The first paper, ``Development of Authentication Protocols: Some Misconceptions and a New Approach'', was given by Wenbo Mao (coauthor Colin Boyd, both of University of Manchester, UK) in which the authors propose the separation of authentication and secrecy concealment in cryptographic protocols and also give examples of poor choice of cryptosystems and misuse of redundancy. Protocol specification techniques are suggested to address these issues. The next paper was by Paul Syverson (NRL) on ``A Taxonomy of Replay Attacks'' where the taxonomy is in terms of message origin and destination and is complete in that any replay attack is composed entirely of elements classified by the taxonomy (as opposed to previous works where replay attacks were listed but not as systematically organized). The last technical paper of the workshop was given by Ulf Carlsen (Telecom Bretagne, France) on ``Cryptographic Protocols Flaws'' where flaws in protocol design were grouped (e.g., under the headings of elementary flaws, oracle flaws, and type flaws) and counter-measures discussed. Ulf also had the last say in croquet by beating Ann Morris in the final. As usual, the last item on the workshop agenda was the workshop business meeting (open to all), where reactions to this year's workshop were solicited and future plannings discussed. It was decided that the 8th workshop (CSFW-8) will be held in Kenmare, County Kerry, Ireland, and that Simon Foley (s.foley@cs.ucc.ie) will be the General Chair. I will continue to serve as Program Chair (the tenure of the position is limited to two terms) and Joshua Guttman kindly agreed to continue as Publications Chair. The workshop dates will be from June 13 to 15, 1995, with due dates as follows: paper submission (five copies to me) due February 3, 1995; notification of acceptance by March 14; and camera-ready final versions by April 11. In reproducing the Franconia atmosphere that has become the trade mark of this workshop series, Simon successfully located the magnificent Dromquinna Manor (built in 1850), which is situated in its own private grounds with 42 acres of woodland and lawns that sweep down to 0.75 miles of sea frontage. Dromquinna is ideal for activities such as walking, boating, fishing, swimming (sea), tennis, cricket, croquet, and is situated near the border of Counties Cork and Kerry, which claim some of the most varied and spectacular scenery and tourist attractions in Ireland, including Charles Fort Kinsale, Bantry House and Gardens, Blarney Castle, Killarney National Park, Lough Hyne, Ilnaculin Island, Gallarus Oratory, and many more. There are direct flights from the east and west coast of the US to Dublin/Shannon and connecting flights to Cork, as well as direct flights to Cork from major European cities such as London and Amsterdam. Connections from many other cities can be best made by using London or Amsterdam or by availing of the scheduled services from Dublin to Cork. There are also car/passenger ferries from the United Kingdom and Europe to Cork, Dublin and Rosslare. Workshop cost (fee plus lodging and meals) is estimated to be similar to that at Franconia. The Franconia workshop is never complete without the full participation of the US Immigration and Naturalization Service (INS). For three years running, the INS had reliably set up road blocks on I-93, the only major highway between Franconia and Boston, on the last day of the workshop. Although they supposedly chose 3 days at random each year to do ID checks, they must be delighted at repeatedly capturing an unusually large number of Europeans. This year I (being a Chinese) was stopped by the same INS officer who stopped me in all previous years. He instantly recognized me and waived the check on the basis of last year's satisfactory outcome. I wanted to recommend to him the two workshop papers on non-monotonicity but then thought that the INS was probably not the best testing ground for new research ideas. Maybe the haunt of the INS was the real reason for changing the workshop venue? Notes. 1. The workshop proceedings (including past and future ones) are available from IEEE Computer Society Press, 10662 Los Vaqueros Circle, P.O. Box 3014, Los Alamitos, CA 90720-1264, (email cs.books@computer.org), with order number 6230-02. 2. Peter G. Neumann of SRI and some workshop participants made very helpful comments on drafts of this summary, but all errors and inaccuracies remain mine.