## 1 Introduction  
Security Protocols (SPs) play a fundamental role in ensuring the secure exchange of data across communication systems. The primary objectives of these protocols include achieving unilateral or bilateral authentication of the communicating parties, preserving the confidentiality and integrity of the transmitted information, and distributing new session keys that enable encrypted and secure communication channels. SPs, such as widely implemented communication protocols, are typically integral components of larger systems. However, both literature and practical network implementations have revealed numerous flaws in existing SP schemes, such as those found in the Needham-Schroeder Public Key Authentication protocol (NSPK) [1], CCITT X.509 [2], and the Wide Mouth Frog (WMF) protocol [3], among others. Identifying these vulnerabilities underscores the critical need for robust methods to verify the properties of SPs to ensure their correctness and security. Introducing temporal elements into SP schemes significantly increases the complexity of their modelling and verification processes but also enhances the model's expressiveness by allowing the consideration of time-dependent security properties. However, modellingtime accurately in the context of security protocols is inherently challenging, and addressing time-related security properties is even more complex. Timed Interpreted Systems (TISs) [4] offer an advanced framework for cryptographic protocol verification by incorporating the temporal dimension, which is crucial for accurately modelling and analysing protocols that rely on time constraints. TISs extend traditional interpreted systems by enabling reasoning about the timing of actions, essential for detecting and mitigating time-based attacks, such as replay or delay attacks. By explicitly modelling timing requirements, TISs can verify time-sensitive properties, such as the timely delivery or expiration of cryptographic tokens, ensuring that these properties are upheld throughout the execution of the protocol [5; 6; 7]. Additionally, TISs facilitate the verification of liveness properties, such as guaranteeing that a protocol completes within a specified time frame, which is critical for protocols requiring responsiveness [8]. TISs are particularly effective in analysing scenarios where synchronization between agents is necessary, such as in multi-party cryptographic protocols, thereby enhancing resilience against synchronization-related vulnerabilities [9]. They provide a formal framework to model and reason about temporal aspects, including timeouts, delays, and deadlines, which are crucial in cryptographic operations like key exchange and session management [10]. By integrating time into epistemic logic, TISs enable the verification of temporal-epistemic properties, such as ensuring that \"an agent knows within a certain time that a message has been securely received\", which is vital for secure communication protocols [4; 11]. Furthermore, TISs improve the modelling of network delays and processing times, critical factors affecting real-world cryptographic protocols' security [12]. They allow for a more realistic analysis of how time impacts protocol security under various environmental conditions, such as in mobile networks or high-latency settings, thereby providing more robust security guarantees [13]. TIS also ensures that security properties are maintained in logical terms and within the required time constraints, thus enhancing the practical security of cryptographic systems [14]. This comprehensive temporal modelling leads to more robust cryptographic protocol designs that are better equipped to withstand real-world, timing-based threats. The primary objective of this paper is to present a novel method for modelling and analysing protocol executions, taking into account the temporal relationships and dependencies among the time primitives involved, such as ticket generation times, validity periods, and data transmission times within the network.