Timed Interpreted Systems as a New Agent-Based Formalism for Verification of Timed Security Protocols

Abstract

This article introduces a new method for modelling and verifying the execution of timed security protocols (TSPs) and their time-dependent security properties. The method, which is novel and reliable, uses an extension of interpreted systems, accessible semantics in multi-agent systems, and timed interpreted systems (TISs) with dense time semantics to model TSP executions. We enhance the models of TSPs by incorporating delays and varying lifetimes to capture real-life aspects of protocol executions. To illustrate the method, we model a timed version of the Needham–Schroeder Public Key Authentication Protocol. We have also developed a new bounded model checking reachability algorithm for the proposed structures, based on Satisfiability Modulo Theories (SMTs), and implemented it within the tool. The method comprises a new procedure for modelling TSP executions, translating TSPs into TISs, and translating TISs’ reachability problem into the SMT problem. The paper also includes thorough experimental results for nine protocols modelled by TISs and discusses the findings in detail.

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, modelling time 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.

We require a description in the language specified by the tool to verify protocol properties formally using specific verification tools. It necessitates strict language rules that prevent the direct use of traditional protocol message descriptions. Our approach begins by describing the timed protocol using the well-established Alice-Bob notation. We then formalise it using a time-extended version of the ProToc specification language, which captures all external and internal actions performed during the protocol. This description is subsequently used to automatically create a model of protocol executions with time dependencies as a TIS. This system models the behaviours of honest agents, the intruder, and the environment, all represented as networks of synchronizing timed automata [7]. We selected TIS for modelling Timed Security Protocol (TSP) executions due to limitations in previous approaches that modelled TSPs as networks of timed automata [7]. These approaches could not separate users from their operational environment, relied on non-interleaved semantics of timed automata–preventing the modelling of real-world SP executions–and only considered a single delay and lifetime parameter.

Our proposed method addresses these limitations by expanding the number of analysed time parameters, enabling a deeper analysis. Furthermore, our approach utilises dense time semantics, which facilitates the analysis of a broader range of attacks [15,16].

To automatically verify the fundamental security properties of TSPs, we employ Satisfiability Modulo Theories-based bounded model checking (SMT-BMC) [17,18], a symbolic model-checking technique known for its efficiency in finding counterexamples and mitigating the state explosion problem. BMC operates by checking whether the negation of the property of interest holds in a pruned model up to a specific depth, reducing the problem to the satisfiability of a quantifier-free first-order formula.

The structures created and utilised in our BMC method encompass all elements necessary for modelling and verifying timed protocol primitives, including ticket generation times, validity periods, and data transmission times across the network. The results demonstrate the ability to establish characteristic time dependencies that determine the correct functioning of each protocol.

In conclusion, the primary contributions of this paper consist of a new formal verification approach for TSP security properties, which include:

• Modelling TSP executions as timed interpreted systems with real-time, in which each agent (user) taking part in the protocol is modelled as a network of timed, synchronised automata—it is a more realistic solution compared with the previous ones;
• Expressing times of actions performed during the protocol’s execution and the network delays (which include message generation times, encryption, decryption, and network transfer times)—using these, we can compute dependencies between these values and lifetimes of TSPs’ time primitives (time tickets), which is essential when considering the possibility of an attack;
• The ability to detect and prevent the existence in the network of a passive Intruder in Man-in-the-Middle configurations;
• Considering a strongly monotonic version of dense timed semantics and many different lifetimes and their values;
• New, suitable implementation and experimental results.

These ideas will be further developed and discussed in the subsequent sections.

2. Related Work

The application of timed automata and timed multi-agent systems (MAS) in verifying cryptographic protocols has gained significant momentum in recent years, underscoring the critical importance of temporal aspects in securing communication protocols and systems. Recent studies reflect this evolution by addressing the challenges of time-sensitive attacks, enhancing security features, and ensuring system robustness under various operational conditions.

Since the 1990s, researchers have proposed numerous methodologies for verifying the properties of security protocols. Beyond basic real or virtual simulations, several mathematical approaches, including inductive and deductive methods, have been introduced [19]. These methods prove that a given protocol possesses a specific security property. Currently, the most effective methods in this domain involve model checking of transition systems that encode user behaviour, including their knowledge during the execution of a protocol [7,17,20,21,22,23].

In recent years, there has been an increasing need to consider the properties of time-dependent protocols, which is inherently challenging due to the complexity of time models. Only a few well-founded approaches address time dependencies between protocol parameters or user behaviours [24,25,26]. Several notable proposals utilise MAS for verification purposes within the extensive literature on the verification of timed security protocols (TSPs).

For example, ref. [27] introduces a new MAS-based semantics for security protocol verification called LDYIS, which employs rewriting rules for the automatic generation of protocol runs, where certain temporal epistemic logic can be interpreted. In [28], the authors formalise the concept of attack detectability within MAS and demonstrate its application to a variant of the Kerberos protocol. These approaches have also been applied to more complex systems, like e-voting protocols. In [29], the same authors propose a new technique for automatically verifying protocols specified in the CAPSL language [30]. They define translation models based on CAPSL descriptions into Interpreted Systems, the most widely used semantics for temporal-epistemic logic. The method also includes rewriting protocol goals expressed in CAPSL into temporal-epistemic formulas, which are then linked to the MCMAS symbolic model checker for verification.

The study presented in [31] addresses the analysis of security protocol properties for an unbounded number of sessions. The authors define a parameterised model-checking problem based on security requirements formulated in temporal-epistemic logic, focusing on authentication and key-establishment protocols. A specialised tool is proposed and utilised to verify the properties of the NSPK and ASRPC (Andrew Secure RPC Remote Procedure Call) protocols. However, these MAS-based approaches must address the temporal aspects of security protocols.

The difficulty of modelling time has limited the development of solutions addressing the temporal properties of TSPs. Notable contributions include works such as [7,32,33,34], which incorporate time primitives into formal modelling systems to describe and verify temporal properties.

One of the earliest studies on TSP verification [32,33], employed different types of Timed Automata (TA) for formal TSP modelling. In [7], the authors adapted Networks of Timed Synchronised Automata (TSA) for TSP verification. In a subsequent study [35], a systematic method was developed to formally specify and automatically verify timed security protocols with clock drift. In [24], a parametric verification approach for TSPs was proposed using a timed version of calculus for specification. This method defines its formal semantics as a transition structure constructed over timed logic rules, facilitating the efficient verification of TSP properties. The authors also introduced the concept of minimal network latency, describing the time required for message composition (including encryption) within the network.

Further contributions include [36], demonstrating how self-adaptive MAS can dynamically adjust to environmental changes using probabilistic timed automata to verify system behaviour and enhance operational stability. Similarly, ref. [37] presents a methodology integrating automata learning to improve timed systems’ synthesis and verification processes, signalling a shift towards automated and scalable solutions. The article [38] focuses on symbolic approaches for verifying timed cryptographic primitives, providing new tools for ensuring time-limited security properties in protocols like sealed-bid auctions and contract signing. Moreover, studies such as [39,40] explore novel techniques for analysing communication protocols’ temporal behaviour and correctness by integrating new logical frameworks and model-checking tools. These advancements emphasise the critical role of temporal dimensions in cryptographic protocol analysis, fostering a new era of research where timing constraints and behaviours are central to the verification process, ultimately enhancing the security and reliability of cryptographic systems.

However, these approaches often need to adequately account for the time required to compose and decompose messages, which is crucial for cryptographic operation protocols. In complex cases, the time required for message generation may exceed the network delay time. Additionally, the existing literature often assumes that the lifetime values are consistent across all timestamps and that the minimal network latency remains constant throughout all protocol steps. Furthermore, these studies do not explicitly differentiate between protocol users. Our new approach addresses all of these limitations identified in previous works.

3. Timed Interpreted Systems

Interpreted systems (ISs) [41] were initially developed to model distributed systems. However, with the increasing interest in Multi-agent Systems [42], the concept of ISs has evolved into a formalism for modelling, for example, communication between agents. Over the years, this formalism has been successfully extended [4,43,44]. The formalism of TISs, as presented in [4], enhances ISs by enabling reasoning about the discrete time aspects of MASs. In our work, we have extended this capability to reason about the real-time aspects of MASs. The primary advantage of employing dense time semantics is that timed models with dense time allow for abstraction from the specific rate at which clocks may tick. In contrast, using discrete-time semantics results in timed models where each clock ticks and measures time in discrete units.

3.1. The Intuition Behind Interpreted Systems, Interleaved Interpreted Systems and a Network of Timed Automata

Timed Interpreted Systems offer a powerful and expressive framework for modelling security protocols, especially when timing is critical. They enable the detailed analysis of time-dependent behaviours and vulnerabilities, providing insights that other models might overlook. However, these advantages have significant challenges, including increased complexity, resource demands, and scalability issues.

The previous approaches usually used timed automata to model security protocols.

To compare our new approach to modelling and verification security protocols to the existing ones, we present the intuition behind Timed Interpreted Systems, Timed Interleaved Interpreted Systems, and Timed Automata. The main difference and the crucial one lie in action synchronisation.

In standard interpreted systems, all agents perform actions synchronously [45]. This means that every agent in the system executes an action simultaneously at each discrete time step (often modelled as a global clock tick). The global state of the system transitions based on the combination of actions taken by all agents at that time step. The collective effect of these actions determines the system’s evolution. The system progresses in synchronised time steps where each agent acts. The system considers the joint action of all agents to determine the next global state. If the agents’ actions and the environment’s response are deterministic, the next state is uniquely determined by the current state and the agents’ actions. Agents may need to coordinate their actions, as they know other agents act simultaneously.

In interleaved interpreted systems [45], agents perform actions asynchronously. At each time step, only one agent executes an action while the others remain idle. Thus, agents’ actions are interleaved over time rather than occurring simultaneously. The global state transitions are based solely on the action of the single active agent at that time step. The system’s evolution results from individual agents acting one after another in some order. The system represents all possible sequences (interleavings) of agent actions. The order in which agents act may be non-deterministic unless specified by some scheduling policy. Agents act independently without the assumption that others are acting simultaneously. Agents do not need to consider concurrent actions by others at the same time step.

In a Network of Automata [10], multiple automata (representing agents or system components) operate concurrently. Synchronisation is achieved through explicit mechanisms, such as synchronisation labels, channels, or shared actions. Automata can perform actions independently or synchronously with other automata, depending on the synchronisation requirements. Synchronisation can be partial (involving only some automata) or full (involving all automata).

3.2. TIS Formalism

We begin by establishing some notation that will be used throughout the paper. Let ${\mathbb{R}}_{+}$ denote the set of positive real numbers, $\mathbb{N}$ denote the set of natural numbers, and $\mathbb{X}$ denote a finite set of variables known as clocks. Each clock is a variable that ranges over the set of non-negative real numbers. For a clock $x\in \mathbb{X}$ and a constant $c\in \mathbb{N}$, we define the set of clock constraints over $\mathbb{X}$, denoted by $\mathcal{C}\left(\mathbb{X}\right)$. These constraints, $\mathfrak{cc}$, are conjunctions of comparisons between a clock and a time constant c taken from the set of natural numbers, $\mathbb{N}$. Next, we recall the TIS definition from [4]. Let $\mathcal{A}={\mathbf{i}}_1,\cdots ,{\mathbf{i}}_n$ represent a non-empty finite set of agents, and let $\mathcal{E}$ represent a special agent used to model the environment in which these agents operate. Additionally, let $\mathcal{AP}={\bigcup }_{\mathbf{i}\in \mathcal{A}\cup \mathcal{E}}{\mathcal{AP}}_{\mathbf{i}}$ be the set of propositional variables, where ${\mathcal{AP}}_{\mathbf{i}}\bigcap {\mathcal{AP}}_{\mathbf{j}}=\varnothing$ for all distinct agents $\mathbf{i},\mathbf{j}\in \mathcal{A}\cup \mathcal{E}$. The set of agents, $\mathcal{A}$, and the environment, $\mathcal{E}$, form a multi-agent system.

A timed interpreted system is defined as a tuple:

$$\mathrm{TIS}=({\{L_{\mathbf{i}},Ac{t}_{\mathbf{i}},{\mathbb{X}}_{\mathbf{i}},P_{\mathbf{i}},{\mathcal{V}}_{\mathbf{i}},{\iota }_{\mathbf{i}}\}}_{\mathbf{i}\in \mathcal{A}\cup \{\mathcal{E}\}},{\{t_{\mathbf{i}}\}}_{\mathbf{i}\in \mathcal{A}},\{t_{\mathcal{E}}\}),$$

where $L_{\mathbf{i}}$ is a non-empty set of locations for an agent $\mathbf{i}$, and ${\iota }_{\mathbf{i}}\subseteq L_{\mathbf{i}}$ is a non-empty set of initial locations. The set $Ac{t}_{\mathbf{i}}$ represents the possible actions that the agent $\mathbf{i}$ can perform. Each agent has a special action, referred to as the ‘null’ or ‘silent’ action, denoted as ${ϵ}_{\mathbf{i}}$, which belongs to $Ac{t}_{\mathbf{i}}$, and similarly, ${ϵ}_{\mathcal{E}}$ belongs to $Ac{t}_{\mathcal{E}}$.

The set ${\mathbb{X}}_{\mathbf{i}}$ denotes a non-empty set of clocks, ensuring that ${\mathbb{X}}_{\mathbf{i}}\cap {\mathbb{X}}_{\mathbf{j}}=\varnothing$ for all distinct agents $\mathbf{i},\mathbf{j}\in \mathcal{A}\cup \mathcal{E}$. The function $P_{\mathbf{i}}:L_{\mathbf{i}}\to 2^{Ac{t}_{\mathbf{i}}}$ is a protocol function that models the program executed by the agent $\mathbf{i}$. Formally, for any agent $\mathbf{i}\in \mathcal{A}\cup \mathcal{E}$, the actions are determined according to this local protocol.

A valuation function ${\mathcal{V}}_{\mathbf{i}}:L_{\mathbf{i}}\to 2^{{\mathcal{AP}}_{\mathbf{i}}}$ assigns to each location a set of atomic formulae that are considered true at that location. The set $Act={Act}_1\times \dots \times {\mathrm{Act}}_n\times {Act}_{\mathcal{E}}$ represents the collection of joint actions performed by all agents.

The evolution function specifies how local states ‘evolve’ based on several factors: the local state of the agent, the actions of other agents, the local state of a special agent representing the environment, the clock constraints of the agent $\mathbf{i}$, and the set of clocks to reset. A function $t_{\mathbf{i}}:L_{\mathbf{i}}\times L_{\mathcal{E}}\times \mathcal{C}\left({\mathbb{X}}_{\mathbf{i}}\right)\times 2^{{\mathbb{X}}_{\mathbf{i}}}\times Act\to L_{\mathbf{i}}$ is a (partial) evolution function for agents, while a function $t_{\mathcal{E}}:L_{\mathcal{E}}\times \mathcal{C}\left({\mathbb{X}}_{\mathcal{E}}\right)\times 2^{{\mathbb{X}}_{\mathcal{E}}}\times Act\to L_{\mathcal{E}}$ is a (partial) evolution function for the environment.

We assume that the environment’s locations, actions, and clocks are ‘public’, while the locations and clocks of any agent are considered ‘private’. We further assume that if ${ϵ}_{\mathbf{i}}\in P_{\mathbf{i}}\left({\ell }_{\mathbf{i}}\right)$, then $t_{\mathbf{i}}({\ell }_{\mathbf{i}},{\ell }_{\mathcal{E}},{\mathfrak{cc}}_{\mathbf{i}},\mathbb{X},(a_1,\dots ,a_n,a_{\mathcal{E}}))={\ell }_{\mathbf{i}}$ for $a_{\mathbf{i}}={ϵ}_{\mathbf{i}}$, any ${\mathfrak{cc}}_{\mathbf{i}}\in \mathcal{C}\left(\mathbb{X}\right)$, and any $\mathbb{X}\in 2^{{\mathbb{X}}_{\mathbf{i}}}$.

Each element t of $t_{\mathbf{i}}$ is represented by a tuple $<{\ell }_{\mathbf{i}},{\ell }_{\mathcal{E}},{\mathfrak{cc}}_{\mathbf{i}},{\mathbb{X}}^{\prime },a,{\ell }_{\mathbf{i}}^{\prime }>$, where ${\ell }_{\mathbf{i}}$ denotes the source location, ${\ell }_{\mathbf{i}}^{\prime }$ represents the target location, a is the action, $\mathfrak{cc}$ is the enabling condition for $t_{\mathbf{i}}$, and ${\mathbb{X}}^{\prime }\subseteq \mathbb{X}$ is the set of clocks reset when performing t. The guard $\mathfrak{cc}$ must be satisfied to enable the transition.

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:

α₁

$A\to B:{\langle T_A·i\left(A\right)\rangle }_{K_B},$

α₂

$B\to A:{\langle T_A·T_B\rangle }_{K_A},$

α₃

$A\to B:{\langle T_B\rangle }_{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\left(A\right)$. 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 Gavin Lowe discovered an attack [47] that involved two interlaced executions of the protocol.

${\alpha }_1^1$

$A\to I:{\langle T_A·i\left(A\right)\rangle }_{K_I},$

${\alpha }_1^2$

$I\left(A\right)\to B:{\langle T_A·i\left(A\right)\rangle }_{K_B},$

${\alpha }_2^2$

$B\to I\left(A\right):{\langle T_A·T_B\rangle }_{K_A},$

${\alpha }_2^1$

$I\to A:{\langle T_A·T_B\rangle }_{K_A},$

${\alpha }_3^1$

$A\to I:{\langle T_B\rangle }_{K_I},$

${\alpha }_3^2$

$I\left(A\right)\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. The hypothetical executions of the protocols specified in the ProToc language can be generated as composite substitutions of the abstract protocol within a defined finite space and structure, reflecting the actual operation of the network. For our experiments, we consider a space comprising two honest users, an Intruder, one key (or one pair of keys), and a one-time ticket per user. These hypothetical substitutions can be generated automatically using combinatorial techniques. By incorporating the Intruder in this manner, we can compute such executions as:

• $A\to B$,
• $A\to I$ (Intruder as an ordinary user),
• $A\to I\left(B\right)$ (Intruder impersonating B),
• $B\to A$,
• $B\to I$,
• $B\to I\left(A\right)$ (Intruder impersonating A),
• $I\to A$,
• $I\to B$,
• $I\left(A\right)\to B$,
• $I\left(B\right)\to A$,

and several others of a similar nature. The executions mentioned above are translated into a product of synchronised automata. Given that we know in which execution the Intruder impersonates an honest user, our goal is to determine whether the final step of one of these executions can be performed in our experiments. To achieve this, we check the reachability of undesired states within our automata network. Our analysis is based on the Dolev–Yao model of the Intruder. This concept is illustrated in the following example.

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 ${\mathbb{A}}_{T_A}^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, $Ac{t}_{\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 $\left\{x_0\right\}$. 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.

We assume the following local evolution functions for the environment:

• $t_{\mathcal{E}}(l{\mathcal{E}}_0,x_0>D_1,\varnothing ,{\alpha }_1)=l{\mathcal{E}}_1,$
• $t_{\mathcal{E}}(\mathcal{Z},\varnothing ,\{x_0,x_{T_A}\},{\alpha }_1)=\mathcal{Z}$,
• $t_{\mathcal{E}}(l{\mathcal{E}}_1,x_0>D_2,\varnothing ,{\alpha }_2)=l{\mathcal{E}}_2,$
• $t_{\mathcal{E}}(\mathcal{Z},\varnothing ,\{x_0,x_{T_B}\},{\alpha }_2)=\mathcal{Z}$,
• $t_{\mathcal{E}}(l{\mathcal{E}}_2,x_0>D_3,\varnothing ,{\alpha }_3)=l{\mathcal{E}}_3,$
• $t_{\mathcal{E}}(\mathcal{Z},\varnothing ,\left\{x_0\right\},{\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,\varnothing ,{\alpha }_1)=l_1$,
• $t_A(l_1,l{\mathcal{E}}_1,x_{T_A}<L_{T_A},\varnothing ,{\alpha }_2)=l_1,$
• $t_B(l_0,l{\mathcal{E}}_0,x_{T_A}<L_{T_A},\varnothing ,{\alpha }_1)=l_1$,
• $t_B(l_1,l{\mathcal{E}}_1,x_{T_A}<L_{T_A},\varnothing ,{\alpha }_2)=l_1$,
• $t_A(l_0,l{\mathcal{E}}_1,x_{T_B}<L_{T_B},\varnothing ,{\alpha }_2)=l_1$,
• $t_A(l_1,l{\mathcal{E}}_2,x_{T_B}<L_{T_B},\varnothing ,{\alpha }_3)=l_1$,
• $t_B(l_0,l{\mathcal{E}}_1,true,\varnothing ,{\alpha }_2)=l_1$,
• $t_B(l_1,l{\mathcal{E}}_2,x_{T_B}<L_{T_B},\varnothing ,{\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.

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^2,l{\mathcal{E}}_3^2,\mathcal{Z}$, actions $Ac{t}_{\mathcal{E}}=\{{\alpha }_1^1,{\alpha }_2^1,{\overline{\alpha }}_2^1,{\alpha }_3^1,{\alpha }_1^2,{\overline{\alpha }}_1^2,$ ${\alpha }_2^2,{\alpha }_3^2,{\overline{\alpha }}_3^2\}$, and a set of clocks ${\mathbb{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·T_B\rangle }_{K_A}}^I$).

The automata ${\mathbb{A}}_{{\langle T_B\rangle }_{K_B}}^I$ and ${\mathbb{A}}_{{\langle T_A·i\left(A\right)\rangle }_{K_B}}^I$, 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_{\mathcal{E}}(l{\mathcal{E}}_0^1,x_0>D_1,\varnothing ,{\alpha }_1^1)=l{\mathcal{E}}_1^1$,
• $t_{\mathcal{E}}(l{\mathcal{E}}_1^1,x_0>D_2,\varnothing ,{\alpha }_2^1)=l{\mathcal{E}}_2^1$,
• $t_{\mathcal{E}}(l{\mathcal{E}}_1^1,x_0>D_2,\varnothing ,{\overline{\alpha }}_2^1)=l{\mathcal{E}}_2^1$,
• $t_{\mathcal{E}}(l{\mathcal{E}}_2^1,x_0>D_3,\varnothing ,{\alpha }_3^1)=l{\mathcal{E}}_3^1$;

• the second execution:

• $t_{\mathcal{E}}(l{\mathcal{E}}_0^2,x_0>D_4,\varnothing ,{\alpha }_1^2)=l{\mathcal{E}}_1^2$,
• $t_{\mathcal{E}}(l{\mathcal{E}}_0^2,x_0>D_4,\varnothing ,{\overline{\alpha }}_1^2)=l{\mathcal{E}}_1^2$,
• $t_{\mathcal{E}}(l{\mathcal{E}}_1^2,x_0>D_5,\varnothing ,{\alpha }_2^2)=l{\mathcal{E}}_2^2$,
• $t_{\mathcal{E}}(l{\mathcal{E}}_2^2,x_0>D_6,\varnothing ,{\alpha }_3^2)=l{\mathcal{E}}_3^2$,
• $t_{\mathcal{E}}(l{\mathcal{E}}_2^2,x_0>D_6,\varnothing ,{\overline{\alpha }}_3^2)=l{\mathcal{E}}_3^2$;

• and the resetting automaton:

• $t_{\mathcal{E}}(\mathcal{Z},\varnothing ,\{x_0,x_{T_A}\},{\alpha }_1^1)=\mathcal{Z},$
• $t_{\mathcal{E}}(\mathcal{Z},\varnothing ,\left\{x_0\right\},{\alpha }_2^1)=\mathcal{Z},$
• $t_{\mathcal{E}}(\mathcal{Z},\varnothing ,\left\{x_0\right\},{\alpha }_3^1)=\mathcal{Z},$
• $t_{\mathcal{E}}(\mathcal{Z},\varnothing ,\left\{x_0\right\},{\alpha }_1^2)=\mathcal{Z},$
• $t_{\mathcal{E}}(\mathcal{Z},\varnothing ,\{x_0,x_{T_B}\},{\alpha }_2^2)=\mathcal{Z},$
• $t_{\mathcal{E}}(\mathcal{Z},\varnothing ,\left\{x_0\right\},{\alpha }_3^2)=\mathcal{Z}$.

• For the agents, we define the local evolution functions for the $T_A$:

• $t_A(l_0,l{\mathcal{E}}_0^1,true,\varnothing ,{\alpha }_1^1)=l_1$,
• $t_A(l_1,l{\mathcal{E}}_1^1,x_{T_A}<L_{T_A},\varnothing ,{\alpha }_2^1)=l_1$,
• $t_B(l_0,l{\mathcal{E}}_0^2,x_{T_A}<L_{T_A},\varnothing ,{\alpha }_1^2)=l_1,$
• $t_B(l_1,l{\mathcal{E}}_1^2,x_{T_A}<L_{T_A},\varnothing ,{\alpha }_2^2)=l_1$,
• $t_I(l_0,l{\mathcal{E}}_0^1,true,\varnothing ,{\alpha }_1^1)=l_1$,
• $t_I(l_1,l{\mathcal{E}}_0^2,x_{T_A}<L_{T_A},\varnothing ,{\alpha }_1^2)=l_1$;

• and for the ticket $T_B$:

• $t_A(l_0,l{\mathcal{E}}_1^1,x_{T_B}<L_{T_B},\varnothing ,{\alpha }_2^1)=l_1,$
• $t_A(l_1,l{\mathcal{E}}_2^1,x_{T_B}<L_{T_B},\varnothing ,{\alpha }_3^1)=l_1$,
• $t_B(l_0,l{\mathcal{E}}_1^2,true,\varnothing ,{\alpha }_2^2)=l_1,$
• $t_B(l_1,l{\mathcal{E}}_2^2,x_{T_B}<L_{T_B},\varnothing ,{\alpha }_3^2)=l_1$,
• $t_I(l_0,l{\mathcal{E}}_2^1,true,\varnothing ,{\alpha }_3^1)=l_1,$
• $t_I(l_1,l{\mathcal{E}}_2^2,x_{T_B}<L_{T_B},\varnothing ,{\alpha }_3^2)=l_1$.

• The intruder-specific automaton for a complete message ${\langle T_A·T_B\rangle }_{K_A}$ can be described by the following functions:

• $t_I(l_0,l{\mathcal{E}}_1^2,true,\varnothing ,{\alpha }_2^2)=l_1$,
• $t_I(l_1,l{\mathcal{E}}_1^1,true,\varnothing ,{\alpha }_2^1)=l_1$;

• and all the blocking automata:

• $t_I(l_1,l{\mathcal{E}}_1^1,true,\varnothing ,{\overline{\alpha }}_2^1)=l_1$,
• $t_I(l_1,l{\mathcal{E}}_2^0,true,\varnothing ,{\overline{\alpha }}_1^2)=l_1,$
• $t_I(l_1,l{\mathcal{E}}_2^2,true,\varnothing ,{\overline{\alpha }}_3^2)=l_1.$

The timed model induced by the above description of both NSPKT scenarios, as outlined in Section 5.1, should be straightforward to infer.

5. Reachability Checking

Timed Interpreted Systems provide computationally grounded semantics that enable the interpretation of time-bounded temporal modalities.

The transition system [48] that models the behaviour of TISs, referred to as the timed model, consists of two types of transitions. The first type is action transitions, which are labelled with timeless joint actions representing the discrete evolutions of TIS. The second type is time transitions, labelled with non-negative real numbers corresponding to the passage of time. Due to the infinite nature of time, there are infinitely many possible time transitions.

Let us recall the necessary notations adopted from the theory of Timed Automata. A clock valuation v of $\mathbb{X}$ is a total function mapping $\mathbb{X}$ to the set of non-negative real numbers. The set of all clock valuations is denoted by ${\mathbb{R}}_{+}^{\mid \mathbb{X}\mid }$. For a subset ${\mathbb{X}}^{\prime }\subseteq \mathbb{X}$, the valuation that assigns the value 0 to all clocks in ${\mathbb{X}}^{\prime }$ is defined as follows: ${\forall }_{x\in {\mathbb{X}}^{\prime }}{v}^{\prime }\left(x\right)=0$ and ${\forall }_{x\in \mathbb{X}\setminus {\mathbb{X}}^{\prime }}{v}^{\prime }\left(x\right)=v\left(x\right)$, and is denoted by $[{\mathbb{X}}^{\prime }:=0]$. For $v\in {\mathbb{R}}_{+}^{\mid \mathbb{X}\mid }$ and $\delta \in {\mathbb{R}}_{+}$, $v+\delta$ is the clock valuation of $\mathbb{X}$ that assigns the value $v\left(x\right)+\delta$ to each clock x. A valuation v satisfies a clock constraint $\mathfrak{cc}$, denoted as $v\vDash \mathfrak{cc}$ if $\mathfrak{cc}$ evaluates to true using the clock values provided by the valuation v.

5.1. Timed Model

For a given TIS, let the symbol $S={\prod }_{\mathbf{i}\in \mathcal{A}\cup \mathcal{E}}(L_{\mathbf{i}}\times {\mathbb{R}}_{+}^{\mid {\mathbb{X}}_{\mathbf{i}}\mid })$ denote the non-empty set of all the global states. Furthermore, for a specific global state $s=(({\ell }_1,v_1),\dots ,({\ell }_n,v_n),({\ell }_{\mathcal{E}},v_{\mathcal{E}}))\in S$, let the symbols $l_{\mathbf{i}}\left(s\right)={\ell }_{\mathbf{i}}$ and $v_{\mathbf{i}}\left(s\right)=v_{\mathbf{i}}$ represent, respectively, the local component and the clock valuation of the agent $\mathbf{i}\in \mathcal{A}\cup \mathcal{E}$ in the global state s.

We define a timed model (or simply a model) for a given TIS as a tuple $\mathcal{M}=(Act,S,\iota ,T,\mathcal{V})$, where: $\iota ={\prod }_{\mathbf{i}\in \mathcal{A}\cup \mathcal{E}}({\iota }_i\times 0^{\mid {\mathbb{X}}_i\mid })$ is the set of all initial global states; $\mathcal{V}\left(s\right)={\bigcup }_{\mathbf{i}\in \mathcal{A}\cup \mathcal{E}}{\mathcal{V}}_{\mathbf{i}}\left(l_{\mathbf{i}}\left(s\right)\right)$; $T\subseteq S\times (Act\cup {\mathbb{R}}_{+})\times S$ is a transition relation defined by action and time transitions. This relation is crucial in understanding how the system evolves, as it captures the possible transitions from one global state to another based on actions and time.

For an action $\tilde{a}\in Act$, an action transition $(s,\tilde{a},s^{\prime })\in T$ (denoted as $s\stackrel{\tilde{a}}{⟶}{s}^{\prime }$) holds if, for all $\mathbf{i}\in \mathcal{A}\cup \mathcal{E}$, there exists a local transition $t_{\mathbf{i}}(l_{\mathbf{i}}\left(s\right),l_{\mathcal{E}}\left(s\right),{\mathfrak{cc}}_{\mathbf{i}},{\mathbb{X}}^{\prime },\tilde{a})=l_{\mathbf{i}}\left(s^{\prime }\right)$ such that $v_{\mathbf{i}}\left(s\right)\vDash {\mathfrak{cc}}_{\mathbf{i}}$ and $v_{\mathbf{i}}^{\prime }\left(s^{\prime }\right)=v_{\mathbf{i}}\left(s\right)[{\mathbb{X}}^{\prime }:=0]$. Additionally, there must exist a local transition $t_{\mathcal{E}}(l_{\mathcal{E}}\left(s\right),{\mathfrak{cc}}_{\mathcal{E}},{\mathbb{X}}^{\prime },\tilde{a})=l_{\mathcal{E}}\left(s^{\prime }\right)$ such that $v_{\mathcal{E}}\left(s\right)\vDash {\mathfrak{cc}}_{\mathcal{E}}$ and $v_{\mathcal{E}}^{\prime }\left(s^{\prime }\right)=v_{\mathcal{E}}\left(s\right)[{\mathbb{X}}^{\prime }:=0]$. A time transition $(s,\delta ,s^{\prime })\in T$ holds if, for all $\mathbf{i}\in \mathcal{A}\cup \mathcal{E}$, we have $l_{\mathbf{i}}\left(s\right)=l_{\mathbf{i}}\left(s^{\prime }\right)$ and $v_{\mathbf{i}}^{\prime }\left(s^{\prime }\right)=v_{\mathbf{i}}\left(s\right)+\delta$, where $\delta \in {\mathbb{R}}_{+}$.

An infinite path $\pi$ in $\mathcal{M}$ is defined as a sequence $\pi =(s_0,s_1,\dots )$ of states such that $s_0$ is an initial state, and for each even $i\ge 0$, there exists $\delta \in {\mathbb{R}}_{+}$ such that $(s_i,\delta ,s_{i+1})\in T$. For each odd $i>0$, there exists a joint action $\tilde{a}$ such that $(s_i,\tilde{a},s_{i+1})\in T$.

Note that the above definition of a path ensures that the first transition is a time transition. Each action transition is followed by a time transition, and each time transition is followed by an action transition. Semantics in which every action transition is preceded by a time transition with $\delta >0$ is strongly monotonic. Strongly monotonic semantics require that no two events occur at the same time.

The transition system (timed model) $\mathcal{M}$ of a timed interpreted system typically has infinitely many states and infinitely many labels. However, the reachability problem for $\mathcal{M}$ can be reduced to a reachability problem for a transition system with finitely many states and finitely many labels.

Let $c_{max}$ be the largest constant c such that some clock x is compared with c in some constraint appearing in a guard of TIS. By $\widehat{\mathcal{M}}$, we denote the transition system for a timed interpreted system that differs from $\mathcal{M}$ only in its set of labels: for the set of labels of $\widehat{\mathcal{M}}$, we take the set $\mathcal{V}\cup [0,c_{max}+1]$.

The region equivalence (the equivalence relation ≃) is defined over the set of all clock valuations for $\mathbb{X}$. For two clock valuations v and $v^{\prime }$ in ${\mathbb{R}}^{\mid \mathbf{X}\mid }$, we say that $v\simeq v^{\prime }$ if, for each $0⩽j<n$, where n is the number of clocks, either $v\left(x_j\right)>c^{max}j$ and $v^{\prime }\left(x_j\right)>c^{max}j$, or $v\left(x_j\right)⩽c^{max}j$ and $v^{\prime }\left(x_j\right)⩽c^{max}j$ and $v\left(x_j\right)=v^{\prime }\left(x_j\right)$.

It is well-known that the relation ≃ is an equivalence relation, allowing for constructing a finite abstract model.

5.2. Reachability Analysis

The reachability problem for multi-agent systems modelled by Timed Interpreted Systems involves determining whether, for a specified set of target locations, a state containing a target location can be reached from some initial state. We assume that a propositional formula representing a particular property describes the set of target locations. To verify the reachability of a state that satisfies this property using the Bounded Model Checking method, the model’s transition relation is initially unfolded iteratively to a certain depth k and encoded as a quantifier-free first-order formula of state variables. Subsequently, the property is converted into a quantifier-free first-order formula of state variables, and an SMT-solver is used to check the satisfiability of the conjunction of these two formulae.

If the conjunction (denoted in the algorithm by ${\beta }_k$) is satisfiable, it can be concluded that a path to a target location has been found. If not, the value of k is incremented by 2, as time transitions do not alter the global locations (Algorithm 1). The parameter n, which represents the number of steps in a given protocol, is crucial in determining the depth of the model’s transition relation that needs to be unfolded.

Algorithm 1 The standard bounded model checking algorithm for testing reachability

1: procedure REACHABILITY 2:     $k:=0$ 3:     loop 4:         $result:=checkSAT\left({\beta }_k\right)$ 5:         if $result$ = $SATISFIABLE$ then 6:            return $REACHABLE$ 7:         else if $result$ = $UNKNOWN$ then 8:            return $UNKNOWN$ 9:         end if 10:         $k:=k+2$ 11:         if $k>4·n$ then 12:            return $UNREACHABLE$ 13:         end if 14:     end loop 15: end procedure

The SMT encoding of the reachability problem for TIS builds upon the encoding described in [49]. However, we have:

• refined the definitions for the encoding of the transition relation (as the definition in the cited paper lacked precision), and 
• incorporated real-time aspects of multi-agent systems, whereas the previous SMT encoding was limited to discrete time.

Let $\widehat{\mathcal{M}}$ be a model. To formulate and solve the reachability problem for TISs, we must define the unfolding of the transition relation up to depth $k\in \mathbb{N}$. To this end, we define a k-path as a finite prefix of a path. Note that an arbitrary state s is reachable in $\widehat{\mathcal{M}}$ if and only if it is reachable on a k-path for some $k\ge 0$.

Next, we define the formula $pat{h}_k({\overline{\mathbf{w}}}_0,\dots ,{\overline{\mathbf{w}}}_k)$, which symbolically encodes all the k-paths starting at the initial state of $\widehat{\mathcal{M}}$. The definition of the formula $pat{h}_k({\overline{\mathbf{w}}}_0,\dots ,{\overline{\mathbf{w}}}_k)$ assumes that each global state $s\in S$ of $\widehat{\mathcal{M}}$ can be represented by a valuation of a symbolic state $\overline{\mathbf{w}}=((w1,v_1),\dots ,(w_n,v_n),(w_{\mathcal{E}},v_{\mathcal{E}}))$ that consists of symbolic local states. Each symbolic local state is a pair $(w_{\mathbf{i}},v_{\mathbf{i}})$ of individual variables ranging over the natural numbers, which represent the local state of the agent $\mathbf{i}$ and a clock valuation. Similarly, each action can be represented by a valuation of a symbolic joint action $\overline{\mathbf{a}}$, which is a vector of individual variables ranging over natural numbers.

Let $\overline{\mathbf{w}}$ and ${\overline{\mathbf{w}}}^{\prime }$ be two symbolic states, $\overline{\mathbf{a}}$ a symbolic action, and $\mathbf{d}$ a symbolic non-negative real number. We define the following quantifier-free first-order formulae:

• $I_s\left(\overline{\mathbf{w}}\right)$ encodes the state s of the model $\widehat{\mathcal{M}}$,
• ${\mathcal{T}}_{\sigma }(w_{\mathbf{i}},\overline{\mathbf{a}},{w^{\prime }}_{\mathbf{i}})$ encodes an action transition and ensures that every local action $a_i$ in $\overline{\mathbf{a}}$ is performed by each agent in which this action appears,
• ${\mathcal{T}}_{\tau }(w_{\mathbf{i}},\mathbf{d},{w^{\prime }}_{\mathbf{i}})$ encodes a time transition in $\widehat{\mathcal{M}}$.

For every even $k\in \mathcal{N}$, we can now define the formula $pat{h}_k({\overline{\mathbf{w}}}_0,\dots ,{\overline{\mathbf{w}}}_k)$ as follows:

$$\begin{array}{c}\underset{s\in \iota }{\bigvee }{I}_s\left({\overline{\mathbf{w}}}_0\right)\wedge \underset{\begin{array}{c}j=0\\ jmod2=0\end{array}}{\overset{k-2}{\bigwedge }}\left({\mathcal{T}}_{\tau }\left({\overline{\mathbf{w}}}_j,\mathbf{d},{\overline{\mathbf{w}}}_{j+1}\right)\wedge {\mathcal{T}}_{\sigma }\left({\overline{\mathbf{w}}}_{j+1},{\overline{\mathbf{a}}}_j,{\overline{\mathbf{w}}}_{j+2}\right)\right).\end{array}$$

Using the above formula and a quantifier-free first-order formula $reach\left(\overline{\mathbf{w}}\right)$, which encodes the set of states that satisfy a given property, we aim to determine whether any state satisfying $reach\left(\overline{\mathbf{w}}\right)$ is reachable. It is achieved by verifying the satisfiability of the following formula:

$${\psi }_k=pat{h}_k({\overline{\mathbf{w}}}_0,\dots ,{\overline{\mathbf{w}}}_k)\wedge {\bigvee }_{j=0}^{k}reach\left({\overline{\mathbf{w}}}_j\right).$$

The method described relies on the following theorem.

Theorem 1.

Let $\widehat{\mathcal{M}}$ be a model and s a state. Then, for every $k\in \mathbb{N}$, the state s is reachable in $\widehat{\mathcal{M}}$ via a path of length k if and only if the formula ${\psi }_k$ is satisfiable.

The proof by induction on k is straightforward.

We terminate the unfolding of the transition relation if either the formula ${\psi }_k$ is satisfiable or if the SMT-solver cannot determine the satisfiability of the formula in question. Alternatively, termination could occur if the value of k equals the reachability diameter of the system–the minimum number of steps required to reach all reachable states. However, the reachability diameter cannot be calculated for many systems, and the available estimates often need more precise. This limitation results in BMC needing to be completed in practice.

6. Experimental Results

In this section, we present the experimental results and the implementation details.

6.1. Implementation

We provide a complete end-to-end implementation (the implementation [26], along with instructions for installing the necessary software and the specifications of the tested protocols, can be found on GitHub (https://github.com/amz-research-veri/VerSecTis, accessed on 3 November 2024)). All the protocols are specified using the ProToc language.

The first step of the method involves translating the executions of the TSP into TIS. The second step entails converting this model into a BMC problem and generating a file that encodes the transition relation as an SMT problem. The final step is to perform satisfiability checking using an SMT solver. Our SMT-based BMC reachability algorithm is implemented as a standalone program written in C++ (standard ISO/IEC 14882:2020). For this purpose, we utilised the state-of-the-art SMT solver Z3 [50] (version 8.4.5).

6.2. SMT-Solvers

Given a quantifier-free first-order formula with variables defined in Section 5, the objective is to find an assignment for the variables that makes the formula satisfiable. Solving the SMT problem becomes particularly useful when restricted to specific logical theories where existing tools, known as SMT solvers, are employed to find solutions. The most notable solvers include Z3 [50], Yices2 [51], and CVC4 [52].

For a given input, which is a conjunction of two quantifier-free first-order formulae, it is denoted as $\phi$, the SMT solver has three possible outcomes: sat: when the input $\phi$ is satisfiable; unsat: when the input $\phi$ is not satisfiable; unknown: when it is indeterminate whether $\phi$ is sat or unsat, as this determination exceeds the capabilities of the decision procedures.

Our choice for the Z3 SMT solver is motivated by several reasons. Z3 is used on an industrial scale; many experimental results for different systems, including MAS and timed automata, show that for reachability checking, Z3 gives the best results [34]. Z3 can also be trusted: when it answers sat, then it produces a witness (an assignment of variables) that makes the formula satisfiable; when it answers unsat, it produces proof that the formula is not satisfiable.

6.3. Performance Evaluation

Unfortunately, we could not compare our results with other approaches, as the executions of our TSP model are richer, capturing more time dependencies than the timed models mentioned in Section 2. An honest comparison with the existing approaches would not be possible. First, the synchronisation in the network of timed automata and the interpreted systems is entirely different (Section 3.1). The possible comparison is to compare the modelling of protocol execution by a network of timed automata and interleaved interpreted systems.

Our experiments were meticulously conducted on a high-performance computer featuring an I7-5500U processor (Intel Corporation, Santa Clara, CA, USA), 12 GB of RAM, and a Linux operating system running kernel 5.2.9. This robust setup ensured the reliability and accuracy of our results.

In our experiments, we examined the standard authentication and secrecy properties of TSP. In addition, we also detected and prevented situations where a passive intruder participates in the protocol execution by positioning themselves between the users and merely relaying all transmitted data. This scenario represents a Man-in-the-Middle (MitM) attack [53]. Although the intruder may not gain access to secret data or compromise the authentication process, the mere presence of the intruder in the network is undesirable. Such situations can be detected and prevented by selecting appropriate lifetime values.

We will discuss the experimental results and draw our conclusions based on nine timed versions of protocols well-known from the literature. We tested the following: the Needham–Schroeder Public Key Protocol [46] and Lowe’s modification of NSPKT (NSPKT_L) [1]; the Denning-Sacco Protocol (DS) [54]; the Woo-Lam Pi Protocol (WLP) [34,55]; other versions of the Woo-Lam Pi protocol, WLP 1 and 3 [55]; the Andrew Protocol (AP) [56]; Lowe’s modification of the Andrew Protocol (A_LP) [57]; and MobInfoSec (MIS) [58].

Table 1. Short characteristics of security protocols and their advantages and disadvantages.

Protocol	Advantages	Disadvantages
NSPKT [46]	- Foundational in cryptographic communication - Mutual authentication via public-key cryptography	- Vulnerable to man-in-the-middle attack
NSPKTL [1]	- Addresses NSPKT vulnerability - Enhanced security with minimal structural change	- Increased complexity - Higher computational requirements
DS [54]	- Reduced reliance on timestamps - Key confirmation for increased trust	- Relies on uncompromised third parties - Susceptible to session hijacking
WLP [34,55]	- Simplified message authentication - Mutual authentication without complex cryptographic functions	- Potential replay attacks - Assumes session key confidentiality
WLP 1 & 3 [55]	- Security tailored for different applications - Mitigates replay attack vulnerabilities	- Increased complexity - May require further modifications
AP [56]	- Efficient for lightweight environments - Nonce-based verification	- Replay attacks possible without checks - Not robust for high-security scenarios
ALP [57]	- Improved security addressing AP vulnerabilities - Enhanced replay attack protection	- Increased computational cost - More complex than original AP
MIS [58]	- Designed for mobile information security - Scalable and flexible for modern needs	- High resource consumption - Limited compatibility with older devices

presents short security protocols’ characteristics, advantages, and disadvantages.

6.3.1. Andrew Protocol

To present the experimental results, we assume the delay values: $D_1=2$, $D_2=3$, $D_3=4$, and $D_4=5$. For the Andrew protocol (Figure 3), we conducted a comprehensive analysis and identified two paths indicative of Man-in-the-Middle behaviour (though not a complete attack). In these paths, locations 74 or 94 were found to be reachable. Additionally, we observed two paths that correspond to honest executions (paths where location 4 or 9 was reachable) and eight paths representing executions involving the Intruder (paths where locations 14, 24, 34, 44, 54, 64, 84, or 104 were reachable). The term executions with the Intruder encompasses two scenarios: firstly, executions in which the Intruder behaves as a legitimate user (paths where one of the locations 14, 54, 64, or 104 is reachable); and secondly, executions in which the Intruder unsuccessfully attempts to impersonate honest users (paths where one of the locations 24, 34, 44, or 84 is reachable).

It was found that the minimum lifetime values for the assumed delay values that ensure only honest executions occur (i.e., values that prevent Man-in-the-Middle behaviour) are $L_1=L_2=14$. The minimum values that permit Man-in-the-Middle behaviour to manifest at locations 74 and 94 are $L_1=L_2=21$.

6.3.2. Lowe’s Modification of Andrew Protocol

For Lowe’s modification of the Andrew Protocol (Figure 4), we assumed the following delay values: $D_1=2$, $D_2=3$, and $D_3=4$. With these delay settings, we identified two paths that indicate a Man-in-the-Middle behaviour (where locations 74 or 94 were reachable), two paths representing an honest execution (where locations 4 or 9 were reachable), and eight paths representing executions involving the Intruder (where locations 14, 24, 34, 44, 54, 64, 84, or 104 were reachable). The minimum lifetime values required to permit only honest executions are $L_1=L_2=7$. The minimum values required to enable a Man-in-the-Middle behaviour (reachability of locations 74 and 94) are $L_1=L_2=11$.

6.3.3. Denning–Sacco Protocol

In our analysis of the Denning–Sacco protocol (Figure 5), we assigned the following delay values: $D_1=2$, $D_2=3$, $D_3=4$, $D_4=5$. We found two paths that exhibit a Man-in-the-Middle behaviour, where locations 47 or 87 were reachable. Additionally, we discovered two paths representing an honest execution, with locations 3 or 7 being reachable, and two paths representing an execution involving the Intruder, with locations 43 or 83 being reachable. Our observations showed that for the Denning–Sacco protocol, under the assumed delays, the minimum value allowing both honest executions but not permitting a Man-in-the-Middle attack is $L_1=7$. Furthermore, we determined that the minimum value enabling a Man-in-the-Middle behaviour for the given delays (reachability of locations 47 and 87) is $L_1=8$.

6.3.4. Needham–Schroeder Public Key Protocol

Within the NSPKT protocol (Figure 6), we assigned the following delay values: $D_1=2$, $D_2=3$, $D_3=4$. Over the course of our analysis, we executed four scenarios, encompassing two instances of Intruder interventions, two Lowe’s attacks, and two instances of Man-in-the-Middle behaviour. It is important to note that, as outlined by the protocol structure, we were required to employ two distinct lifetime values, which play a crucial role in the protocol’s operation.

Lowe’s attacks were found to be possible at locations 23 or 55, while Man-in-the-Middle behaviour could manifest at locations 47 or 71. Honest executions were feasible at locations 3 or 7. Intruder interventions were observed at locations 11, 15, 27, 31, 39, 43, 59, or 63.

Our investigation revealed that for the NSPKT protocol and the stipulated delays, the minimum values of $L_1=L_2=9$ ensured honest executions without enabling the Man-in-the-Middle behaviour. To allow for the occurrence of the Man-in-the-Middle behaviour at locations 47 and 71, the minimum required values were $L_1=L_2=12$. These minimum values for honest executions and specific attacks are crucial for understanding the behaviour of the NSPKT protocol.

6.3.5. Lowe’s Modification of Needham–Schroeder Public Key Protocol

In the NSPKT protocol (Figure 7), we assigned the following delay values: $D_1=2$, $D_2=3$, $D_3=4$. During our analysis, we carried out four scenarios, including two Intruder interventions, two Lowe’s attacks, and two Man-in-the-Middle behaviour. It is important to note that as per the protocol structure, we had to use two distinct lifetime values, which are crucial for the protocol’s operation.

Lowe’s attacks were found to be possible at locations 23 or 55, while Man-in-the-Middle behaviour could occur at locations 47 or 71. Honest executions were feasible at locations 3 or 7. Intruder interventions were observed at locations 11, 15, 27, 31, 39, 43, 59, or 63.

Upon investigation, we found that for the NSPKT protocol and the given delays, the minimum values of $L_1=L_2=9$ ensured honest executions without enabling the Man-in-the-Middle behaviour. The minimum values that allow a Man-in-the-Middle behaviour (the locations 47 and 71 are reachable) are $L_1=L_2=12$. These minimum values for honest executions and specific attacks are crucial for understanding the behaviour of the NSPKT protocol.

6.3.6. Woo Lam Pi Protocol

We have established the following delay values for the WLP protocol (Figure 8): $D_1=2,D_2=3,D_3=4$. Our analysis revealed two paths indicating potential Man-in-the-Middle behaviour, with locations 71 or 131 being reachable. These two paths represent honest executions, with locations 5 or 11 being reachable, while ten other paths represent executions with an intruder, where locations 17, 29, 35, 41, 53, 77, 83, 89, 101 or 113 are reachable. For this protocol, the values $L_1=L_2=8$ are the minimum values allowing both honest executions. Furthermore, the minimum values that allow Man-in-the-Middle behaviour to appear (locations 71 and 131 are reachable) are $L_1=L_2=10$.

6.3.7. Woo Lam Pi 1, 2 and 3

For the WLP1 and WLP3 protocols (Figure 9), we assumed delay values as $D_1=2$, $D_2=3$, $D_3=4$. We found two paths indicating a Man-in-the-Middle behaviour (locations 53 or 113 are reachable). These two paths represent an honest execution (locations 5 or 11 are reachable), and six paths represent execution with the Intruder (locations 17, 29, 41, 77, 89, or 101 are reachable). For those protocols and the assumed delays, we observed that values $L_1=L_2=8$ are minimum values that allow us to perform honest executions and do not allow Man-in-the-Middle behaviour. However, it was impossible to find the lifetime values that allow performing the executions to represent MitM behaviour for the assumed delays, highlighting the challenges in network security. We present only a single chart as the differences in execution time and memory usage between WLP 1 and 2 are negligible (see

Table 2. Sample experimental results for the protocols with the attacks.

Protocol	BMC		SMT		Type of the Attack
	[s]	[MB]	[s]	[MB]
NSPKT	0.48	2.43	0.90	24.28	MitM
NSPKT	0.49	1.61	2.40	30.80	Lowe’s attack
NSPKTL	0.49	2.43	2.38	26.11	MitM
Denning-Sacco Protocol	0.28	2.57	0.40	23.38	MitM
Woo Lam Pi Protocol	0.40	2.54	0.70	29.11	MitM
Woo Lam Pi Protocol 1	0.54	2.61	1.26	32.54	MitM
Woo Lam Pi Protocol 3	0.54	2.61	1.44	32.19	MitM
Andrew Protocol	1.80	2.69	12.90	48.93	MitM 1
AndrewL Protocol	0.98	2.75	3.15	40.44	MitM
MobInfoSec	40.67	16.49	199.01	384.17	MitM

).

6.3.8. MobInfoSec Protocol

The MIS protocol has the following delay values: $D_1=2,D_2=3,D_3=4$. We have identified four paths that indicate a Man-in-the-Middle behaviour (locations 195, 1345, 1763, or 2463 are reachable), twenty-four paths representing an honest execution (locations from 1 to 24 are reachable), and 380 paths representing execution with the Intruder.

For this protocol, we have observed that values $L_1=L_2=L_3=11$ and $L_4=11$ are the only values that allow all the honest executions (these values do not allow a Man-in-the-Middle behaviour). The minimum values that allow a Man-in-the-Middle behaviour to appear (locations 1345, 1763, or 2463 are reachable) are $L_1=L_2=L_3=L_4=12$.

The minimum values that allow all Man-in-the-Middle behaviours to appear (locations 195, 1345, 1763, or 2463 are reachable) are $L_1=L_2=L_3=L_4=13$.

6.4. Conclusions on Performance Evaluation

Table 2 presents time consumption and memory usage for each attack, respectively, for BMC algorithm and satisfiability testing. The table does not include protocols free of considered types of attacks.

We have found the final results promising and would like to apply our approach further to validate more complex TSPs. Additionally, we aim to expand upon the algorithm presented in [34], which currently only considers a single lifetime value and does not account for system delays or the identification of time dependencies for when attacks occur. We plan to compare both approaches to assess their effectiveness.

The experiments presented above demonstrate the outstanding scalability of the method, which is most evident when analysing memory usage and runtime results for the MobInfoSec protocol, the most complex protocol tested in these experiments. The scalability and efficiency of our method result from the fact that, unlike other approaches to time-based system verification, we do not model the entire protocol. Instead, we focus on modelling the executions of security protocols. This approach reduces the model size, allowing for faster identification of states in which an intruder may attack the protocol. The computational complexity of BMC using SMT for temporal interpreted systems is exponential concerning the bound k. It depends on the complexity of the theories used in SMT.

It is known that the SMT problem is NP-hard since Boolean satisfiability is already NP-complete; moreover, the BMC-based verification process needs exponential time. However, the final stage of verification, which involves using an SMT solver, can often yield surprising results. Research indicates [59] that the choice of SMT solver also plays a significant role. It may be beneficial to experiment with various SMT solvers and select the one best suited to the specific problem, as the differences in runtime and memory usage can be substantial and depend on the solver’s heuristics.

7. Future Work

A noteworthy approach for future work would be to compare our modelling with the one presented in [24], which extends the formalism of the applied $\pi$-calculus [60] with parametric timed constraints. Using this formalism, the authors of [24] model security protocols along with an adversary and synthesise parameter valuations for which the system remains secure. Since the expressiveness of such modelling appears close to that of parametric timed automata [61,62], one might consider that modelling through timed interpreted systems would be appropriate here. However, our method is based on modelling the executions of security protocols using timed interpreted systems rather than the protocols themselves, which results in a smaller model and, consequently, faster verification.

The study [24] does not consider timed automata and timed interpreted systems. Still, the method employed has similarities to parameter synthesis for parametric timed automata, leading to the conclusion that it could also be applied to parametric timed interpreted systems. Here, it would be worth considering the definition of parametric timed interpreted systems and a method for translating the executions of security protocols into parametric timed interpreted systems. The verification process would be similar to that presented in [61].

8. Conclusions

This paper introduces Timed Interpreted Systems with dense time semantics to model the execution of Timed Security Protocols. Our TIS model captures shifts in user behaviour and knowledge throughout protocol execution, using time conditions to represent system delays and intervals between protocol steps. It adheres to constraints based on timestamps and lifetimes.

We have implemented bounded model checking for TIS, analysing the reachability properties of correctly specified model states. We evaluated nineteen security protocols using a highly effective SMT-based BMC algorithm, highlighting the approach’s robustness and efficiency. Encouraged by these preliminary results, we plan to extend this model to verify more complex protocols and properties in future research.