Verification paths.

This study addresses the problem of attack identification in discrete event systems modeled with Petri nets, focusing specifically on sensor attacks that mislead observers to making incorrect decisions. Insertion attacks are one of the sensor attacks that are considered in this work. First, we formulate a novel observation structure to systematically model insertion attacks within the Petri net framework. Second, by generating an extended reachability graph that incorporates the observation structure, we can find a special class of markings whose components can have negative markings. Third, an observation place is computed by formulating an integer linear programming problem, enabling precise detection of attack occurrences. The occurrence of an attack can be identified by the number of tokens in the designed observation place. Finally, examples are provided to verify the proposed approach. Comparative analysis with existing techniques demonstrates that the reported approach offers enhanced detection accuracy and robustness, making it a significant advancement in the field of secure discrete event systems.

本研究针对以佩特里网（Petri net）建模的离散事件系统（discrete event system）中的攻击识别问题展开，重点关注可误导观测者做出错误决策的传感器攻击（sensor attack）。插入攻击（insertion attack）是本文所考量的一类传感器攻击。首先，本文构建了一种新颖的观测结构，以在佩特里网框架内系统化地对插入攻击进行建模。其次，通过生成融合该观测结构的扩展可达性图，可得到一类特殊的标识（marking），其各分量可取负值。第三，通过构建整数线性规划问题求解得到一个观测库所（observation place），可实现对攻击发生的精准检测；攻击的发生与否可通过该设计的观测库所中的令牌（token）数量进行判定。最后，本文通过实例验证了所提方法的有效性。与现有技术的对比分析表明，本方法具备更优异的检测精度与鲁棒性，为安全离散事件系统领域带来了重要进展。