.png){kind=icon}
.png){kind=icon}
Return
Strong state-based opacity verification using HyperLTL model checking technique
.png){kind=icon}
PRE
AI
DOI：10.1080/00207179.2025.2608824.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
Opacity is an important information-flow security property for characterizing various security and privacy requirements in diverse dynamic systems. As a suitable paradigm for expressing the properties of information flows, HyperLTL has been proven to use a unified Kripke structure to simultaneously verify three types of standard versions of state-based opacity (i.e. initial-state opacity, current-state opacity, and infinite-step opacity). However, the verification of three types of stronger versions of state-based opacity has not been studied under the framework of HyperLTL. To this end, in this paper we provide the HyperLTL formula of strong state-based opacity based on a modified Kripke structure to develop an automated verification method. Furthermore, we remove two assumptions of deadlock-free and divergence-free existing in prior research by adding a sink state to the original system when a deadlock state or/and an unobservable cycle exists. This extends the applicability of the HyperLTL method.
Keywords:
Discrete-event system
opacity
HyperLTL
Kripke structure
verification
Journal
I
IF:
1.6
Papers:
85
Citations:
0