## 2 Related Work  
The application of timed automata and timed multi-agent systems (MAS) in verifying cryptographic protocols has gained significant momentum in recent years, underscoring the critical importance of temporal aspects in securing communication protocols and systems. Recent studies reflect this evolution by addressing the challenges of time-sensitive attacks, enhancing security features, and ensuring system robustness under various operational conditions. Since the 1990s, researchers have proposed numerous methodologies for verifying the properties of security protocols. Beyond basic real or virtual simulations, several mathematical approaches, including inductive and deductive methods, have been introduced [19]. These methods prove that a given protocol possesses a specific security property. Currently, the most effective methods in this domain involve model checking of transition systems that encode user behaviour, including their knowledge during the execution of a protocol [7; 17; 20; 21; 22; 23]. In recent years, there has been an increasing need to consider the properties of time-dependent protocols, which is inherently challenging due to the complexity of time models. Only a few well-founded approaches address time dependencies between protocol parameters or user behaviours [24; 25; 26]. Several notable proposals utilise MAS for verification purposes within the extensive literature on the verification of timed security protocols (TSPs). For example, ref. [27] introduces a new MAS-based semantics for security protocol verification called LDYIS, which employs rewriting rules for the automatic generation of protocol runs, where certain temporal epistemic logic can be interpreted. In [28], the authors formalise the concept of attack detectability within MAS and demonstrate its application to a variant of the Kerberos protocol. These approaches have also been applied to more complex systems, like e-voting protocols. In [29], the same authors propose a new technique for automatically verifying protocols specified in the CAPSL language [30]. They define translation models based on CAPSL descriptions into Interpreted Systems, the most widely used semantics for temporal-epistemic logic. The method also includes rewriting protocol goals expressed in CAPSL into temporal-epistemic formulas, which are then linked to the MCMAS symbolic model checker for verification. The study presented in [31] addresses the analysis of security protocol properties for an unbounded number of sessions. The authors define a parameterised model-checking problem based on security requirements formulated in temporal-epistemic logic, focusing on authentication and key-establishment protocols. A specialised tool is proposed and utilised to verify the properties of the NSPK and ASRPC (Andrew Secure RPC Remote Procedure Call) protocols. However, these MAS-based approaches must address the temporal aspects of security protocols. The difficulty of modelling time has limited the development of solutions addressing the temporal properties of TSPs. Notable contributions include works such as [7; 32; 33; 34], which incorporate time primitives into formal modelling systems to describe and verify temporal properties. One of the earliest studies on TSP verification [32; 33], employed different types of Timed Automata (TA) for formal TSP modelling. In [7], the authors adapted Networks of Timed Synchronised Automata (TSA) for TSP verification. In a subsequent study [35], a systematic method was developed to formally specify and automatically verify timed security protocols with clock drift. In [24], a parametric verification approach for TSPs was proposed using a timed version of calculus for specification. This method defines its formal semantics as a transition structure constructed over timed logic rules, facilitating the efficient verification of TSP properties. The authors also introduced the concept of minimal network latency, describing the time required for message composition (including encryption) within the network.