基于PAT的使用控制模型的形式化规约与安全性分析  

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

作　　者：周从华[1] 陈伟鹤[1] 刘志锋[1] ZHOU Cong-hua CHEN Wei-he LIU Zhi-feng(School of Computer Science and Telecommunication Engineering, Jiangsu University, Zhenjiang 212013, China)

机构地区：[1]江苏大学计算机科学与通信工程学院,江苏镇江212013

出　　处：《网络与信息安全学报》2016年第3期52-67,共16页Chinese Journal of Network and Information Security

基　　金：国家自然科学基金资助项目(No.61300228)~~

摘　　要：使用控制模型UCON是高度分布式、网络化的异构开放式计算环境下实现数字资源保护的新型访问控制模型。首先,利用态式时间进程代数TCSP#建立了每个UCON核模型的形式化规约,以及针对一般化UCON的组合规约机制。其次,提出了各种基于单会话的进程组合机制,实现了复杂并发会话、时间控制与非确定性的形式化规范,从而使组合进程的可达空间即为所求空间。最后,提出了基于可达空间的UCON安全性分析方法,以及基于进程代数等价的控制规则冲突性分析方法。所有的工作都已在PAT上实现,表明所提方法是切实可行的,同时也为UCON的形式化规范与安全性验证寻找到了一个合适的工具。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.

关 键 词：UCON 形式化规约 安全性分析 模型检测 

分 类 号：TP309.7[自动化与计算机技术—计算机系统结构]