Security policy in multi-domain environments

Walid Tfaili, Abdelghani Chibani, Yacine Amirat. Proceedings of the IEEE Information Reuse and Integration (IRI), Las Vegas (USA)

http://iri2009.cpsc.ucalgary.ca/

Secure interoperation between separately administrated domains, is becoming one of the major challenges in multidomain environments. In fact, many companies extend their business beyond traditional boundaries. To perform their tasks, employees must work from everywhere, and have access to applications belonging to other business units, suppliers, partners and affiliates. This is the case of most ubiquitous computing systems. As very little work has been done on

the composition of separately administrated heterogeneous access control policies, so very few information are available on the subject. We present in this paper a survey on composition methods of access control management as well as
mathematical proofs and complexity of composition methods. the complexity results prove that, even for a small number of domains and users in each domain the problem can be very complex. The composition problem can be formulated as an
optimization problem.

Laid Kahloul, Karim Djouani, Walid Tfaili. 4th International Workshop on Verification and Evaluation of Computer and Communication Systems The British Computer Society. Paris (France).

http://vecos.ensta.fr/2010/index.html

Role Based Access Control (RBAC) is one of the models used in designing and implementation of security policies in large networking systems. The classical model doesn’t consider temporal aspects which are so important in such policies. Temporal RBAC (TRBAC) is proposed to deal with this disadvantage. Although the elegance of these models, design a security policy remains a challenge. One is obliged to prove the consistency and the correctness of the policy. Using formal verification allows proving that the designed policy is consistent. In this paper1, we present a
formal modelling/analysis approach for TRBAC policies. We use Timed Colored Petri Nets to model the TRBAC policy, and then CPN-tool is used to analyze the generated models. The analysis allows proving many important properties about the TRBAC security policy.

Laid Kahloul, Karim Djouani, Walid Tfaili. The second international conference on Networked Digital Technologies in the “Communications in Computer and Information Science” (CCIS) Series of Springer LNCS. Prague, (Czech Republic)

Role Based Access Control (RBAC) is more and more applied to design and implement security policies in large networking systems. Although the elegance of this model, the design process of a security policy is a challenge. The consistence and the correctness of the policy are crucial. Formal verification is one of the techniques, which can be used to prove that the designed policy is consistent. In this paper, we present a concrete formal modeling/analysis approach for RBAC policies. The modeling phase uses Colored Petri Nets. The generated models will be analyzed using the CPN-tool.
This analysis will wallow to prove many important proprieties about the RBAC security policy.