天津科技大学学报2025，Vol.40Issue(3)：65-71,7.DOI:10.13364/j.issn.1672-6510.20240024
基于HyperLTL模型检测技术的K步不透明性验证
K-Step Opacity Verification Based on HyperLTL Model Checking Technology
摘要
Abstract
Opacity is an important information-flow security property used to characterize various security and privacy re-quirements in different dynamic systems.In discrete-event systems,K-step opacity describes the inability of an intruder to determine whether the system has accessed the secret state within K observation steps based on the current output observation sequence.As a suitable tool for expressing the properties of information flows,HyperLTL has been proven to use a unified Kripke structure to separately verify initial-state opacity,current-state opacity and infinite-step opacity.However,it does not involve K-step opacity.To solve the verification of the K-step opacity in HyperLTL,we added the Sink state to release the restriction condition of the original system.Then,we constructed the modified Kripke structure.Furthermore,we provided the HyperLTL formula of K-step opacity over the constructed modified Kripke structure for the purpose of verification.关键词
离散事件系统/K步不透明性/HyperLTL/改进的Kripke结构/Sink状态Key words
discrete-event system/K-step opacity/HyperLTL/modified Kripke structure/Sink state分类
计算机与自动化引用本文复制引用
任翔,王子佩,张佳慧,韩晓光..基于HyperLTL模型检测技术的K步不透明性验证[J].天津科技大学学报,2025,40(3):65-71,7.基金项目
国家自然科学基金项目(61903274) （61903274）
天津市教委科研计划一般项目(2019KJ212) （2019KJ212）
