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

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