基于Petri网的保密策略建模与自动化验证方法

本文主要探讨了"基于Petri网的保密性策略建模与验证"这一主题，发表在2007年的华中科技大学学报(自然科学版)第35卷第10期。论文由张明理、洪帆和廖俊国三位作者共同完成，他们来自华中科技大学计算机科学与技术学院，地址位于湖北省武汉市。 核心研究目标是针对那些实施了具体保密性策略的系统、进程或工作流，设计一种有效的方法来分析和验证其保密性。传统的保密性评估可能不足以全面捕捉复杂的系统行为，因此，作者提出了一种创新的方法，即利用Petri网作为工具。Petri网是一种图形模型，用于描述系统动态行为，通过它可以形式化地表达保密性策略。 首先，论文构建了保密性策略的Petri网形式化描述，这是一种标准化的语言，使得策略的抽象和理解更加直观。通过这种方法，系统的行为可以被转化为Petri网模型，其中节点代表活动或事件，边表示它们之间的依赖关系。 接着，作者利用这个模型，结合保密性策略基于Petri网的形式化描述，构建覆盖图来对系统的保密性进行深入分析。覆盖图有助于揭示系统中的关键路径和敏感信息流动，从而判断系统是否满足保密性策略的规定。这种方法的优点在于，由于系统Petri网模型的覆盖图可以自动生成，因此可以实现保密性验证的自动化，节省了大量的人力和时间。 文中通过一个具体的进程实例来详细解释了这种方法的操作步骤和实施过程，包括模型的构建、策略应用、覆盖图生成以及最终的验证结果。这不仅展示了理论的应用潜力，也提供了实际操作的指南。 关键词"保密性策略"、"Petri网"和"模型验证"表明了文章的核心研究内容，同时也揭示了它在信息安全领域的重要地位。这篇论文的研究成果对于理解和保护具有保密需求的系统具有重要的实践价值，尤其是在处理复杂工作流和多进程协作的场景中。 该研究将Petri网理论与保密性策略相结合，提供了一种新颖且实用的方法，能够提升保密性分析的准确性和效率，对于提高信息系统安全性具有显著的意义。