Abstract
|
Article Information:
Formal Specification of Security Properties using Z Notation
Shafiq Hussain, Peter Dunne and Ghulam Rasool
Corresponding Author: Shafiq Hussain
Submitted: September 22, 2012
Accepted: November 23, 2012
Published: May 10, 2013 |
Abstract:
|
Software security is a challenging issue for distributed and open systems. Despite the importance of external protections of software systems, internal security has significant impact on the overall security of the software systems. In this study, internal security issues of software systems are addressed. Internal security of software systems is defined in terms of security properties: authentication, authorization, confidentiality, integrity, non-repudiation and resource availability. Internal security of software systems largely depends on the integration of these security properties into the software systems. A precise and unambiguous representation of these security properties is crucial for any successful secure system. Majority of the existing models are based on informal or semi-formal approaches to model these security properties. But no model is based on formal methods. Therefore, in this study, a formal specification of these security properties is presented in Z notation because formal methods are the only way to specify system properties unambiguously, completely and precisely. The resulting models are then analyzed by using Z/EVES theorem prover. The formal specifications of these security properties are analyzed only for syntax checking, type checking and automatic proofs of models.
Key words: Availability, authentication, authorization, confidentiality, formal methods, integrity, non-repudiation
|
Abstract
|
PDF
|
HTML |
|
Cite this Reference:
Shafiq Hussain, Peter Dunne and Ghulam Rasool, . Formal Specification of Security Properties using Z Notation. Research Journal of Applied Sciences, Engineering and Technology, (19): 4664-4670.
|
|
|
|
|
ISSN (Online): 2040-7467
ISSN (Print): 2040-7459 |
|
Information |
|
|
|
Sales & Services |
|
|
|