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.

Keywords:

Availability, authentication, authorization, confidentiality, formal methods, integrity, non-repudiation,

References

Competing interests

The authors have no competing interests.

Open Access Policy

This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.

Copyright

The authors have no competing interests.