Timed automata as a formalism for expressing security: A survey on theory and practice

TL;DR

This survey reviews two decades of research on using timed automata to verify security properties, highlighting theoretical foundations, practical applications, and open challenges in the field.

Contribution

It provides a comprehensive overview of security-related applications of timed automata, emphasizing theoretical insights, practical tools, and future research directions.

Findings

Focus on opacity in theoretical studies

Use of attack trees for practical security analysis

Identification of open challenges and tool support gaps

Abstract

Timed automata are a common formalism for the verification of concurrent systems subject to timing constraints. They extend finite-state automata with clocks, that constrain the system behavior in locations, and to take transitions. While timed automata were originally designed for safety (in the wide sense of correctness w.r.t. a formal property), they were progressively used in a number of works to guarantee security properties. In this work, we review works studying security properties for timed automata in the last two decades. We notably review theoretical works, with a particular focus on opacity, as well as more practical works, with a particular focus on attack trees and their extensions. We derive main conclusions concerning open perspectives, as well as tool support.