loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2009 International Conference on Availability, Reliability and Security
FORVEST: A Support Tool for Formal Verification of Security Specifications with ISO/IEC 15408
Fukuoka Institute of Technology, Fukuoka, Japan
March 16-March 19
ISBN: 978-0-7695-3564-7
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.
Index Terms:
formal verification, ISO/IEC 15408, security specifications, support tools
Citation:
Kenichi Yajima, Shoichi Morimoto, Daisuke Horie, Noor Sheila Azreen, Yuichi Goto, Jingde Cheng, "FORVEST: A Support Tool for Formal Verification of Security Specifications with ISO/IEC 15408," ares, pp.624-629, 2009 International Conference on Availability, Reliability and Security, 2009
Usage of this product signifies your acceptance of the Terms of Use.