Formal verification of security specifications with common criteria

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Formal verification of security specifications with common criteria

Full text

Pdf (248 KB)

Source

Symposium on Applied Computing archive
Proceedings of the 2007 ACM symposium on Applied computing table of contents

Seoul, Korea

SESSION: Software verification table of contents

Pages: 1506 - 1512

Year of Publication: 2007

ISBN:1-59593-480-4

Authors

Shoichi Morimoto	School of Industrial Technoloy, Higashi-oi, Shinagawa-ku, Tokyo, Japan
Shinjiro Shigematsu	Saitama University, Sakura-ku, Saitama, Japan
Yuichi Goto	Saitama University, Sakura-ku, Saitama, Japan
Jingde Cheng	Saitama University, Sakura-ku, Saitama, Japan

Sponsor

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 20, Downloads (12 Months): 126, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1244002.1244325 What is a DOI?

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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
	2	Clarke, E., Grumberg, O., and Peled, D. Model Checking. MIT Press, 2000.
	3	Common Criteria Org. Evaluated Product Files. http://www.commoncriteriaportal.org/public/files/epfiles/
	4	Sophie Dupuy , Yves Ledru , Monique Chabre-Peccoud, An Overview of RoZ: A Tool for Integrating UML and Z Specifications, Proceedings of the 12th International Conference on Advanced Information Systems Engineering, p.417-430, June 05-09, 2000
	5	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.
	6	Michael G. Hinchey , J. P. Bowen , S. A. Schuman, High-Integrity System Specification and Design, Springer-Verlag New York, Inc., Secaucus, NJ, 1999
	7	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.
	8	ISO/IEC 13568 Standard. Information Technology - Z Formal Specification Notation - Syntax, Type System and Semantics. 2002.
	9	ISO/IEC 15408 Standard. Information Technology - Security Techniques - Evaluation Criteria for IT Security. 1999.
	10	Jacob, J. Basic Theorems About Security. J. Comput. Secur. 1, 3--4, pages. 385--411, 1992.
	11	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.
	12	Morimoto, S. and Cheng, J. Modeling Protection Profiles by UML and their Formal Verification. Systems and Computers in Japan. Wiley, 2007.
	13	Shoichi Morimoto , Jingde Cheng, Patterning Protection Profiles by UML for Security Specifications, Proceedings 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), p.946-951, November 28-30, 2005
	14	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.
	15	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.
	16	ORA Canada, Z/EVES. http://www.ora.on.ca/z-eves/welcome.html
	17	Ben Potter , David Till , Jane Sinclair, An Introduction to Formal Specification and Z, Prentice Hall PTR, Upper Saddle River, NJ, 1996