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

第 2 卷第 3 期 网络与信息安全学报 Vol.2 No.3 2016 年 3 月 Chinese Journal of Network and Information Security March 2016 基于 PAT 的使用控制模型的形式化规约与安全性分析 周从华，陈伟鹤，刘志锋 （江苏大学计算机科学与通信工程学院，江苏 镇江 212013 ） 摘 要：使用控制模型 UCON 是高度分布式、网络化的异构开放式计算环境下实现数字资源保护的新型 访问控制模型。首先，利用态式时间进程代数 TCSP#建立了每个 UCON 核模型的形式化规约，以及针 对一般化 UCON 的组合规约机制。其次，提出了各种基于单会话的进程组合机制，实现了复杂并发会话、 时间控制与非确定性的形式化规范，从而使组合进程的可达空间即为所求空间。最后，提出了基于可达 空间的 UCON 安全性分析方法，以及基于进程代数等价的控制规则冲突性分析方法。所有的工作都已在 PAT 上实现，表明所提方法是切实可行的，同时也为 UCON 的形式化规范与安全性验证寻找到了一个合 适的工具。 关键词：UCON ；形式化规约；安全性分析；模型检测 中图分类号：TP309.7 文献标识码：A doi: 10.11959/j.issn.2096-109x.2016.00038 Formal specification and security verification of usage control model based on PAT ZHOU Cong-hua, CHEN Wei-he, LIU Zhi-feng (School of Computer Science and Telecommunication Engineering, Jiangsu University, Zhenjiang 212013, China) Abstract: Usage control (UCON) is an access control model to enforce digital resources protection in highly dis tributed, 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 con current 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 conflic