关键词: 安全性规格, CC, Z, 时序逻辑, 形式化, 验证方法

Abstract: As information systems become more and more important and indispensable in social lives, the demands of people for the security of information systems are also increasing. For those important information systems that don't allow flaws, its security specification must be described and verified by formal methods. This paper introduces the security specification description and verification method we proposed first in the world based on the international commom standards CC (ISO-NIEC15408). Z notation and temporal logic are used to formalize the information security evaluation standard—the functional elements defined in the international standard CC. On the other hand, UML is used to model the protection profile formally, and after describing the security specification of the target information system by Z notation and temporal logic, theorem proving method and model checking method are used to verify the security specification of the target information system. In order to make the specification and verification easier for people that have poor professional knowledge, a support tool named FORVEST has been developed.

Key words: security specification, CC, Z notation, temporal logic, formalization, verification methods