Please use this identifier to cite or link to this item: http://archives.univ-biskra.dz/handle/123456789/24018
Full metadata record
DC FieldValueLanguage
dc.contributor.authorBenattia, Hasiba-
dc.date.accessioned2023-04-09T07:25:07Z-
dc.date.available2023-04-09T07:25:07Z-
dc.date.issued2019-06-01-
dc.identifier.urihttp://archives.univ-biskra.dz/handle/123456789/24018-
dc.description.abstractThis thesis tackles the problem of formal modelling and verification of security policies in cloud computing. Indeed, our research focuses on the modelling and the verification of access control policies using Coloured Petri Nets (CPNs). Due to its ability to reduce complexity, Role Based Access Control (RBAC) model was one of the predominant models for access control and the specification of security policies. In its original version, RBAC does not consider several important events, thus, TRBAC (Temporal RBAC) was proposed as an RBAC extension. This thesis provides three basic contributions. In the first contribution, HTCPNs (Hierarchical Timed Colored Petri Nets) formalism is used to model the TRBAC (Temporal Role Based Access Control) policy, and then the CPN-tool is exploited to analyse the obtained models. Indeed, the timed aspect in HTCPN allows us to deal with temporal constraints in TRBAC. The hierarchical aspect of HTCPN makes the TRBAC model “manageable”, despite the complexity of the policy. RBAC as well as TRBAC suffer from several drawbacks in large scale networks as the case of cloud environment. Although Attribute Based Access Control (ABAC) model handles some RBAC drawbacks, ABAC misses RBAC advantages. Hence, as a second contribution, we propose an access control model FRABAC (Fine-Grained Role Attribute Based Access Control) that provides scalability, flexibility, and fine granularity in the cloud environment. FRABAC combines and extends, basically, two models RBAC and ABAC. In order to demonstrate the advantages of the new proposed model, an empirical study is realised. In this study, the new proposed model is compared versus three existing models, using specific metrics. The results demonstrate that the new proposed model is more suitable than existing ones. As a third contribution, we provide a formal specification/ verification of FRABAC using HTCPN formalism and CPN-tool.en_US
dc.language.isoenen_US
dc.subjectAccess Control, Security Policy, RBAC, ABCA, FRABAC, Formal Modelling, Formal Analysing, Petri nets, Cloud Computingen_US
dc.titleFormal Modelling and Verification of Security Policies in Cloud Computingen_US
dc.typeThesisen_US
Appears in Collections:Informatique

Files in This Item:
File Description SizeFormat 
Formal Modelling and Verification of Security Policies in Cloud Computing.pdf2,08 MBAdobe PDFView/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.