Formal Verification of Security Specifications with Common Criteria

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 pro cess, 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.