A Marie Curie Action research project based at King's College London funded by the 6th European Community Framework Programme.

Summary

Term rewriting systems are usually defined by specifying a set of terms, and a set of rewrite rules that are used to ``reduce'' terms. This simple idea is very powerful: term rewriting techniques have had deep influence in the development of computational models, specification languages, theorem provers and proof assistants. More recently, rewriting systems have been used as a formal basis for the study of a broad range of security issues.
In this project we focus on the specification, implementation, and validation of security policies. The general goal of this project is to provide a deep analysis of access control models and policies using rewriting. We have developed access control policies for centralised or distributed systems using a term rewriting framework. For doing this, we have extended the usual notion of rewriting to accommodate distributed code and investigated a theory of access control described in terms of a set of rewrite rules and their reductions.
We have applied our framework to the problem of policy combinations via a set of algebraic operators and we have shown how to build a global policy which is consistent with its local specifications.
Moreover, we have taken advantage of the existing tools and rewrite techniques to study the properties of the rewrite system, such as termination and confluence which relates directly to properties of the access control policy such as consistency and totality.
This has then be used as a starting point for the design of a rewrite-based language with access control primitives.