Name
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1145/1244002.1244325 | SAC |
Keywords | Field | DocType |
security criterion,verifying security specification,reliable security property,common criterion,security functional requirement,security specification,verification process,verification instance,verification technique,formal verification,theorem prover,functional requirement,theorem proving,satisfiability,information system,z notation | Information system,Z notation,Functional requirement,Programming language,Verification and validation,Computer science,Automated theorem proving,Algorithm,Runtime verification,Common Criteria,Formal verification | Conference |
ISBN | Citations | PageRank |
1-59593-480-4 | 8 | 0.71 |
References | Authors | |
9 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Shoichi Morimoto | 1 | 71 | 9.00 |
| Shinjiro Shigematsu | 2 | 12 | 1.85 |
| Yuichi Goto | 3 | 126 | 22.31 |
| Jingde Cheng | 4 | 542 | 85.38 |