Chinese Journal of Network and Information Security ›› 2016, Vol. 2 ›› Issue (3): 52-67.doi: 10.11959/j.issn.2909-109x.2016.00038

• academic paper • Previous Articles     Next Articles

Formal specification and security verification of usage control model based on PAT

Cong-hua ZHOU(),Wei-he CHEN,Zhi-feng LIU   

  1. School of Computer Science and Telecommunication Engineering, Jiangsu University, Zhenjiang 212013, China
  • Revised:2016-03-05 Online:2016-12-01 Published:2016-04-20
  • Supported by:
    The National Natural Science Foundation of China(61300228)


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.

Key words: UCON, formal specification, security analysis, model checking

CLC Number: 

No Suggested Reading articles found!