Article

Formal verification of security specifications with common criteria

Authors:

Shoichi Morimoto,

Shinjiro Shigematsu,

Jingde ChengAuthors Info & Claims

SAC '07: Proceedings of the 2007 ACM symposium on Applied computing

Pages 1506 - 1512

https://doi.org/10.1145/1244002.1244325

Published: 11 March 2007 Publication History

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

[1]

Bertot, Y. and Casteran, P. Interactive Theorem Proving and Program Development. Springer-Verlag, 2004.

Digital Library

[2]

Clarke, E., Grumberg, O., and Peled, D. Model Checking. MIT Press, 2000.

Digital Library

[3]

Common Criteria Org. Evaluated Product Files. http://www.commoncriteriaportal.org/public/files/epfiles/

[4]

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.

Digital Library

[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]

Hinchey, M. G. and Bowen, J. P. High-Integrity System Specification and Design. 1st. Springer-Verlag, 1999.

Digital Library

[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.

Digital Library

[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]

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.

Digital Library

[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.

Digital Library

[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]

Potter, B., Till, D., and Sinclair, J. An Introduction to Formal Specification and Z. 2nd. Prentice Hall PTR, 1996.

Digital Library

Cited By

Mishra AMustafa K(2023)Security requirements specification by formal methods: a research metadata analysisMultimedia Tools and Applications10.1007/s11042-023-17218-483:14(41847-41866)Online publication date: 13-Oct-2023
https://doi.org/10.1007/s11042-023-17218-4
Sun NLi CChan HDung Le BIslam MZhang LIslam MArmstrong W(2022)Defining Security Requirements With the Common Criteria: Applications, Adoptions, and ChallengesIEEE Access10.1109/ACCESS.2022.316871610(44756-44777)Online publication date: 2022
https://doi.org/10.1109/ACCESS.2022.3168716
Mishra AMustafa K(2021)A review on security requirements specification by formal methodsConcurrency and Computation: Practice and Experience10.1002/cpe.670234:5Online publication date: 17-Nov-2021
https://doi.org/10.1002/cpe.6702
Show More Cited By

Index Terms

Formal verification of security specifications with common criteria
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

A security specification verification technique based on the international standard ISO/IEC 15408
SAC '06: Proceedings of the 2006 ACM symposium on Applied computing

This 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 Conference

Formal 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

Information & Contributors

Information

Published In

cover image ACM Conferences

SAC '07: Proceedings of the 2007 ACM symposium on Applied computing

March 2007

1688 pages

ISBN:1595934804

DOI:10.1145/1244002

Conference Chairs:
Yookun Cho
Seoul National University, Seoul, Korea
,
Roger L. Wainwright
University of Tulsa, Tulsa, Oklahoma
,
Hisham M. Haddad
Kennesaw State University, Kennesaw, Georgia
,
Sung Y. Shin
South Dakota State University, Brookings, South Dakota
,
Program Chair:
Yong Wan Koo
The University of Suwon, Gyeongggi-do, Korea

Copyright © 2007 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 March 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

SAC07

Sponsor:

SIGAPP

SAC07: The 2007 ACM Symposium on Applied Computing

March 11 - 15, 2007

Seoul, Korea

Acceptance Rates

Overall Acceptance Rate 1,650 of 6,669 submissions, 25%

Upcoming Conference

SAC '25

Sponsor:
sigapp

The 40th ACM/SIGAPP Symposium on Applied Computing

March 31 - April 4, 2025

Catania , Italy

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
838
Total Downloads

Downloads (Last 12 months)25
Downloads (Last 6 weeks)2

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Mishra AMustafa K(2023)Security requirements specification by formal methods: a research metadata analysisMultimedia Tools and Applications10.1007/s11042-023-17218-483:14(41847-41866)Online publication date: 13-Oct-2023
https://doi.org/10.1007/s11042-023-17218-4
Sun NLi CChan HDung Le BIslam MZhang LIslam MArmstrong W(2022)Defining Security Requirements With the Common Criteria: Applications, Adoptions, and ChallengesIEEE Access10.1109/ACCESS.2022.316871610(44756-44777)Online publication date: 2022
https://doi.org/10.1109/ACCESS.2022.3168716
Mishra AMustafa K(2021)A review on security requirements specification by formal methodsConcurrency and Computation: Practice and Experience10.1002/cpe.670234:5Online publication date: 17-Nov-2021
https://doi.org/10.1002/cpe.6702
Hu XZhuang YZhang F(2019)A Security Modeling and Verification Method of Embedded Software Based on Z and MARTEComputers & Security10.1016/j.cose.2019.101615(101615)Online publication date: Sep-2019
https://doi.org/10.1016/j.cose.2019.101615
Höller APreschern CSteger CKreiner CKrieg ABock HHaid J(2013)Automatized high-level evaluation of security properties for RTL hardware designsProceedings of the Workshop on Embedded Systems Security10.1145/2527317.2527323(1-8)Online publication date: 29-Sep-2013
https://dl.acm.org/doi/10.1145/2527317.2527323
Da Bao Junichi Miura Ning Zhang Goto YJingde Cheng (2013)Supporting verification and validation of security targets with ISO/IEC 15408Proceedings 2013 International Conference on Mechatronic Sciences, Electric Engineering and Computer (MEC)10.1109/MEC.2013.6885475(2621-2628)Online publication date: Dec-2013
https://doi.org/10.1109/MEC.2013.6885475
Qamar NFaber JLedru YLiu Z(2013)Automated Reviewing of Healthcare Security PoliciesFoundations of Health Information Engineering and Systems10.1007/978-3-642-39088-3_12(176-193)Online publication date: 2013
https://doi.org/10.1007/978-3-642-39088-3_12
Qamar NLedru YIdani A(2011)Validation of security-design models using ZProceedings of the 13th international conference on Formal methods and software engineering10.5555/2075089.2075113(259-274)Online publication date: 26-Oct-2011
https://dl.acm.org/doi/10.5555/2075089.2075113
Loinig JSteger CWeiss RHaselsteiner E(2011)IdeaProceedings of the Third international conference on Engineering secure software and systems10.5555/1946341.1946369(264-271)Online publication date: 9-Feb-2011
https://dl.acm.org/doi/10.5555/1946341.1946369
Qamar NLedru YIdani A(2011)Validation of Security-Design Models Using ZFormal Methods and Software Engineering10.1007/978-3-642-24559-6_19(259-274)Online publication date: 2011
https://doi.org/10.1007/978-3-642-24559-6_19
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten