## 4 Modelling of TSP Executions
#### TIS for NSPKT Executions Modelling
We assume the following local evolution functions for the environment:  
\[t_{\mathcal{E}}(l\mathcal{E}_{0},x_{0}>D_{1},\mathcal{O},\alpha_{1})=l \mathcal{E}_{1},\]  
Figure 1: Timed Interpreted System for NSPKT. \(t_{\mathcal{E}}(\mathcal{Z},\mathcal{O},\{x_{0},x_{T_{A}}\},\alpha_{1})= \mathcal{Z}\), \(t_{\mathcal{E}}(l\mathcal{E}_{1},x_{0}>D_{2},\mathcal{O},\alpha_{2})=l\mathcal{E}_ {2}\), \(t_{\mathcal{E}}(\mathcal{Z},\mathcal{O},\{x_{0},x_{T_{B}}\},\alpha_{2})= \mathcal{Z}\), \(t_{\mathcal{E}}(l\mathcal{E}_{2},x_{0}>D_{3},\mathcal{O},\alpha_{3})=l \mathcal{E}_{3}\), \(t_{\mathcal{E}}(\mathcal{Z},\mathcal{O},\{x_{0}\},\alpha_{3})=\mathcal{Z}\). As previously noted, agents are modelled using knowledge models. Each automaton, \(\mathbb{A}_{Y}^{X}\), represents the process by which a given agent \(X\) gains knowledge about a specific piece of data \(Y\). For instance, the automaton \(\mathbb{A}_{T_{A}}^{A}\) models the agent's behaviour \(A\) concerning the data \(T_{A}\). These automata have two possible states: \(l_{0}\)--representing the absence of knowledge, and \(l_{1}\)--representing possession of knowledge. Additionally, there are temporal conditions to consider. For example, in the case of \(\mathbb{A}_{T_{A}}^{B}\), during the action \(\alpha_{1}\), a check is performed to determine whether the validity period of the information has expired, specified by \(x_{T_{A}}<L_{T_{A}}\). It is important to note that we distinguish different lifetimes for different tickets, as the later a ticket is generated, the shorter its duration is during the protocol's execution. The local evolution functions for \(T_{A}\) and \(T_{B}\) are:  
\(t_{A}(l_{0},l\mathcal{E}_{0},true,\mathcal{O},\alpha_{1})=l_{1}\),  
\(t_{A}(l_{1},l\mathcal{E}_{1},x_{T_{A}}<L_{T_{A}},\mathcal{O},\alpha_{2})=l_{1}\),  
\(t_{B}(l_{0},l\mathcal{E}_{0},x_{T_{A}}<L_{T_{A}},\mathcal{O},\alpha_{1})=l_{1}\),  
\(t_{B}(l_{1},l\mathcal{E}_{1},x_{T_{A}}<L_{T_{A}},\mathcal{O},\alpha_{2})=l_{1}\),  
\(t_{A}(l_{0},l\mathcal{E}_{1},x_{T_{B}}<L_{T_{B}},\mathcal{O},\alpha_{2})=l_{1}\),  
\(t_{A}(l_{1},l\mathcal{E}_{2},x_{T_{B}}<L_{T_{B}},\mathcal{O},\alpha_{3})=l_{1}\),  
\(t_{B}(l_{0},l\mathcal{E}_{1},true,\mathcal{O},\alpha_{2})=l_{1}\),  
\(t_{B}(l_{1},l\mathcal{E}_{2},x_{T_{B}}<L_{T_{B}},\mathcal{O},\alpha_{3})=l_{1}\). Analysing a single execution typically does not suffice to identify an attack. It is necessary to consider multiple executions, including those involving the Intruder, who will intertwine these executions precisely as they would occur in reality. There are three steps for each execution, and we can intertwine all of them. The rule is that the order of the steps within a single execution must be preserved, and a step cannot be executed if the sender does not possess the necessary knowledge to perform it. The second condition significantly reduces the search space. For example, consider the analysis of step \(\alpha_{3}^{2}\). This step cannot be executed immediately after step \(\alpha_{2}^{2}\) because the Intruder does not know the \(T_{B}\) ticket (he cannot decode the information received from \(B\)). In our model, the Intruder can continue operations (allowing appropriate transitions in the automata) by either sending complete information (as in step \(\alpha_{2}^{1}\)) or by gathering the necessary individual components during the interlacing steps (as in \(\alpha_{1}^{1}\) and \(\alpha_{3}^{1}\)). Three automata are required to model the attack on the NSPKT protocol in the form of a TIS (Figure 2), where their combined product represents the environment. Two of these automata are utilised to model the protocol's execution, while the third automaton is responsible for resetting the clocks.