Enforcing Opacity of Regular Predicates on Modal Transition Systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Discrete Event Dynamic Systems Année : 2015

Enforcing Opacity of Regular Predicates on Modal Transition Systems

Résumé

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.
Fichier principal
Vignette du fichier
jdeds.pdf (243.65 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00987988 , version 1 (07-05-2014)

Identifiants

Citer

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

Altmetric

Partager

Gmail Facebook X LinkedIn More