一种基于标签时间Petri网的当前状态不透明性验证方法

本发明属于信息安全技术领域，具体涉及一种基于标签时间Petri网的当前状态不透明性验证方法，包括建立待验证系统的标签时间Petri网模型，通过利用与变迁序列相关的时间约束，提出一种基于线性规划的方法以判定与给定时间一致的逻辑变迁序列，构建与给定时间一致的关键MSCG，在关键MSCG中寻求其标识属于秘密集且为可观测标识的状态类，并确定可以到达这些状态类的可观测标签序列，基于关键MSCG，通过判断与给定时间和可观测标签序列相一致的逻辑标识集是否包含于秘密集。本发明提出一种无需列举与给定时间和所有观测标签序列相一致的状态类的方法判断系统关于秘密集在给定时间内是否为当前状态不透明,较大程度上降低了具有时间要求的系统受到攻击的危害。