## 4 Modelling of TSP Executions
#### TIS for NSPKT Executions Modelling
For these components of the environment, we define the locations as follows: \(l\mathcal{E}_{0}^{1},l\mathcal{E}_{1}^{1}\), \(l\mathcal{E}_{2}^{1}\), \(l\mathcal{E}_{3}^{1},l\mathcal{E}_{0}^{2},l\mathcal{E}_{1}^{2}\), \(l\mathcal{E}_{2}^{1},l\mathcal{E}_{3}^{2},l\mathcal{E}_{3}^{2},\mathcal{Z}\), actions \(Act_{\mathcal{E}}=\{\alpha_{1}^{1},\alpha_{2}^{1},\overline{\alpha}_{2}^{1}, \alpha_{3}^{1},\overline{\alpha}_{1}^{2},\overline{\alpha}_{1}^{2},\)\(\alpha_{2}^{2},\alpha_{3}^{2},\overline{\alpha}_{3}^{2}\}\), and a set of clocks \(\mathcal{X}_{\mathcal{E}}=\{x_{0},x_{T_{A}},x_{T_{B}}\}\). As observed, the superscript indicates the protocol execution number. Notably, there are no additional clocks, as the Intruder does not generate any new information. Instead, he merely duplicates the information that he has intercepted. The additional actions, denoted by \(\overline{\alpha}_{j}^{i}\), represent the Intruder's enhanced capabilities. Specifically, he can retransmit the entire message if it has been intercepted previously or reconstruct it from individual components. An additional agent is introduced to represent the Intruder in the version that includes an attack. Automata also model the Intruder's knowledge (depicted in red in Figure 2). For the Intruder, we have two standard automata, \(\mathbb{A}_{T_{A}}^{I}\) and \(\mathbb{A}_{T_{B}}^{I}\), as well as an automaton that represents the possibility of the Intruder obtaining the entire message (\(\mathbb{A}_{\langle T_{A}\cdot T_{B}\rangle_{K_{A}}}^{I}\)). The automata \(\mathds{A}^{I}_{\langle T_{B}\rangle_{K_{B}}}\) and \(\mathds{A}^{I}_{\langle T_{A}\cdot i^{(A)}\rangle_{K_{B}}}\), which lack transitions between states \(l_{0}\) and \(l_{1}\) (Figure 2), model the Intruder's inability to proceed. We refer to these as _blocking automata_. Their inclusion allows the constructed interlacing model to be limited to only realistic behaviours. Thus, any path where the Intruder sends a message they could not formulate will not be represented. We define the local evolution functions similarly for the environment and the initial execution:  
\(t_{E}(l\mathcal{E}^{1}_{0},x_{0}>D_{1},\mathcal{O},\alpha^{1}_{1})=l\mathcal{E }^{1}_{1}\),  
\(t_{E}(l\mathcal{E}^{1}_{1},x_{0}>D_{2},\mathcal{O},\alpha^{1}_{1})=l\mathcal{E }^{1}_{2}\),  
\(t_{E}(l\mathcal{E}^{1}_{1},x_{0}>D_{2},\mathcal{O},\overline{\alpha}^{2}_{1})=l \mathcal{E}^{1}_{2}\),  
\(t_{E}(l\mathcal{E}^{1}_{2},x_{0}>D_{3},\mathcal{O},\alpha^{1}_{3})=l\mathcal{E }^{1}_{3}\);  
the second execution:  
\(t_{E}(l\mathcal{E}^{2}_{0},x_{0}>D_{4},\mathcal{O},\alpha^{2}_{1})=l\mathcal{ E}^{2}_{1}\),  
\(t_{E}(l\mathcal{E}^{2}_{0},x_{0}>D_{4},\mathcal{O},\overline{\alpha}^{2}_{1})=l \mathcal{E}^{2}_{1}\),  
\(t_{E}(l\mathcal{E}^{2}_{1},x_{0}>D_{5},\mathcal{O},\alpha^{2}_{2})=l\mathcal{ E}^{2}_{2}\),  
\(t_{E}(l\mathcal{E}^{2}_{2},x_{0}>D_{6},\mathcal{O},\alpha^{2}_{3})=l\mathcal{ E}^{2}_{3}\),  
Figure 2: Timed Interpreted System for Lowe attack on NSPKT. \(t_{\mathcal{E}}(l\mathcal{E}_{2}^{2},x_{0}>D_{6},\emptyset,\overline{\alpha}_{3}^{2 })=l\mathcal{E}_{3}^{2}\);  
and the resetting automaton:  
\(t_{\mathcal{E}}(\mathcal{Z},\emptyset,\{x_{0},x_{T_{\mathcal{E}}}\},a_{1}^{1})= \mathcal{Z}\),  
\(t_{\mathcal{E}}(\mathcal{Z},\emptyset,\{x_{0}\},a_{2}^{1})=\mathcal{Z}\),  
\(t_{\mathcal{E}}(\mathcal{Z},\emptyset,\{x_{0}\},a_{3}^{1})=\mathcal{Z}\),  
\(t_{\mathcal{E}}(\mathcal{Z},\emptyset,\{x_{0},x_{T_{\mathcal{E}}}\},a_{2}^{2})= \mathcal{Z}\),  
\(t_{\mathcal{E}}(\mathcal{Z},\emptyset,\{x_{0}\},a_{3}^{2})=\mathcal{Z}\).