摘要：本文采用Clark-Wilson完整型模型,使用属性证书作为权限传递的载体,结合授权管理基础设施（PMI）实现基于角色的授权模型,并提出一种形式化描述架构,描述权限、证书和相关的授权;基于语义的演算过程对给定的属性证书集和撤销证书集可以验证某种权限是否有效;采用Alloy形式化语言来定义模型,并且给出描述扩展Clark-Wilson的方法。

关键词：证书 授权模型 

单位：湖南大学计算机与通信学院; 湖南长沙410082