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

周从华; 陈伟鹤; 刘志锋

doi:10.11959/j.issn.2909-109x.2016.00038

您当前的位置：

首页 >

文章列表页 >

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

学术论文 | 更新时间：2024-06-03

- 基于PAT的使用控制模型的形式化规约与安全性分析
- Formal specification and security verification of usage control model based on PAT
- 网络与信息安全学报 2016年2卷第3期页码：52-67
- 作者机构：
- 作者简介：
  
  [ "周从华（1978-），男，江苏盐城人，博士，江苏大学副教授，主要研究方向为访问控制、形式化方法。" ]
  [ "陈伟鹤（1974-），男，江苏丹阳人，博士，江苏大学副教授，主要研究方向为访问控制、数据挖掘。" ]
  [ "刘志锋（1981-），男，江苏无锡人，博士，江苏大学副教授，主要研究方向为访问控制、形式化方法。" ]
- 基金信息：
  
  国家自然科学基金资助项目;The National Natural Science Foundation of China(61300228)
- DOI：10.11959/j.issn.2909-109x.2016.00038
  中图分类号： TP309.7
- 网络首发：2016-12，
  
  纸质出版：2016-03-15
- 稿件说明：
移动端阅览
周从华, 陈伟鹤, 刘志锋. 基于PAT的使用控制模型的形式化规约与安全性分析[J]. 网络与信息安全学报, 2016,2(3):52-67.

Cong-hua ZHOU, Wei-he CHEN, Zhi-feng LIU. Formal specification and security verification of usage control model based on PAT[J]. Chinese Journal of Network and Information Security, 2016, 2(3): 52-67.
周从华, 陈伟鹤, 刘志锋. 基于PAT的使用控制模型的形式化规约与安全性分析[J]. 网络与信息安全学报, 2016,2(3):52-67. DOI： 10.11959/j.issn.2909-109x.2016.00038.

Cong-hua ZHOU, Wei-he CHEN, Zhi-feng LIU. Formal specification and security verification of usage control model based on PAT[J]. Chinese Journal of Network and Information Security, 2016, 2(3): 52-67. DOI： 10.11959/j.issn.2909-109x.2016.00038.

摘要

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

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.

关键词

Keywords

references

PFLEEGER C P , PFLEEGER S L . Security in computing [M ] . Prentice Hall Professional Technical Reference , 2002 .

SANDHU R S , COYNE E J . FEINSTEIN H L , et al . Role-based access control models [J ] . Computer , 1996 , 29 ( 2 ): 38 - 47 .

FERRAIOLO D F , SANDHU R . GAVRILA S , et al . Proposed NIST standard for role-based access control [J ] . ACM Transactions on Information and System Security(TISSEC) , 2001 , 4 ( 3 ): 224 - 274 .

PARK J , SANDHU R . The UCON ABC usage control model [J ] . ACM Transactions on Information and System Security(TISSEC) , 2004 , 7 ( 1 ): 128 - 174 .

ZHANG X , PARISI-PRESICCE F , SANDHU R , et al . Formal model and policy specification of usage control [J ] . ACM Transactions on Information and System Security (TISSEC) , 2005 , 8 ( 4 ): 351 - 387 .

ZHANG X . Formal model and analysis of usage control [D ] . Fairfax County , Virgina: George Mason University , 2006 .

JANICKE H , CAU A , ZEDAN H . A note on the formalisation of UCON [C ] // The 12th ACM Symposium on Access Control Models and Technologies .c 2007 : 163 - 168 .

MARTINELLI F , CAU A , ZEDAN H . A model for usage control in GRID systems [C ] // The Third International Conference on Security and Privacy in Communications Networks and the Workshops .c 2007 : 520 - 520 .

JAGADEESAN R , MARRERO W , PITCHER C et al . Timed constraint programming: a declarative approach to usage control [C ] // The 7th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming .c 2005 : 164 - 175 .

LAZOUSKI A , MARTINELLI F , MORI P , . Usage control in computer security: a survey [J ] . Computer Science Review , 2010 , 4 ( 2 ): 81 - 99 .

ZHANG X , SANDHU R , PARISI-PRESICCE F . Safety analysis of usage control authorization models [C ] // The 2006 ACM Symposium on Information, Computer and Communications Security .c 2006 , 6 243 - 254 .

RAJKUMAR P V , GHOSH S K , DASGUPTA P . Concurrent usage control implementation verification using the SPIN model checker [C ] // The Third International, CNSA 2010, Chennai, India . Berlin Heidelberg Springer .c 2010 ： 214 - 223 .

HOLZMANN G J . The model checker SPIN [J ] . IEEE Transactions on Software Engineering , 1997 , 23 ( 5 ): 279 - 295 .

SUN J , LIU Y , DONG J S et al . PAT: towards flexible verification under fairness [C ] // The 21st International Conference on Computer Aided Verification .c 2009 ： 709 - 714 .

SUN J , LIU Y , DONG J S et al . Modeling and verifying hierarchical real-time systems using stateful timed csp [J ] . ACM Transactions on Software Engineering and Methodology(TOSEM) , 2013 , 22 ( 1 ): 139 - 176 .

VARDI M Y . An automata-theoretic approach to linear temporal logic [M ] // Logics for concurrency . Berlin Heidelberg: Springer , 1996 . 238 - 266 .

MCLEAN J . A comment on the ‘basic security theorem’of bell and LaPadula [J ] . Information Processing Letters , 1985 , 20 ( 2 ): 67 - 70 .

KATT B , HAFNER M , ZHANG X . A usage control policy specification with petri nets [C ] // The 5th International Conference on Collaborative Computing: Networking, Applications and Worksharing .c 2009 ： 1 - 8 .

LI N , TRIPUNITARA M V . Security analysis in role-based access control [J ] . ACM Transactions on Information and System Security (TISSEC) , 2006 , 9 ( 4 ): 391 - 420 .

ADI K , BOUZIDA Y , HATTAK I et al . Typing for conflict detection in access control policies [M ] // E-technologies: Innovation in An Open World . Berlin Heidelberg: Springer , 2009 ： 212 - 226 .

ZHANG N , RYAN M , GUELEV D P . Synthesising verified access control systems through model checking [J ] . Journal of Computer Security , 2008 , 16 ( 1 ): 1 - 61 .

LAMPORT L . The temporal logic of actions [J ] . ACM Transactions on Programming Languages and Systems (TOPLAS) , 1994 , 16 ( 3 ): 872 - 923 .

浏览量

1427

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于5G的智慧机场网络安全方案设计与安全性分析

基于模型检测的硬件木马检测技术研究

智能合约安全综述

密文长度可变的Simple Matrix加密方案