Synthesis of opacity-enforcing insertion functions that can be publicly known

Our prior work has studied the enforcement of opacity, a security property, using insertion functions that insert fictitious events at the output of the system, thereby preventing an intruder from inferring the given system´s secret. The insertion functions previously considered enforce opacity under the assumption that the intruder does not know about the implementation of the insertion function. In this paper, we relax that assumption and consider a stronger class of insertion functions that enforce opacity whether or not the intruder knows the insertion function. This property is formally characterized as public-and-private enforceability, or PP-enforceability for short. A PP-enforcing insertion function is guaranteed to output only behaviors consistent with the non-secret behaviors of the system and thus it enforces opacity when the intruder has no knowledge of the insertion function (private case). Moreover, a PP-enforcing insertion function guarantees that the intruder can never infer the occurrence of the secret, even when the intruder knows the exact implementation of the insertion function (public case). We characterize the property of PP-enforceability and present an algorithm that provably synthesizes a PP-enforcing insertion function.