离散事件系统强K步不透明性的验证
密码学与安全
2022-04-12 v1 形式语言与自动机理论
摘要
本文重新考察以非确定有限状态自动机建模的部分可观离散事件系统的强K步不透明性(K-SSO)验证问题。作为标准K步不透明性的更强版本,K-SSO要求入侵者无法确信在过去的K个可观步内是否访问过秘密状态。为高效验证K-SSO,我们提出一种新的并发组合结构,其为我们先前提出结构的一个变体。基于此新结构,我们设计了一个判定K-SSO的算法,并证明所提算法不仅降低了已有算法的时间复杂度,且不依赖于K的取值。此外,推导出了K-SSO中K值的新上界,该上界也降低了文献中已有的K值上界。最后,通过一个简单示例说明了所提算法。
引用
@article{arxiv.2204.04698,
title = {Verification of Strong K-Step Opacity for Discrete-Event Systems},
author = {Xiaoguang Han and Kuize Zhang and Zhiwu Li},
journal= {arXiv preprint arXiv:2204.04698},
year = {2022}
}
备注
6 pages, 2 figures, submitted to IEEE CDC on March 28, 2022