This thesis reports an investigation into authorisation models, as used in identity and access management. It proposes new versions of an authorisation model, the Tees Confidentiality Model (TCM), and presents formal specifications in B, and verifications and implementations of the key concepts using Spec Explorer, Spec# and LinQ. After introducing the concepts of authorisation and formal models, a formal methods specification in B of Role Based Access Control (RBAC) is presented. The concepts in RBAC have heavily influenced authorisation over the last two decades, and most of the research has been with their continued development. A complete re-working of the ANSI RBAC Standard is developed in B, which highlights errors and deficiencies in the ANSI Standard and confirms that B is a suitable method for the specification of access control. A formal specification of the TCM in B is then developed. The TCM supports authorisation by multiple concepts, with no extra emphasis given to Role (as in RBAC). The conceptual framework of Reference Model and Functional Specification used in the ANSI RBAC Standard is used to structure the TCM formal model. Several improvements to the original TCM are present in the formal specification, notably a simplified treatment of collections. This new variation is called TCM2, to distinguish it from the original model. Following this, a further B formal specification of a TCM reduced to its essential fundamental components (referred to as TCM3) was produced. Spec Explorer was used to animate this specification, and as a step towards implementation An implementation of TCM3 using LinQ and SQL is then presented, and the original motivating healthcare scenario is used as an illustration. Finally, classes to implement the versions of the TCM models developed in the thesis are designed and implemented. These classes enable the TCM to be implemented in any authorisation scenario. Throughout the thesis, model explorations, animations, and implementations are illustrated by SQL, C# and Spec# code fragments. These illustrate the correspondence of the B specification to the model design and implementation, and the effectiveness of using formal specification to provide robust code.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:517470 |
| Date | January 2008 |
| Creators | Howitt, Anthony |
| Contributors | Longstaff, Jim : Dunne, Steve E. |
| Publisher | Teesside University |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://hdl.handle.net/10149/112674 |
Page generated in 0.0058 seconds