The paper Enforcement and Validation (at runtime) of Various Notions of Opacity has been accepted to Discrete Event Dynamic Systems, a Springer journal. This is an extended version of our paper that appeared in CDC 2013. One of the new contributions of this paper is to introduce what we call K-step strong opacity.
The abstract of the paper is below.
We are interested in the validation of opacity. Opacity models the impossibility for an attacker to retrieve the value of a secret in a system of interest. Roughly speaking, ensuring opacity provides confidentiality of a secret on the system that must not leak to an attacker. More specifically, we study how we can model-check, verify and enforce at system runtime, several levels of opacity. Besides existing notions of opacity, we also introduce K-step strong opacity, a more practical notion of opacity that provides a stronger level of confidentiality.
A pre-print of the paper can be downloaded here.
This is joint work with Hervé Marchand, from Inria Rennes.