Skip to Main content Skip to Navigation
Journal articles

Enforcing Opacity of Regular Predicates on Modal Transition Systems

Abstract : Given a labelled transition system G partially observed by an attacker, and a regular predicate Sec over the runs of G, enforcing opacity of the secret Sec in G means computing a supervisory controller K such that an attacker who observes a run of the controlled system K/G cannot ascertain that the trace of this run belongs to Sec based on the knowledge of G and K. We lift the problem from a single labelled transition system G to the class of all labelled transition systems specified by a Modal Transition System M. The lifted problem is to compute the maximally permissive controller K such that Sec is opaque in K/G for every labelled transition system G which is a model of M. The situations of the attacker and of the controller are asymmetric: at run time, the attacker may fully know G and K whereas the controller knows only M and the sequence of actions executed so far by the unknown G. We address the problem in two cases. Let S_a denote the set of actions that can be observed by the attacker, and let S_c and S_o denote the sets of actions that can be controlled and observed by the controller, respectively. We provide optimal and regular controllers that enforce the opacity of regular secrets when S_c\subseteqS_o\subseteqS_a=S. We provide optimal and regular controllers that enforce the opacity of regular upper-closed secrets (Sec=Sec.S^*) under the following assumptions: (i) S_a\subseteqS_c\subseteqS_o=S or (ii) S_a,S_c\subseteqS_o=S and w\sigma\in Sec\Rightarrow w\in Sec for all \sigma\in S\S_c.
Document type :
Journal articles
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-00987988
Contributor : Hervé Marchand <>
Submitted on : Wednesday, May 7, 2014 - 9:58:47 AM
Last modification on : Friday, July 10, 2020 - 4:03:18 PM
Long-term archiving on: : Thursday, August 7, 2014 - 11:00:54 AM

File

jdeds.pdf
Files produced by the author(s)

Identifiers

Citation

Philippe Darondeau, Hervé Marchand, Laurie S. L. Ricker. Enforcing Opacity of Regular Predicates on Modal Transition Systems. Discrete Event Dynamic Systems, Springer Verlag, 2015, 25 ((1-2)), pp.251-270. ⟨10.1007/s10626-014-0193-7⟩. ⟨hal-00987988⟩

Share

Metrics

Record views

647

Files downloads

416