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

• 作者: 刘志锋 周从华 陈伟鹤
• 来源期刊: 网络与信息安全学报
• 学科: 工学
• 关键词: UCON 形式化规约 安全性分析 模型检测
• 年，卷（期）: 2016,（3）
• 所属期刊栏目: 学术论文
• 页码范围: 00038-1-00038-16
• 页数: 1页
• 分类号: TP309.7
• 字数: 16689字
• 语种: 中文
• DOI: 10.11959/j.issn.2096-109x.2016.00038

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	周从华	江苏大学计算机科学与通信工程学院	46	193	7.0	11.0
2	刘志锋	江苏大学计算机科学与通信工程学院	29	118	5.0	10.0
3	陈伟鹤	江苏大学计算机科学与通信工程学院	21	410	7.0	20.0