Yi-Chin Wu, Stéphane Lafortune: Synthesis of opacity-enforcing insertion functions that can be publicly known. CDC 2015: 3506-3513