FLoC 2006 - FCS-ARSPA

FCS-ARSPA'06

Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis
Seattle, August 15 - 16, 2006

FCS-ARSPA on Wednesday, August 16th

Session 4: Invited Talk (09:00‑10:00)
Chair: the PC chairs

09:00‑10:00 Martin Abadi (University of California at Santa Cruz and Microsoft Research)
Access Control in a Core Calculus of Dependency [ppt]
Access control is central to security in computer systems. Over the years, there have been many efforts to explain and to improve access control, sometimes with logical ideas and tools. In this talk, we explore a new approach based on type systems. For this purpose, we revisit the Dependency Core Calculus (DCC) from a logical perspective. DCC is an extension of the computational lambda calculus that was designed in order to capture the notion of dependency that arises in information-flow control, partial evaluation, and other programming-language settings. We show that, unexpectedly, DCC can be attractive also as a calculus for access control in distributed systems.

Session 5: Access Control and Policies 1 (10:00‑10:30)
Chair: the PC chairs

10:00‑10:30 Mathieu Jaume (University Paris 6)
Charles Morisset (University Paris 6)
Towards a formal specification of access control
Access control software must be based on a security policy model as software flaws often come from a lack of precision or some incoherences in the policy model. In this paper, we introduce an abstract framework allowing to define access control policies, in a very concise way, offering to refine specifications through several levels and ending by different possible implementations. Such a framework allows to formally reason about security policies and also to compare them, a point which is rarely approached. As an illustration, we give a formal description of the Bell and LaPadula and the Chinese Wall policies and we briefly sketch how to compare these two policies.

Break (10:30‑11:00)

Session 6: Access Control and Policies 2 (11:00‑12:30)
Chair: the PC chairs

11:00‑11:30   Amit Walvekar (University of Tulsa)
Manasi Kelkar (University of tulsa)
Melanie Smith (University of Tulsa)
Rose Gamble (University of tulsa)
Determining Conflicts in Interdomain Mappings for Access Control
Component-based software engineering provides time-efficient development solutions for fast-growing industry by allowing software reuse. When multiple software systems are combined into a single application, their access control policies must flawlessly integrate to allow users of one software system to interact with the other connected software systems. Within the application environment, these mappings among software systems are called interdomain mappings. Interdomain mappings between access control policies can introduce security vulnerabilities. A modified Petri Net, called a Conflict Petri Net, can be used to quickly analyze the interdomain access control mappings and evaluate the potential for security violations. These violations manifest themselves as conflicts within places of the Conflict Petri Net. The Conflict Petri Net is founded on Colored Petri Nets where different colored tokens have distinct access values. In this paper, we detect conflict in interdomain access control mappings for role-based access reflected in separation of duty, temporal, and cardinality policies.

11:30‑12:00   A. Prasad Sistla (University of Illinois at Chicago)
Min Zhou (University of Illinois at Chicago)
Analysis of Dynamic Policies
The paper considers the problem of modeling and analyzing dynamic policies in Trust Management Systems. It presents a general frame work and a specification language FCTL for specifying properties in such systems. Various important security properties such as simple safety, liveness, role containment can all be elegantly specified in this logic. The paper presents various upper and lower bounds for checking classes of formulas specifying various securities properties in this logic for dynamic systems specified in the RT0 Role based Trust management system.

12:00‑12:30   Chamseddine Talhi (Reseach Assistant)
Nadia Tawbi (Full Professor)
Mourad Debbabi (Full Professor)
Execution Monitoring Enforcement Under Memory-Limitation Constraints
Recently, attention has been given to formally characterize security policies that are enforceable by different kinds of security mechanisms. A very important research problem is the characterization of security policies that are enforceable by execution monitors constrained by memory limitations. This paper contributes to give more precise answers to this research problem. To represent execution monitors constrained by memory limitations, we introduce a new class of automata, Bounded History Automata. Characterizing memory limitations leads us to define a precise taxonomy of security policies enforceable under memory limitation constraints.

Lunch break (12:30‑14:00)

Session 7: Protocols 3 (14:00‑15:30)
Chair: Vitaly Shmatikov

14:00‑14:30   Veronique Cortier (Loria UMR 7503 & CNRS & INRIA Lorraine projet Cassis)
Graham Steel (School of Informatics, University of Edinburgh)
On the Decidability of a Class of XOR-based Key-management APIs
We define a new class of security protocols using XOR, and show that secrecy after an unbounded number of sessions is decidable for this class. The new class is important as it contains examples of key- management APIs, such as the IBM 4758 CCA API, which lie outside the classes for which secrecy has previously been shown to be decidable. Earlier versions of the CCA API were shown to have serious flaws, and the fixes introduced by IBM in version 2.41 have not been formally verified in a model with unbounded sessions. In showing the decidability of this class, we also suggest a simple decision procedure, which we plan to implement in future work to finally verify the revised API.

14:30‑15:00   Massimo Benerecetti (Dipartimento di Scienze Fisiche, Universit� di Napoli "Federico II")
Nicola Cuomo (Dipartimento di Scienze Fisiche, Universit� di Napoli "Federico II")
Adriano Peron (Dipartimento di Scienze Fisiche, Universit� di Napoli "Federico II")
Timed HLPSL for specification and verification of time sensitive protocols
In this paper we face the problem of specifying and verifying security protocols where temporal aspects explicitly appear in the description. For these kinds of protocols we propose an extension of the specification language HLPSL, originally proposed in the context of the Avispa Project and where quantitative temporal aspects were not considered. The semantics of such an extension, called Timed HLPSL, is given in terms of eXtended Timed Automata (XTA). The verification of timed protocols can then exploit standard model checking techniques. In particular, we have developed a protocol verification tool which employs the model checker UPPAAL as the verification engine. To illustrate how our framework applies, we also provide a specification of the Wide Mouthed Frog authentication protocol and show how its temporal features can be specified.

15:00‑15:30   Alan Jeffrey (Bell Labs, Lucent Technologies)
Ruy Ley-Wild (Carnegie Mellon University)
Dynamic Model Checking of C Cryptographic Protocol Implementations
We describe the Dolev�Yao C (DYC) cryptographic protocol message API. In addition to generating executable protocol implementations, DYC can be used to generate constraints on an attacker against the protocol. The resulting constraints can be handed to a constraint solver, which (if successful) will find an executable attack against the protocol. To our knowledge, this is the first attempt to automate the discovery of flaws with executable cryptographic protocol implementations, rather than high-level protocol specifications or simulations.