Formal Verification of Security Model Using SPR Tool - Kim, Il Gon; Kang, Miyoung; Choi, Jin Young; Zegzhda, Peter D.; Kalinin, Maxim O.; Zegzhda, Dmitry P.; Kang, Inhye (Computing and Informatics, 2012)
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.