离散事件系统的强当前状态与强初始状态不透明性

不透明性作为信息流安全中的重要性质，刻画了系统对入侵者隐藏某些秘密信息的能力。在离散事件系统中，基于入侵者完全掌握系统结构的标准设定，当前状态不透明性与初始状态不透明性的标准版本无法完美刻画高层隐私需求。为克服此局限，本文提出部分可观测离散事件系统中两种更强的不透明性版本，称为强当前状态不透明性（strong current-state opacity）与强初始状态不透明性（strong initial-state opacity）。强当前状态不透明性描述入侵者永远无法确切判断系统当前是否处于秘密状态，即若系统满足该性质，则对每条以秘密状态结束的系统运行，存在一条非秘密运行，其观测与前述运行相同。强初始状态不透明性刻画入侵者在任意时刻均无法推断初始时刻对秘密状态的访问。具体而言，若每条从秘密状态开始的运行都存在一条系统的非秘密运行与其观测相同，则称系统为强初始状态不透明的。为验证这两种性质，我们提出两种使用新颖并发组合技术的信息结构，其时间复杂度为指数级 $O(|X|^4|\Sigma_o||\Sigma_{uo}||\Sigma|2^{|X|})$，其中 $|X|$（相应地 $|\Sigma|$、$|\Sigma_o|$、$|\Sigma_{uo}|$）为系统的状态数（相应地事件数、可观测事件数、不可观测事件数）。