Social networks supply a means by which people can communicate with each other while allowing for ease in initiating interaction and expressions. These systems of human collaboration may also be used to store and distribute information of a sensitive nature that must be secured against intrusions at all times. Given the massive operation embodied by social networks, multiple methods have been developed that control the flow of information so that those with authorization can gain access. Before allowing a social network to begin distributing its contents, a prudent prerequisite should be that the security protocols prevent unauthorized access.
Formal modeling and analysis of security properties, particularly those of Role-Based Access Control (RBAC), in social networks is the main focus of this thesis. A social network system and its security assurance mechanisms are modeled using the input language of Symbolic Model Verifier (SMV), and the properties of the system are specified using computation tree temporal logic (CTL*). Those properties are then verified using the SMV model checker. A real case was studied to demonstrate the effectiveness of model checking security properties in a social network system. The case consists of an account in which a group of users share various resources and access privileges which are controlled by RBAC. The case study results show that model checking is capable of formally analyzing security policies particularly RBAC in a social network system. In addition, the counter examples generated from model checking could help to create test cases for testing system implementation, and they can help us to find defects in the model as well. Formally modeling and model checking security policies in a complex system, like a social network, can greatly improve the security of these systems.
|Commitee:||Abrahamson, Karl, Ding, Junhua, Ding, Qin, Tabrizi, Nasseh|
|School:||East Carolina University|
|School Location:||United States -- North Carolina|
|Source:||MAI 51/02M(E), Masters Abstracts International|
|Keywords:||Model checking, Social networks|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be