Enforcing opacity of regular predicates on modal transition systems

Given a labelled transition system G partially observed by an attacker, and a regular predicate S e c over the runs of G, enforcing opacity of the secret S e c 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 S e c 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 S e c 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 I pound (a) denote the set of actions that can be observed by the attacker, and let I pound (c) and I pound (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 . We provide optimal and regular controllers that enforce the opacity of regular upper-closed secrets (S e c=S e c.I (au)) pound under the following assumptions: (i) or (ii) and for all I aI pound a-I pound pound (c) .