基于π演算的工作流访问控制建模及安全性验证

为了保证工作流管理系统的正常运行，必须采用形式化的方法来分析和验证工作流管理系统的正确性和安全性。目前对工作流管理技术的研究大多集中在工作流结构的正确性验证和工作流性能分析上，缺少对工作流系统安全性的分析和验证。本课题拟采用基于π演算的形式化方法对工作流访问控制系统进行建模，在此基础上通过类型分析和模型检测的方法来保证工作流访问控制系统的安全。通过类型分析的方法可以对工作流模板进行类型一致性检查从而保证类型安全。而通过模型检测的方法可以验证对工作流的授权是否满足系统的安全策略。通过这两种方法的分析，可以查找和定位出工作流管理系统中违反安全策略的权限设置，为系统管理员设计工作流模板提供安全方面的指导。本课题的研究工作通过将π演算及其分析方法引入到工作流的安全分析中，对安全工作流管理系统的开发和验证提供理论指导与工程方法。