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.
Type de document :
Article dans une revue
Discrete Event Dynamic Systems, Springer Verlag, 2014, pp.20. 〈http://dx.doi.org/10.1007/s10626-014-0193-7〉. 〈10.1007/s10626-014-0193-7〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00987988
Contributeur : Hervé Marchand <>
Soumis le : mercredi 7 mai 2014 - 09:58:47
Dernière modification le : mercredi 16 mai 2018 - 11:24:06
Document(s) archivé(s) le : jeudi 7 août 2014 - 11:00:54

Fichier

jdeds.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Philippe Darondeau, Hervé Marchand, Laurie S. L. Ricker. Enforcing Opacity of Regular Predicates on Modal Transition Systems. Discrete Event Dynamic Systems, Springer Verlag, 2014, pp.20. 〈http://dx.doi.org/10.1007/s10626-014-0193-7〉. 〈10.1007/s10626-014-0193-7〉. 〈hal-00987988〉

Partager

Métriques

Consultations de la notice

469

Téléchargements de fichiers

139