14th Computer Security Foundations Workshop CSFW 2001
Cape Breton, Nova Scotia, Canada, 11-13 June 2001
Review by Geraint Price

The fourteenth Computer Security Foundation Workshop (CSFW 2001) was held in an idyllic location at Keltic Lodge on Cape Breton in Nova Scotia. Although the travel was lengthy the location and isolation led to a definite closed community feel to the workshop, which is very much in keeping with the goals of the steering committee. The isolation of the hotel and its surrounding facilities lent itself naturally to the feeling that you had come away from it all to get to grips with the workshop.

Every session was well attended, with the lawn outside the conference room providing excellent opportunity to converge during the coffee breaks, discuss the work, and also bask in the fortunately clement weather with which we were provided.

The first session was based on Information Flow theory.

Sylvan Pinsky: Noninterference Equations for Nondeterministic Systems: This talk was well presented and was based on the notion that deterministic and nondeterministic finite state machines are in fact equivalent. There was comment from the floor that similar work had been started in past research, but that one difficulty posed by using the state machine approach in these scenarios was the speed at which state space explosion became a problem.

Steve Zdancewic: Robust Declassification: The basic premise of this paper was to make a distinction between intentional and unintentional information flow. The author's intention was to demonstrate that declassification of sensitive material was an intentional leakage of information. The overriding claim made was the implicit connection between the integrity of a data object and its confidentiality, the notion being that a surreptitious disruption of the integrity of an object could compromise the confidentiality of the object as an unintentional effect. A few questions were raised with regards to the usage of a log-in password mechanism as a vehicle for demonstrating the concept, but on the whole the basis for discussion had merit.

The second session was based around Access Control.

Ajay Chander: A State-transition Model of Trust Management and Access Control: This talk provided a novel modeling of different types of trust management. They specifically model and derive the relationships between (i) Access Control Lists (ii) Capability based methods (iii) Localized Trust Management - such as those developed in the KeyNote system developed by Blaze et al. The state based system they use is expressive in abstracting the relations between client and object away from the details of each category. A small set of slides where the results - and hence the relationships - were shown in graphical form made it very easy to follow the result (and with the title "A picture paints...", it drew a laugh from the audience). A novel piece of work that clears up the equivalence between ACL and capabilities.

Asa Hagstrom: Revocations - a Classification: The outline of this talk was to study the temporal difference between what they term positive and negative access permissions. Their re-calculation of permission chains in the light of new rights close to the source of the chain provides us with an easy means of letting revocation percolate throughout the system. There was concern from the floor about the absolute nature of the negative rights represented in the paper, and that their model lacks the expressiveness for such things as a hierarchy of users.

Joseph Halpern: A logical reconstruction of SPKI: This talk presented a formal analysis of the SPKI/SDSI system of public key certificates put forward by Rivest and Lampson. There was some confusion as to whether this was an extension of the SPKI/SDSI environment, but the speaker cleared up that it was purely an analysis. The authors extend some of their earlier analyses to include expiry in the certificates. Their analysis of reduction rules in SPKI concludes that they need to be enhanced to allow for more complete reasoning about certificates.

The third session was based on Protocols.

Olivier Pereira: A Security Analysis of the Cliques Protocol Suites: This paper presents the outline of a model for analysis of Diffie-Hellman based group key-agreement protocols, and demonstrates this by using it to analyse the Cliques protocols. An interesting topic of discussion due to the analysis of the protocol when players are added or deleted to the group. This itself presents a major headache when it comes to analysing the forward secrecy properties of the protocols.

Bruno Blanchet: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules: As noted in the title, the speaker presents a new protocol analyser based on Prolog rules. While a few of these have appeared in the literature before, the main advancement put forward was a new solving algorithm that limits the number of runs in a protocol. They presented a list of run times to demonstrate that this made their analyser very efficient in its search time - although comment from the floor questioned the need for program run times in a conference on theory, the answer was an honest: "Because all other automated model checking papers have them!".

Veronique Cortier: Proving secrecy is easy enough: This talk introduced a state-based analysis of security aimed at proving the secrecy of the protocol. They encapsulate the notion of secrecy in terms of "occultness" which they present as a means of deciding if states can be generated that reveal secrets. They noted that under the assumptions they use that they might not be able to prove a protocol secure in some cases where it is actually secure.

The fourth session was a panel discussion entitled "Relating Cryptography and Cryptographic Protocols": This panel brought together a nice mix of theory and practical experience. The final panel line up was slightly different to that presented in the proceedings, with the panel consisting of David Wagner, Martin Abadi, Ran Canetti and Joshua Guttman. The overall discussion focussed on the gap that exists between analysis of protocols in theoretical models and their use for analysis by real world implementors of security systems. The main conclusion drawn was that there was much scope for work on building tools that made secure protocol analysis more accessible to those who really need to use it. The highlight of this sales pitch in my opinion came from David Wagner of U.C. Berkeley. Starting off by apologising for any flaws in protocol analysis he made due to not being an expert, he went on to present three independent protocol designs which while standing on their own were child's play for picking holes in, and each individually raised a laugh from the audience. He concluded by demonstrating how these flaws in combination made it possible for him and others at Berkeley to break the IEEE 802.11 WEP protocol.

The fifth session was the interaction of Information Flow and Type Systems.

Geoffrey Smith: A New Type System for Secure Information Flow: The morning of the second day started with an interesting talk on type systems in multi-threaded programs. The basis for the talk was analysis of information leakage within the scheduler of a multi-threaded program which contains high and low variables. The analysis is not of the scheduler itself but of possible interactions between threads if we assume a fair scheduler. The analysis comes down to the guards used in loops, and whether they are high or low variables. He demonstrates that for probabilistic noninterference to be guaranteed, threads that are contaminated with a high while loop need to be separated from other threads from that point onwards.

Andrei Sabelfeld: A Generic Approach to the Security of Multi-Threaded Programs: This talk gave an overview of the integration between security properties of programming languages and abstract level properties of information flow. The model used for the information flow properties is the one that the co-author (Heiko Mantel) presented at CSFW 2000. Offering this integration between communicating processing in the distributed sense along with local information sharing in the programming sense provided an interesting overview of how models of different security properties could be combined to increase the relative power of their analysis.

The sixth session was a second look at Protocols.

Alan Jeffrey: Authenticity by Typing for Security Protocols: This talk looked at using type based language checking as a means of analysing the security of protocols after they had been represented using the Spi calculus (itself developed by Andy Gordon, a co-author on the paper). The method used for typing provided a very neat means of encapsulating the safety property usually associated with the use of nonces.

Marcelo Fiore: Computing Symbolic Models for Verifying Cryptographic Protocols: The presentation overviewed the use of symbolic techniques to tackle the problem of infinite-state systems that arise when trying to analyse even seemingly most simple cryptographic protocols. This seems an interesting avenue for exploration, due to the problems of state explosion faced by many methods for analysing cryptographic protocols.

Michael Rusinowitch: Protocol Insecurity with Finite Number of Sessions is NP-complete: This talk gave a view of the complexity of deciding the analysis of checking various modes of cryptographic protocols. Even when limiting the number of sessions they were able to demonstrate NP-Completeness of the result.

The seventh session covered Intrusion Detection.

Francesco Parisi-Presicce: Multi-Phase Damage Confinement in Database Systems for Intrusion Tolerance: Unfortunately the speaker on this occasion was not one of the authors of the paper. The session chair gave note after the talk that he was thus at liberty not to answer any of the questions. The overall model of the system aimed to highlight the difficulty in maintaining availability and safety in a database system which had a known compromise. Reducing the set of possible damaged elements is the key to increasing availability. They note that assessment latency was a key factor in determining which parts of the database were potentially compromised. The means of building their recovery tree is based on a multi-phase recovery process where parts of the database are unconfined early depending on the type of the objects in the database, thus aiming to reduce the latency in relaxing the recovery set, and hence increase availability. A novel idea, and it was slightly unfortunate that the authors were not present to elucidate further, even though an excellent job had been done in presenting this from scratch.

Somesh Jha: Markov Chains, Classifiers, and Intrusion Detection: This talk started off with an interesting overview of different methods of Intrusion Detection highlighting the difference between pattern based (rule based) intrusion detection, and statistical based intrusion detection. After highlighting the usual downfall characteristics of pattern based variants they proposed a novel use of Markov Chain models in order to detect potentially anomalous behaviour. Their model uses an intuitively satisfying pattern checking method within the Markov model for raising alarms.

Muriel Roger: Log Auditing through Model-Checking: The speaker presented a means of analyzing intrusion detection logs by using a model checker to check signature patterns independently of implementation details.

The eighth session was a panel discussion entitled "Non-interference: Who Needs It?": This was by far and away the most eagerly anticipated session of the Workshop. Peter Ryan appeared to have come up with an ideal topic to throw the discussion into hostile territory. Unfortunately this session failed to live up to its billing. Although this was not a waste of time at all and the speakers - John McLean, Jon Millen and Virgil Gligor - put forward some very persuasive arguments, the sting in the tail was missing. Paul Syverson tried to provide a voice of objection, but failed to get a bite. The overall tone of the panel was summed up efficiently by McLean's assertion that only by understanding the fundamental principles of security such as non-interference could we then hope to move on and make proper and complete analysis of security systems.

The ninth session was based on logics for protocol verification.

Nancy Durgin: A compositional logic for protocol correctness: What was presented here was an extension to a BAN-like analysis, by adding a means for inference rules to be described in order to capture the actions in a protocol. Cathy Meadows asked why this tool should be used above others. The answer was succinct, in that the method put forward here aims to take the sting out of the protocol idealization phase, with its notorious pitfalls.

Eijiro Sumii: Logical relations for Encryption: This presentation demonstrates another means of assessing security protocols based on type mechanisms rather than the message passing semantics (as used in the Spi-calculus).

The final session was based on Secrecy & Privacy. Unfortunately due to travel constraints I had to cut short this session, getting a lift back across country to the airport.

The papers at Cape Breton presented a mix of the old and the new. Comments were made about the links between topics that had come up in some of the first CSFW meetings, along with people bringing in new ideas from areas such as language based systems. It was - as last year - an interesting place to talk through ideas, with plenty of opportunity to spark up questions during the intervals. I was party to a discussion between some of the organising committee during the first evening, where concern was expressed over the rapid growth of the workshop. From my point of view bringing in new blood seems important to make sure that the lessons learned in these workshops trickle out to the wider audience, but I do agree that moving to enlarge the conference too much could hamper with the very open attitude to discussion experienced in what was a very thought provoking few days. Good luck to those next year in achieving the same balance.

Those interested in the workshop further can find copies of the program, slides of most of the talks, some picture, etc., at the following URL:   www.csl.sri.com/programs/security/csfw/csfw14/

Finally, the croquet tournament was better this year for the lack of rain!