Shoichi Morimoto
ABSTRACT
This paper proposes a formalization and verification technique for security specifications, based on common criteria. Generally, it is difficult to define reliable security properties that should be applied to validate an information system. Therefore, we have applied security functional requirements that are defined in the ISO/IEC 15408 common criteria to the formal verification of security specifications. We formalized the security criteria of ISO/IEC 15408 and developed a process, using Z notation, for verifying security specifications. We also demonstrate some examples of the verification instances using the theorem prover Z/EVES. In the verification process, one can verify strictly whether specifications satisfy the security criteria defined in ISO/IEC 15408.
- Bertot, Y. and Casteran, P. Interactive Theorem Proving and Program Development. Springer-Verlag, 2004. Google Scholar
Digital Library
- Clarke, E., Grumberg, O., and Peled, D. Model Checking. MIT Press, 2000.Google ScholarDigital Library
- Common Criteria Org. Evaluated Product Files. http://www.commoncriteriaportal.org/public/files/epfiles/Google Scholar
- Dupuy, S., Ledru, Y., and Chabre-Peccoud, M. An Overview of RoZ: A Tool for Integrating UML and Z Specifications. In Proc. of the 12th international Conference on Advanced information Systems Engineering. B. Wangler and L. Bergman, Eds. Lecture Notes in Computer Science, vol. 1789, pages. 417--430, Springer-Verlag, 2000. Google ScholarDigital Library
- Hall, A. Z Styles for Security Properties and Modern User Interfaces. In Proc. of the Formal Aspects of the First International Conference. A. E. Abdallah, P. Ryan, and S. Schneider, Eds. Lecture Notes in Computer Science, vol. 2629, pages. 152--166, Springer-Verlag, 2002.Google Scholar
- Hinchey, M. G. and Bowen, J. P. High-Integrity System Specification and Design. 1st. Springer-Verlag, 1999. Google ScholarDigital Library
- Horie, D., Morimoto, S., and Cheng, J. A Web User Interface of the Security Requirement Management Database Based on ISO/IEC 15408, In Proc. of Computational Science - ICCS 2006: 6th International Conference. V. N. Alexandrov et al., Eds. Lecture Notes in Computer Science, vol. 3994, pages. 797--804, Springer-Verlag, 2006. Google ScholarDigital Library
- ISO/IEC 13568 Standard. Information Technology - Z Formal Specification Notation - Syntax, Type System and Semantics. 2002.Google Scholar
- ISO/IEC 15408 Standard. Information Technology - Security Techniques - Evaluation Criteria for IT Security. 1999.Google Scholar
- Jacob, J. Basic Theorems About Security. J. Comput. Secur. 1, 3--4, pages. 385--411, 1992.Google Scholar
- Long, B. W., Fidge, C. J., and Cerone, A. A Z Based Approach to Verifying Security Protocols. In Proc. of the 5th International Conference on Formal Engineering Methods. J. S. Dong and J. Wood-. cock, Eds. Lecture Notes in Computer Science, vol. 2885, pages. 375--395, Springer-Verlag, 2003.Google ScholarCross Ref
- Morimoto, S. and Cheng, J. Modeling Protection Profiles by UML and their Formal Verification. Systems and Computers in Japan. Wiley, 2007.Google Scholar
- Morimoto, S. and Cheng, J. Patterning Protection Profiles by UML for Security Specifications. In Proc. of the international Conference on Computational intelligence For Modelling, Control and Automation and international Conference on intelligent Agents, Web Technologies and internet Commerce Vol-2 (Cimca-Iawtic'06) - Volume 02. pages. 946--951, IEEE Computer Society, 2005. Google ScholarDigital Library
- Morimoto, S., Horie, D., and Cheng, J. A Security Requirement Management Database Based on ISO/IEC 15408. In Proc. of Computational Science and Its Applications - ICCSA 2006, International Conference. M. Gavrilova et. al., Eds. Lecture Notes in Computer Science, vol. 3982, pages. 1--10, Springer-Verlag, 2006. Google ScholarDigital Library
- Oheimb, D. Interacting State Machines - a stateful approach to proving security -. In Proc. of the Formal Aspects of the First International Conference. A. E. Abdallah, P. Ryan, and S. Schneider, Eds. Lecture Notes in Computer Science, vol. 2629, pages. 15--32, Springer-Verlag, 2002.Google Scholar
- ORA Canada, Z/EVES. http://www.ora.on.ca/z-eves/welcome.htmlGoogle Scholar
- Potter, B., Till, D., and Sinclair, J. An Introduction to Formal Specification and Z. 2nd. Prentice Hall PTR, 1996. Google ScholarDigital Library
Index Terms
- Formal verification of security specifications with common criteria
Recommendations
A security specification verification technique based on the international standard ISO/IEC 15408
SAC '06: Proceedings of the 2006 ACM symposium on Applied computingThis paper proposes a security specification verification technique based on the international standard ISO/IEC 15408. We formalized the security criteria of ISO/IEC 15408 and developed the verification technique of security specifications based on the ...
Verifying security properties of internet protocol stacks: The split verification approach
We propose a novel method to construct user-space internet protocol stacks whose security properties can be formally explored and verified. The proposed method allows construction of protocol stacks using a C++ subset. We define a formal state-...
Visualization of Formal Specifications
APSEC '99: Proceedings of the Sixth Asia Pacific Software Engineering ConferenceFormal specification techniques provide precise and analyzable software specifications. However, formal notations provided by most formal specification techniques are not easy to use and understand for most people. Our approach counters this difficulty ...
Comments