## 4 Modelling of TSP Executions  
This section briefly overviews the foundational theory of security protocols and introduces our novel method for modelling the execution of Timed Security Protocols as Timed Interpreted Systems. Security Protocols are distributed algorithms that define a sequence of data exchanges during communication within a network. During the execution of a protocol, the actions of the involved parties can be categorised into internal actions-such as generating new confidential information, encrypting and decrypting cryptograms, comparing data, or performing mathematical operations on locally stored data--and external actions, which involve the mutual transmission of information between the parties. To illustrate our new method clearly, we have selected an example involving the timed version of the Needham-Schroeder Public-Key Protocol (NSPKT) [46]. The NSPKT, presented in Alice-Bob notation, proceeds as follows:  
\(\alpha_{1}\) \(A\to B:(T_{A}\cdot i(A))_{K_{B}}\),  
\(\alpha_{2}\) \(B\to A:(T_{A}\cdot T_{B})_{K_{A}}\),  
\(\alpha_{3}\) \(A\to B:(T_{B})_{K_{B}}\). In the first step, \(\alpha_{1}\), user \(A\) initiates communication by sending an encrypted message to user \(B\). This message includes the timestamp (ticket) \(T_{A}\) generated by \(A\) and the identifier \(i(A)\). The user \(B\) decrypts the message to obtain the ticket \(T_{A}\). In response, during the second step, \(\alpha_{2}\), the user \(B\) generates their own ticket \(T_{B}\) and combines it with the ticket \(T_{A}\) in an encrypted message, which is then sent back to \(A\). In this manner, it appears that \(B\) is authenticating to \(A\). Subsequently, the user \(A\) decrypts the received message and returns the timestamp \(T_{B}\) to \(B\). Again, this appears to authenticate user \(A\) to user \(B\). Since 1978, the NSPK protocol was widely used until 1995, when [PERSON] discovered an attack [47] that involved two interlaced executions of the protocol. \(\alpha_{1}^{1}\) \(A\to I\) : \(\langle T_{A}\cdot i(A)\rangle_{K_{I}}\),  
\(\alpha_{2}^{1}\) \(I(A)\to B\) : \(\langle T_{A}\cdot i(A)\rangle_{K_{B}}\),  
\(\alpha_{3}^{2}\) \(B\to I(A)\) : \(\langle T_{A}\cdot T_{B}\rangle_{K_{A}}\),  
\(\alpha_{4}^{2}\) \(A\to B\) : \(\langle T_{A}\cdot T_{B}\rangle_{K_{A}}\),  
\(\alpha_{5}^{2}\) \(A\to B\) : \(\langle T_{A}\cdot T_{B}\rangle_{K_{A}}\),  
\(\alpha_{6}^{2\(\alpha_{2}^{1}\)\(I\to A\ :\ \langle T_{A}\cdot T_{B}\rangle_{K_{A}}\),  
\(\alpha_{3}^{1}\)\(A\to I\ :\ \langle T_{B}\rangle_{K_{I}}\),  
\(\alpha_{3}^{2}\)\(I(A)\to B\ :\ \langle T_{B}\rangle_{K_{B}}\). The executions \(\alpha^{1}\) and \(\alpha^{2}\) cannot occur independently. In the first execution, \(\alpha^{1}\), an honest user \(A\) sends a message to the user \(I\). Here, the Intruder \(I\) acts like a normal user. In the second execution, \(\alpha^{2}\), the Intruder impersonates a user \(A\) and relays information from \(A\) to \(B\). In doing so, the Intruder deceives \(B\) by assuming the identity of \(A\). Before commencing the modelling process, several underlying assumptions must be considered. Firstly, honest users generate dedicated, confidential information only once for a given execution and do not reuse it. The Intruder, however, is capable of generating keys, timestamps, and messages for backup purposes, storing them, copying elements from others, presenting them as their own, impersonating users, and taking control. Encryption is assumed to be secure, and the Intruder cannot decrypt messages without the appropriate key. The Intruder may intercept communication and attempt to exploit any information gained after earning the trust of honest users. Additionally, it is essential to consider temporal dependencies, such as lifetimes and delays. All of these assumptions are incorporated into our modelling approach. In this work, as in [7], we treat a TSP as an abstract object.