Synthesis of an Obfuscation Policy that Guarantees Utility Satisfying a New Privacy Criterion

Nowadays, with the advancement of technology, several systems are connected through computer networks, which makes it necessary to develop techniques capable of guaranteeing the privacy and utility of the transmitted information. In this work, we consider the synthesis of an obfuscation policy of Discrete Event Systems that guarantees utility satisfying a new privacy criterion. The system is modeled as a labeled transition system with secret states. The first goal is to keep the information generated by the system useful so that legitimate users can use it for decision making. At the same time, the second goal is to hide critical information about the secret states of the system from attackers. However, unlike previous approaches presented in the literature, we consider the case in which it is possible for the obfuscator to report the secret states if the actual state of the system is in a safe region. Thus, this approach increases the number of systems that can be obfuscated. The software SynthSMV is used to perform the obfuscator synthesis.