Abstract
In this paper, formal verification methodologies and the SPR (Safety Problem Resolver) model checking tool are used for verifying a security model's safety. The SPR tool makes it possible to analyze security issues on security systems based on the access control model. To illustrate this approach, a case study of the Simple Access Control Model (SACM) is used and specific safety problems of the security model are analyzed using the SPR tool.
Keywords
- SPR (Safety Problem Resolver)
- SEW (Security Evaluation Workshop)
- SPSL (Safety Problem Specification Language)
Cite this article
@article{cai-1421,
author = {Il-Gon Kim and Miyoung Kang and Jin-Young Choi and Peter D. Zegzhda and Maxim O. Kalinin and Dmitry P. Zegzhda and Inhye Kang},
title = {Formal Verification of Security Model Using SPR Tool},
journal = {Computing and Informatics},
volume = {25},
number = {5},
pages = {353--368},
year = {2006},
issn = {1335-9150},
url = {https://cai.type.sk/content/2006/5/formal-verification-of-security-model-using-spr-tool/}
}
TY - JOUR AU - Il-Gon Kim AU - Miyoung Kang AU - Jin-Young Choi AU - Peter D. Zegzhda AU - Maxim O. Kalinin AU - Dmitry P. Zegzhda AU - Inhye Kang TI - Formal Verification of Security Model Using SPR Tool JO - Computing and Informatics VL - 25 IS - 5 SP - 353 EP - 368 PY - 2006 SN - 1335-9150 UR - https://cai.type.sk/content/2006/5/formal-verification-of-security-model-using-spr-tool/ KW - SPR (Safety Problem Resolver) KW - SEW (Security Evaluation Workshop) KW - SPSL (Safety Problem Specification Language) ER -
Kim, I., Kang, M., Choi, J., Zegzhda, P. D., Kalinin, M. O., Zegzhda, D. P., & Kang, I. (2006). Formal Verification of Security Model Using SPR Tool. Computing and Informatics, 25(5), 353–368. https://cai.type.sk/content/2006/5/formal-verification-of-security-model-using-spr-tool/