## 1 Introduction
We require a description in the language specified by the tool to verify protocol properties formally using specific verification tools. It necessitates strict language rules that prevent the direct use of traditional protocol message descriptions. Our approach begins by describing the timed protocol using the well-established Alice-Bob notation. We then formalise it using a time-extended version of the ProToc specification language, which captures all external and internal actions performed during the protocol. This description is subsequently used to automatically create a model of protocol executions with time dependencies as a TIS. This system models the behaviours of honest agents, the intruder, and the environment, all represented as networks of synchronizing timed automata [7]. We selected TIS for modelling Timed Security Protocol (TSP) executions due to limitations in previous approaches that modelled TSPs as networks of timed automata [7]. These approaches could not separate users from their operational environment, relied on non-interleaved semantics of timed automata-preventing the modelling of real-world SP executions-and only considered a single delay and lifetime parameter. Our proposed method addresses these limitations by expanding the number of analysed time parameters, enabling a deeper analysis. Furthermore, our approach utilises dense time semantics, which facilitates the analysis of a broader range of attacks [15; 16]. To automatically verify the fundamental security properties of TSPs, we employ Satisfiability Modulo Theories-based bounded model checking (SMT-BMC) [17; 18], a symbolic model-checking technique known for its efficiency in finding counterexamples and mitigating the state explosion problem. BMC operates by checking whether the negation of the property of interest holds in a pruned model up to a specific depth, reducing the problem to the satisfiability of a quantifier-free first-order formula. The structures created and utilised in our BMC method encompass all elements necessary for modelling and verifying timed protocol primitives, including ticket generation times, validity periods, and data transmission times across the network. The results demonstrate the ability to establish characteristic time dependencies that determine the correct functioning of each protocol. In conclusion, the primary contributions of this paper consist of a new formal verification approach for TSP security properties, which include:  
* Modelling TSP executions as timed interpreted systems with real-time, in which each agent (user) taking part in the protocol is modelled as a network of timed, synchronised automata--it is a more realistic solution compared with the previous ones;
* Expressing times of actions performed during the protocol's execution and the network delays (which include message generation times, encryption, decryption, and network transfer times)--using these, we can compute dependencies between these values and lifetimes of TSPs' time primitives (time tickets), which is essential when considering the possibility of an attack;
* The ability to detect and prevent the existence in the network of a passive Intruder in Man-in-the-Middle configurations;
* Considering a strongly monotonic version of dense timed semantics and many different lifetimes and their values;
* New, suitable implementation and experimental results. These ideas will be further developed and discussed in the subsequent sections.