安全组管理模型研究

形式化方法是研究复杂管理系统的有用工具。本文提出一个基于状态的安全组管理形式模型，采用Z Notation语言描述。安全组是共享组密钥的授权成员的集合，本文不是直接定义安全组而是定义组状态，组状态是某一时刻的组安全上下文，组的安全性和可靠性描述为某时刻组状态的性质。组管理过程是事件触发的组状态的变换过程，其终极目标是保证组在任一个稳定时刻都处于安全状态，但完全安全是不可能的。本文给出一个组策略框架，在此框架下提出安全组管理行为规则，并说明根据规则组状态转换过程满足安全策略约束。

Formal Model for Secure Group Management

Formal method is useful and important for researching complicated management systems. A state-based model for sec-group management is presented in this paper. Using Z Notation language, group is defined as an association of group members and group keys. Group security and soundness are described as properties of group state at a time. The management system is modeled as a state transition system triggered hy management events. The purpose of secgroup management is to maintain the group in a secure state at any stable time, but completely security is hardly possible. Given a group policy framework, we describe a suit of action rules and state that group is secure restricted in the framework under the rules.