Formal Verification of Security Model Using SPR Tool

keywords: SPR (Safety Problem Resolver), SEW (Security Evaluation Workshop), SPSL (Safety Problem Specification Language)
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.
reference: Vol. 25, 2006, No. 5, pp. 353–368