DocumentCode :
2478429
Title :
Model Checking Based Security Policy Verification and Validation
Author :
Ma, Jianli ; Zhang, Dongfang ; Xu, Guoai ; Yang, Yixian
Author_Institution :
State Key Lab. of Networking & Switching Technol., Beijing Univ. of Posts & Telecommun., Beijing, China
fYear :
2010
fDate :
22-23 May 2010
Firstpage :
1
Lastpage :
4
Abstract :
Lots of security mechanisms have been applied in current information systems to assure the confidentiality and integrality for the information processed. These mechanisms are selected in accordance with the certain security policies which should satisfy the system requirements. It is necessary to validate the security whether it really and truly protect the system. In this paper, we first define and formalize the validity and reliability for validation and verification criteria for the security validating. Then, we propose a model checking based method to validate the consistency and completeness for security policies. In our method, the system´s behaviors are modeled as the transfer structure and the property is described using LTL formula, and the model checker SPIN is applied to verify and validate the security policy. The model checking based validation also can be used to generate the validate sequences. In the end, we approve the method proposed is valid and reliable for information system security validation.
Keywords :
formal verification; information systems; security of data; LTL formula; SPIN; confidentiality; information system security validation; integrality; model checking; reliability; security policy verification; Calculus; Hardware; Information security; Information systems; Laboratories; Logic; Privacy; Protection; Protocols; Telecommunication switching;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Intelligent Systems and Applications (ISA), 2010 2nd International Workshop on
Conference_Location :
Wuhan
Print_ISBN :
978-1-4244-5872-1
Electronic_ISBN :
978-1-4244-5874-5
Type :
conf
DOI :
10.1109/IWISA.2010.5473291
Filename :
5473291
Link To Document :
بازگشت