Execution-Time Opacity Logic: A Logic for Ensuring ET-Opacity in Timed Systems
The proposed Execution-Time Opacity Logic (ETOL), a new formalism that specifies opacity by requiring that for every execution satisfying a secret formula, there exists another execution of the same duration that does not satisfy it, enables efficient verification of execution-time confidentiality under timing attacks.