Verifying Opacity of Discrete-Timed Automata

This is the authors' abstract. We don't add key points for this paper.

Opacity is a powerful confidentiality property that holds if a system cannot leak secret information through observable behavior. In recent years, time has become an increasingly popular attack vector. The notion of opacity has therefore been extended to timed automata (TA). However, the verification of opacity of TA has been proven to be undecidable for the commonly used dense time model. To make the problem decidable, state of the art approaches consider weaker notions of opacity or heavily restrict the class of considered TA, resulting in unrealistic threat models.