Journal of Computer Security

Rôle-based access control (RBAC) is increasingly attracting attention because it reduces the complexity and cost of security administration by interposing the notion of rôle in the assignment of permissions to users. In this paper, we present a formal framework relying on an extension of the π-calculus to study the behaviour of concurrent systems in a RBAC scenario. We define a type system ensuring that the specified policy is respected during computations, and a behavioural equivalence to equate systems. We then consider a more sophisticated feature that can be easily integrated in our framework, i.e., the possibility of automatically adding rôle activations and deactivations to processes to be run under a given policy (whenever possible). Finally, we show how the framework can be easily extended to express significant extensions of the core RBAC model, such as rôles hierarchies or constraints determining the acceptability of the system components.

Noninterference requires that there is no information flow from sensitive to public data in a given system. However, many systems release sensitive information as part of their intended function and therefore violate noninterference. To control information flow while permitting information release, some systems have a downgrading or declassification mechanism, but this creates the danger that it may cause unintentional information release. This paper shows that a robustness property can be used to characterize programs in which declassification mechanisms cannot be controlled by attackers to release more information than intended. It describes a simple way to provably enforce this robustness property through a type-based compile-time program analysis. The paper also presents a generalization of robustness that supports upgrading (endorsing) data integrity.

The A-GDH.2 and SA-GDH.2 authenticated group key agreement protocols showed to be flawed in 2001. Even though the corresponding attacks (or some variants of them) have been rediscovered in several different frameworks, no fixed version of these protocols has been proposed until now.

In this paper, we prove that it is in fact impossible to design a scalable authenticated group key agreement protocol based on the same design assumptions as the A-GDH ones. We proceed by providing a systematic way to derive an attack against any A-GDH-type protocol with at least four participants and exhibit protocols with two and three participants which we cannot break using our technique. As far as we know, this is the first generic insecurity result reported in the literature concerning authentication protocols.