This paper proposes a new hybrid method to formally verify whether the security specification of a target information system satisfies security functional requirements defined in ISO/IEC 15408 evaluation criteria for security. We classify at first the security functional requirements of ISO/IEC 15408 into two classes: static requirements concerning static properties and dynamic requirements concerning dynamic behavior of target systems, and then formalize the static requirements with Z notation and the dynamic requirements with temporal logic. Thus, we can verify static properties using theorem-proving and dynamic behavior using model-checking. As a result, developers can easily use the method to verify whether the security specification of a target information system satisfies both static and dynamic security functional requirements defined in ISO/IEC 15408. The new method is an evolution and improvement of our early verification method where only Z notation was adapted and to verify dynamic behavior of target systems is difficult. © Springer-Verlag Berlin Heidelberg 2008.
CITATION STYLE
Morimoto, S., Shigematsu, S., Goto, Y., & Cheng, J. (2008). Classification, formalization and verification of security functional requirements. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4910 LNCS, pp. 622–633). Springer Verlag. https://doi.org/10.1007/978-3-540-77566-9_54
Mendeley helps you to discover research relevant for your work.