1. Formal specification and security verification of usage control model based on PAT
- Author
-
Cong-hua ZHOU, Wei-he CHEN, and Zhi-feng LIU
- Subjects
UCON ,formal specification ,security analysis ,model checking ,Electronic computers. Computer science ,QA75.5-76.95 - Abstract
Usage control (UCON) is an access control model to enforce digital resources protection in highly distributed, heterogeneous network computing environment. Firstly, each core model of UCON was specified formally with TCSP#, and a combination specification mechanism was proposed for general UCON. Secondly, as the basis of the security analysis, the concepts and calculation method of the reachable space were given. Various combination mechanisms of processes based on single-session was presented to achieve formal specifications of complex concurrent sessions, timings and nondeterminism. Then the reachable space of combined processes was the desired space. Finally, the security analysis method based on the reachable space and the conflict analysis of access control policies based on the equivalent checking in process algebras were proposed for UCON model. All the proposed work had been formal checked in PAT. The experiment result shows that the proposed approaches are feasible, and PAT is a really great tool for the systematic formal specification and security analysis of UCON.
- Published
- 2016
- Full Text
- View/download PDF