MONDAY June 28, 2004

8:45 - 9:00 WELCOME
George Dinolt (Naval Postgraduate School), General Chair
Riccardo Focardi (University of Venice), Program Chair

9:00 - 10:30 Protocols I
Session Chair: Jon Millen

A Theory of Dictionary Attacks and its Complexity
Stephanie Delaune, Florent Jacquemard (Laboratoire Specification et Verification)

In a dictionary attack, the attacker wants to confirm that his guess of a user's password is correct, by computing some term in two ways and comparing the results. This can be formalized by adding some inference rules to the attacker's capability. The approach is not new, but this paper proves for the first time that security in this model is NP-complete.

Generic Insecurity of Cliques-Type Authenticated Group Key Agreement Protocols
Olivier Pereira, Jean-Jacques Quisquater (UCL Crypto Group)

Cliques-type protocols create and distribute a common key among a group of arbitrary size. They exchange Diffie-Hellman exponentiated terms to a common base, authenticated between parties by including a pairwise shared key in the exponent. This paper shows the remarkable result that any protocol constructed this way can be attacked if the group has four or more parties.

Abstraction and Refinement in Protocol Derivation
Anupam Datta, Ante Derek, John Mitchell (Stanford University), Dusko Pavlovic (Kestrel Institute)

This latest paper in a series extends the protocol refinement process by allowing protocol "templates" with function variables. This approach does not affect proof difficulty, but it facilitates comparison between related protocols like some different proposed versions of JFK (a proposed standard key exchange protocol).

11:00 - 12:00 Access Control
Session Chair: Andre Scedrov

A Distributed Calculus for Role-Based Access Control Chiara Braghin (Universita' Ca' Foscari di Venezia), Daniele Gorla (Universita' di Firenze), Vladimiro Sassone (University of Sussex)

This is an application of pi-calculus to RBAC. An RBAC schema assigns possible roles to users and permitted access modes of roles to objects. A type system is set up whereby a successful type check implies that the schema is satisfiable by some nontrivial system in which each process is associated with a user and a role.

From Stack Inspection to Access Control: A Security Analysis for Libraries Frederic Besson (Microsoft Research), Tomasz Blanc (INRIA), Cedric Fournet, Andrew Gordon (Microsoft Research)

They have a tool to analyze code that must be trusted and is written in a subset of IL, the intermediate language for CLR (Common Language Runtime), the .NET analogue of bytecode on JVM. The tool generates a call graph and looks for various known problems. Thus, this method goes beyond stack inspection.

2:00 - 3:00
Intrusion Detection
Session Chair: Catherine Meadows

Selecting Appropriate Counter-Measures in an Intrusion Detection Framework; Frederic Cuppens, Thierry Sans, Sylvain Gombault (ENST Bretagne)

They formally define "anti-correlation" for this purpose and have implemented it in a system called DIAMS.

Using Active Learning in Intrusion Detection Magnus Almgren, Erland Jonsson (Chalmers University)

Active learning, in which an expert labels those training examples that are likely to improve the performance of the intrusion classifier, is shown to outperform the traditional self-learning substantially, both in accuracy and in the ability to train with less data.

3:30 - 4:30 Information Flow
Session Chair: Andrew Myers

Secure Information Flow by Self-Composition
Gilles Barthe (INRIA Sophia-Antipolis), Pedro R. D'Argenio (Universite de Provence), Tamara Rezk (INRIA Sophia-Antipolis)

Information flow is analyzed using an extension of Hoare logic called separation logic, used to reason about shared mutable data structures. This approach is more accurate than information flow based on type systems, can sometimes be sound and complete, and is amenable to mechanization.

Lenient Array Operations for Practical Secure Information Flow
Zhenyue Deng, Geoffrey Smith (Florida International University)

New simple and permissive typing rules are proposed for array operations, to enforce noninterference. (Information flow involving array indices can be subtle.)

4:30 - 5:30 Business meeting

The next CSFW will be held in Aix-en-Provence, France, near Marseilles. The program chair is Joshua Guttman, and the general chair is Roberto Amadio. There was considerable discussion about how to create a conference (rather than a workshop) for theoretical computer security. Oakland and ESORICs were deemed unsatisfactory, in their current mode. Growing CSFW had mixed reactions. A small, informal meeting has benefits, but greater access for students and researchers in related fields was considered important. Removing the "invitational" restriction is probably not harmful.

9:00 - 10:30 Security Policies
Session Chair: Andy Gordon

Owned Policies for Information Security
Hubie Chen, Stephen Chong (Cornell University)

The Myers-Liskov decentralized label model, in which each label is a set of (owner, reader-set) permission pairs, is extended so that a reader-set is replaced by a lattice of policy labels (like the combined mandatory sensitivity-integrity lattice proposed by Biba) and the owners are roles in an "acts-for" hierarchy. It is assumed that permissions of a role are included in higher roles.

Cassandra: Flexible Trust Management, Applied to Electronic Health Records
Moritz Y. Becker, Peter Sewell (Computer Laboratory, University of Cambridge)

Cassandra expresses policies in an extension of Datalog with constraints. It uses a top-down evaluation algorithm that is sound, complete, terminating, and efficient enough to deal with the 310-rule health application. It handles RBAC, trust negotiation, and remote entities.

The Consistency of Task-Based Authorization Constraints in Workflow Systems
Kaijun Tan (University of Pennsylvania), Jason Crampton (Royal Holloway, University of London), Carl Gunter (University of Pennsylvania)

In a workflow schema with RBAC authorizations, role permissions are qualified by where they are in the task flow graph. Authorization constraints (such as separation of duty) can conflict with task role requirements. An algorithm is given for checking consistency.

11:00 - 12:00 Declassification & Information Flow
Session Chair: Heiko Mantel

Enforcing Robust Declassification Andrew Myers (Cornell University), Andrei Sabelfeld (Chalmers University of Technology), Steve Zdancewic (University of Pennsylvania)

A security-type-checking approach on programs is used to allow "robust declassification," in which high-integrity code is allowed to explicitly declassify or downgrade expressions. (Integrity is part of the security level.) Robustness means that low-integrity code may not cause downgrading by, for example, affecting a branch.

Modelling Downgrading in Information Flow Security
Annalisa Bossi, Carla Piazza, Sabina Rossi (Universita' Ca' Foscari di Venezia, Italy)

This is a process algebra (SPA) approach for expressing forms of noninterference that allow downgrading. They mention a 1992 Rushby report and other intransitive noninterference notions for deterministic systems. Their extension is expressive enough to handle various nondeterministic possibilistic formulations. They support unwinding, compositionality, and refinement under given conditions.

2:00 - 3:00 Formal Methods & Cryptography
Session Chair: John Mitchell

Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library
Michael Backes, Birgit Pfitzmann (IBM Zurich Research Laboratory)

It is shown how to add symmetric encryption to the ideal cryptographic library proposed earlier by this group. The library allows cryptographically sound security proofs with a symbolic Dolev-Yao approach. Symmetric encryption was difficult for their simulatability approach because secret keys can be sent as data.

On Universally Composable Notions of Security for Signature, Certification and Authentication
Ran Canetti (IBM Research)

The basic security properties of a signature scheme are captured as a stand-alone module, in contrast with the the common library approach of, e.g., the IBM Zurich work. This formulation is chosen-message-attack- (CMA-) secure. The paper in the proceedings has an appendix reviewing the universally-composable (UC) security framework.

3:30 - 5:00 Panel: Formal Methods & Cryptography
Panel Chair: Cathy Meadows (Naval Research Laboratory)
Panelists: Ran Canetti, Michael Backes, and Andre Scedrov

The discussion included a reminder from Scedrov not to forget Shannon's basic information flow approach, as in the proof of one-time-pad security, in the context of computational models. Mitchell (in a question) challenged Canetti's use of interactive Turing machines as a model, suggesting that other models are more standard and better suited to model concurrent systems. Restrained, learned fireworks ensued.

9:00 - 10:00 Authorization
Session Chair: Geoff Smith

By Reason and Authority: A System for Authorization of Proof-Carrying Code Nathan Whitehead, Martin Abadi (University of California, Santa Cruz), George Necula (University of California, Berkeley)

This approach presupposes that Java or typed assembly language is downloaded along with a proof that it satisfies a security property. It is shown here how to verify authorization properties with a type check. Properties are expressed in BLF, a combination of Binder and LF, a modal logic based on Datalog with "says" and "believe" operators.

A Formal Foundation for XrML Licenses
Joseph Halpern, Vicky Weissman (Cornell University)

XrML, used for writing license policies, does not have a formal semantics, and there are startling problems in the way groups are handled. A semantics for a fragment of XrML is provided, along with a decision procedure for inferring access permission from licenses.

10:30 - 11:30 Protocols II
Session Chair: Michael Backes

Formal analysis of multi-party contract signing
Rohit Chadha (University of Sussex), Steve Kremer (Universite Libre de Bruxelles), Andre Scedrov (University of Pennsylvania)

Mocha was used to analyze two published protocols. In the Garay-Mackenzie protocol there is a fairness problem that shows up only with four or more signers. (This is the second example of a multi-party protocol problem that requires four participants; the other was for Cliques protocols.)

Symbolic Model Checking the Knowledge of the Dining Cryptographers Kaile Su (Zhongshan University, China), Ron van der Meyden (University of New South Wales, Sydney)

Chaum's Dining Cryptgraphers problem is a multiparty anonymity protocol (involving coin flips but no cryptography). Surprisingly, there is no general proof; this paper is about model checking knowledge formulas using BDDs, and gets up to around 1000 diners.

(Croquet winner: Millen; 2nd was Mantel)

Summary by Jon Millen. (Corrections, additions welcomed)