FORVEST: A Support Tool for Formal Verification of Security Specifications with ISO/IEC 15408

It is very important to formally verify security specifications of information systems for ensuring their security. Thus we have proposed a formal verification method of security specifications with ISO/IEC 15408. However, to use the method, verifiers have to be familiar with Z notation, linear temporal logic, NuSMV input language, theorem proving, model checking, and ISO/IEC 15408. Moreover, the verifiers also have to prepare some tools supporting the formal verification. Therefore, the verifiers cannot utilize the method easily. To easily verify security specifications based on the method, this paper presents a support tool for the method, named "FORVEST". FORVEST supports the verifiers by guiding the verifiers appropriately and providing information of Z notation, linear temporal logic, theorem proving, model checking, and ISO/IEC 15408 when they are needed. FORVEST also provides an environment where verifiers can access and use tools of model checking and theorem proving through a Web browser. By using FORVEST, verifiers can easily perform the formal verification.