## 4 Modelling of TSP Executions
#### TIS for NSPKT Executions Modelling  
We now explain how the previously defined structures are utilised to build the TIS model for NSPKT executions. Translating the protocol specified in ProToc into a Timed Interpreted System extends the method presented in [7]. The execution automata represent the transmission of messages within the network. Each execution of the protocol is modelled as a distinct automaton, where each transition corresponds to a single step of the protocol. Additionally, we introduce a separate automaton that models the system's time clock. The collection of all such automata constitutes the environment of our TIS model. In real network scenarios, the execution of protocols depends on the user's knowledge, as every step can only be executed with the user possessing the requisite knowledge. To represent this, we define and employ knowledge automata that model the knowledge of users [7]. For instance, an automaton \(\mathds{A}^{A}_{T_{A}}\) models the knowledge of the user \(A\) regarding the timestamp \(T_{A}\). These automata function similarly to characteristic functions over the set of knowledge primitives. They consist of two states: the first states indicate that the user lacks a particular piece of knowledge (such as \(T_{A}\)), while the second state represents the situation where the user has acquired that knowledge (\(T_{A}\)). In such automata, the first transition model possesses the process of the proper primitive, and the loop in the second state models the necessity of knowing a primitive for executing a protocol's step. These loops are specific guards for executing steps from the user's knowledge point of view. In this way, we can model the protocol's executions as the work of a TIS system that consists of three agents: a collection of automata that model the environment (executions automata [7] and clock automaton) and the users that execute the protocol (modelled by knowledge automata). Firstly, for the honest execution of NSPKT, we have the following structure (Figure 1). This system involves three agents: one representing each honest user and one representing the environment. Within the model, we distinguish automata that map the execution of the protocol (the first one in Figure 1) and the clock automaton, which can reset each clock within the system. The product of these automata constitutes the environment \(\mathcal{E}\). We also differentiate a network of synchronised automata that model the knowledge of individual agents, with blue representing agent \(A\) and green representing agent \(B\). For the components of the environment depicted, we consider the locations: \(l\mathcal{E}_{0}\), \(l\mathcal{E}_{1}\), \(l\mathcal{E}_{2}\), \(l\mathcal{E}_{3}\), \(\mathcal{Z}\); the actions associated with the protocol steps, \(Act_{\mathcal{E}}=\alpha_{1},\alpha_{2},\alpha_{3}\); and a set of clocks \(\mathbb{X}_{\mathcal{E}}=x_{0},x_{T_{A}},x_{T_{B}}\). The clock \(x_{0}\) serves as a global clock, reflecting the passage of time between individual steps. Thus, to transition to the next state, a certain amount of time \(D_{i}\) must elapse, where \(i\) denotes the step number. The value of \(D_{i}\) corresponds to the time required for ticket generation, encryption, message creation, or decryption. In some steps of the protocol, encryption or decryption time is not considered; this occurs when users send encrypted messages they received earlier or need more knowledge to decrypt the message. Therefore, each transition depends on the time condition--guard \(x_{0}>D_{i}\), and for every step, the global clock is reset \(\{x_{0}\}\). The agent used the other two clocks to check the validity of the generated data. They are reset in transitions, during which the appropriate ticket is generated. For example, the environment's clock \(x_{T_{A}}\), corresponding to the ticket \(T_{A}\), is reset when a transition labelled with the action \(\alpha_{1}\) is executed because \(T_{A}\) is generated in this step.