An Omniscience-Free Temporal Logic of Knowledge for Verifying Authentication Protocols

Abstract

Since the advent of BAN logic, many logics have been proposed for verifying authentication protocols. In one line of research, scholars have presented logics that can be utilized in verifying timed requirements of the protocols. Although many temporal epistemic logics have been developed to this end, there is no complete logic of this kind to prevent logical omniscience. Thus, they may lead to misleading judgments about the properties of the protocol being analyzed. In this paper, we propose a complete and omniscience-free temporal epistemic logic for analyzing authentication protocols. The main challenging issue in devising this logic is formulating intuitive models that on one hand reflect what is naturally meant by a protocol execution and on the other hand make it possible to achieve properties such as completeness. We show that such models can build on interpreted systems and that the resulting logic is useful in analyzing authentication protocols.

1 Introduction

Different deductive systems have been devised for the verification of authentication protocols. In particular, since the introduction of the modal logic BAN [9], many epistemic logics have been proposed for this purpose [2, 5, 6, 13, 14, 18, 22, 24, 33, 36, 37]. The rationale behind using such logics is that the knowledge of the agents involved in the protocol changes as messages are exchanged during the protocol execution. The sole modality of knowledge, however, is not enough for the analysis of protocols in which the order of actions taken by the principals may result in different beliefs, especially when there is an interaction between time and knowledge [4]. To attain an effective verification method for such protocols, a natural solution is to add a temporal dimension to a core epistemic logic. The need for proving properties of specific steps of an authentication protocol amplifies the necessity of temporal operators. This has been a research topic in the past two decades [4, 6,7,8, 10, 19, 25, 28, 29, 31, 32, 34].

At the same time, epistemic logics with standard Kripke semantics result in omniscience where agents know all logical truths [21]. Verifying authentication protocols using such logics may lead to wrong judgments. In actual fact, the logical omniscience bypasses the limitations placed on the knowledge of an agent who receives an encrypted message but does not have the correct key to extract the plain information from that message.

There are some attempts at resolving the problem of logical omniscience in the epistemic logics proposed for the specification and verification of cryptographic protocols. In [12], the problem is dealt within a logic where the authors modify the truth definition of the modal operator “knows”. They indeed make use of specific message renaming functions to evaluate statements in the worlds accessible from a given world. This logic, which is referred to as WS5 throughout this paper, does not have any temporal operators and can be thought of as a weakened S5, hence the name. The problem of omniscience has also been tackled in [6] where the authors suggest the goals of the protocol be translated into statements so that the bad effects of omniscience can be prevented. The presented logic, however, is not omniscience-free. The logical omniscience can also be defeated using exact models of the knowledge an agent may acquire during a protocol execution [20]. Another endeavor is the so-called temporal deductive logic [25] which is a sound and complete temporal epistemic logic. Although part of the logic linking every explicit knowledge to an awareness statement is omniscience-free, the problem remains in the part involving implicit knowledge.

Having said all this, there is no complete and omniscience-free temporal epistemic logic for the verification of authentication protocols. To attain such a logic, we extend WS5 with temporal operators. The result is called Temporal WS5, or TWS5 for short. The logic TWS5 allows knowledge and time operators to appear in each other’s scope. Thus, it is more powerful than logics in which temporal operators cannot be located in the scope of knowledge operators [31]. Moreover, similar to some other works, e.g., [19, 25, 32], TWS5 does not have any axiom connecting timed and epistemic statements. It is shown that TWS5 is useful in analyzing some authentication protocols that cannot be verified by similar logics.

The main challenging issue in developing TWS5 is finding intuitive models in such a way that completeness remains provable. Such models, at the same time, must reflect what is naturally meant by a protocol execution. We define the semantics of TWS5 in terms of validity over possible states of a Kripke model that is generated by a so-called message passing interpreted system [16]. Each possible state corresponds to a set of messages sent or received by agents involved in an execution of the protocol up to a particular time. We prove that TWS5 is complete.

Although there are many dynamic epistemic logics used for modeling knowledge protocols, we do not investigate them in this paper because they are inconvenient in a cryptographic setting for generating equivalence relations among messages [15, 38]. The rest of this paper is organized as follows: In Sect. 2, we present a motivating example that justifies why an effective logic for verifying authentication protocols should be temporal and omniscience-free. Section 3 is an overview of an omniscience-free epistemic logic which we call it WS5. In Sect. 4, we propose the syntax and semantics of our logic TWS5. The proof of completeness is given in Sect. 5. In Sect. 6, we show that TWS5 is useful in verifying authentication protocols. Section 7 concludes the paper.

2 Motivating Example

We give an example to show why an effective epistemic logic for verifying authentication protocols must have temporal operators and be omniscience-free. Our example is the protocol in Fig. 1. It is a variant of the stream authentication protocol TESLA [35]. Using this protocol, the sender S sends a stream of messages he has encrypted by his secret key $k_{\text {s}}$ to the receiver R. The protocol is intended to preserve the authenticity of the source and messages.

Fig. 1

A variant of the stream authentication protocol TESLA

In this protocol $n_r$ is a nonce generated by R and the packet $P_i$ is of the form

$$\begin{aligned} \{m_i\}_{k_{\text {s}}}\cdot f(k_{i+1})\cdot k_{i-1}\cdot {\text {mac}} \big (g(k_i),\quad \{m_i\}_{k_{\text {s}}}\cdot f(k_{i+1}). k_{i-1}\big ) \end{aligned}$$

for $i=2,3,\ldots$ where f and g are two one-way functions known to everyone, $k_{i+1}$ is the fresh key S has chosen in the ith step of the protocol, and “mac” is a message authentication code used in the verification of messages sent through packets. The message authentication code has two inputs separated by a camma notation. To authenticate $\{m_i\}_{k_{\text {s}}}$, R must wait for the next packet $P_{i+1}$. By receiving $P_{i+1}$, R extracts $k_i$ and computes $f(k_i)$ and compares it with the commitment, i.e., $f(k_i)$, sent in packet $P_{i-1}$. If the two values are equal, R concludes that $k_i$ is safe. Then, R computes ${\text {mac}}\big (g(k_i), \{m_i\}_{k_{\text {s}}}\cdot f(k_{i+1})\cdot k_{i-1}\big )$ and verifies the authenticity of $\{m_i\}_{k_{\text {s}}}$. The authenticity of the source of $P_i$ is inductively established on the basis of the belief formed when R receives $P_{01}$ carrying his own nonce $n_r$ encrypted by the source’s private key $pr_{\text {s}}$. This protocol can be used in outsourced databases whenever the receiver who keeps the sender’s encrypted records in his database asks the sender to update the records or create new ones.

Stream authentication protocols may operate in different modes [34]. An operation mode is defined to be a pair ([u, v], d) where $u,v,d \in \mathbb {N}$ and $d \ne 0$. If the protocol operates in this mode, the arrival time of every packet sent at time t can be at an instant in $[t+u,t+v]$. If the packet is received outside this time interval it is not accepted as a valid packet—the clocks of the sender and the receiver are synchronized. Moreover, the time distance between the transmission of two consecutive packets is d. If $v \ge d$, the protocol in Fig. 1 may be vulnerable to attack and fail in providing authentication requirements. In fact, S may consecutively send two packets which are intercepted by the adversary C. The adversary then forges the first packet by the information he obtains from the second one and sends the resulting packets to R. If the time taken by the attacker to alter and send packets to R is small enough, R will accept the packets. In this way, R is deceived into accepting ungenuine packets. Indeed, the so-called agreement [27] may not be established between S and R. The following describes an example attack which exploits this vulnerability.

Fig. 2

Executions $h_1$ and $h_2$ of the protocol shown in Fig. 1

Let C(S) and C(R) stand for a principal C impersonating S and R and $k_{\text {c}}$ be C’s secret key. An execution is considered to be a sequence of messages sent or received by a principal. Assume that there are at least two executions $h_1$ and $h_2$ of this protocol shown in Fig. 2 and where we use snd and rcv to represent sending and receiving a message by a principal in a model, i.e., a semantic notation, and snt and rcvd are used as the syntactic representation of the same. As seen in $h_2$, principal C is an adversary that intercepts $P_i$ and $P_{i+1}$. It infers $k_i$ from $P_{i+1}$ and uses this key to change the packet $P_i$ in which $\{m_i\}_{k_{\text {s}}}$ is replaced by $\{m'_i\}_{k_{\text {c}}}$. After changing $P_i$, C impersonates S and sends the forged packet along with the original packet $P_{i+1}$, in order, to R. This attack is possible in the mode of operation ([1, 4], 2), for example. The sender sends $P_i$ and $P_{i+1}$ at t and $t+2$. The attacker receives these two packets at $t+1$ and $t+3$. If the packets the attacker sends to the receiver are received at $t+4$ and $t+6$, they are accepted by the receiver since they are received in time intervals $[t+1, t+4]$ and $[t+3, t+6]$ as expected. Thus, the protocol is vulnerable to the attack.

Suppose that we want to investigate whether the run of the protocol in Fig. 1 between S and R can assure R that the ith packet received has certainly been sent by S. This requirement may be specified in an epistemic logic by a formula like $R \ \mathrm{{knows}} \ S \ {\text {snt}} \ P_i$. Now, assume that we employ an epistemic logic to verify this protocol against the property specified above, but the logic is not omniscience-free. In such a logic, $A \ \mathrm{{knows}} \ \phi$ is true in a possible world w whenever $\phi$ is true in every world reachable from w. Such an interpretation of truth leads to omniscience. Moreover, assume that $h_1$ and $h_2$ in Fig. 2 are two possible worlds in the model of the protocol. Thus, to show that the formula is true in $h_1$, we should verify $S \ {\text {snt}} \ P_i$ in every execution being indistinguishable from $h_1$ in R’s view. Since R does not know $k_{\text {s}}$ and $k_{\text {c}}$, he cannot distinguish between $\{m_i\}_{k_{\text {s}}}$ and $\{m'_i\}_{k_{\text {c}}}$, and consequently, $h_1$ is indistinguishable from $h_2$ in his view. As $S \ {\text {snt}} \ P_i$ holds in $h_2$, these two possible worlds, i.e., $h_1$ and $h_2$, are not enough to refute the above property. At the same time, $h_2$ indicates an attack and is reasonable to take part in a counterexample for the property.

If we use an omniscience-free epistemic logic such as WS5 [11], then $h_2$ is enough to refute the property. In fact, WS5 requires a modified set of statements to be true in the worlds accessible from the world the truth of a given modal formula is being investigated. Recall that the possible worlds $h_1$ and $h_2$ are indistinguishable in R’s view because he cannot differentiate between $\{m_i\}_{k_{\text {s}}}$ and $\{m'_i\}_{k_{\text {c}}}$. Now, consider the renaming function $\rho$ that maps the message $\{m_i\}_{k_{\text {s}}}$ to $\{m'_i\}_{k_{\text {c}}}$ and keeps the other messages intact. The modified formula that must hold in $h_2$ is then

$$\begin{aligned} S \ {\text {snt}} \ \rho \big ( \{m_i\}_{k_{\text {s}}} \big ).f(k_{i+1})\cdot k_{i-1}\cdot {\text {mac}}\big (g(k_i), \rho \big (\{m_i\}_{k_{\text {s}}} \big ) \cdot f(k_{i+1}). k_{i-1}\big ) \end{aligned}$$

which is equal to

$$\begin{aligned} S \ {\text {snt}} \ \{m'_i\}_{k_{\text {c}}} \cdot f( k_{i+1})\cdot k_{i-1}\cdot {\text {mac}}\big (g(k_i), \{m'_i\}_{k_{\text {c}}}\cdot f(k_{i+1})\cdot k_{i-1}\big ). \end{aligned}$$

As this formula is not true in $h_2$, the property is refuted.

Fig. 3

The specification of the protocol shown in Fig. 1 using epistemic and temporal operators

The receiver may receive the ith packet sent at time t at most v clock ticks later. As stated above, the security of the protocol depends on its mode of operation. Thus, an appropriate logic for the specification of the protocol and requirements should additionally have temporal operators like next and its derived form $\mathrm{{next}}^{t}$ representing the next clock tick and t clock ticks later, respectively. In Fig. 3, $S_1$ is an axiom scheme in which A and B can be any principal including the sender S, the receiver R, and an intruder C. Moreover, X can be a packet sent by a principal. For example, the consecutive packets sent and received in $h_1$ and $h_2$ (Fig. 2) can be represented as appropriate instances of $S_1$. The axiom scheme S5 represents the fact that the key $k_i$ that is used in $g(k_i)$ of the ith packet is disclosed d time units later. The following formalizes the authentication requirement for the packet $P_i$ with $i \ge 1$ as a modal formula using epistemic and temporal operators.

$$\begin{aligned} \mathrm{{next}}^{(i+1)d+v} \ R \ \mathrm{{knows}} \ S \ {\text {snt}} \ P_i. \end{aligned}$$

3 WS5: An Omniscience-Free Epistemic Logic

The logic proposed in this paper builds on an epistemic logic for verifying authentication protocols [11]. We name it WS5 since it can be thought of as a variant of S5 in which there is a weak necessitation rule. In WS5, modal operators represent the knowledge of the agents identified by the set $\mathcal {A}=\{A_1,\ldots ,A_n \}$. In this logic, propositions are about messages. A message may be atomic or be constructed from two messages m and $m'$ by pairing or encryption, denoted $m.m'$ and $\{m\}_{m'}$, respectively. The sub-message relation ‘$\le$’ is defined as the smallest reflexive and transitive relation on messages satisfying $m,m' \le \{m \}_{m'}$ and $m,m'\le m.m'$. The converse of ‘$\le$’ is noted ‘$\ge$’ as well. The set of all messages is assumed to be a finite set $\tau$, a subset of which is the set of keys.¹

An atomic formula is a proposition a(m) in which $m \in \tau$ and a is a keyword of the set $\mathcal {P}=\{A \ \ {\text {snt}}, \ A \ \ {\text {rcvd}}, \ A \ \ {\text {sen}}, \ A \ \ {\text {rec}}, \ {\text {exists}}, \ {\text {unfresh}} \ | \ A \in \mathcal {A}\}$. Atomic formulae can be interpreted as follows:

• $A \ {\text {snt}} \ m$: A has sent m.

• $A \ {\text {rcvd}} \ m$: A has received m.

• $A \ {\text {sen}} \ m$: A has sent $m'$ and m is a sub-message of $m'$.

• $A \ {\text {rec}} \ m$: A has received $m'$ and m is a sub-message of $m'$.

• ${\text {exists}} \ m$: An agent has sent or received $m'$ and m is a sub-message of $m'$.

• ${\text {unfresh}} \ m$: m is not fresh.²

There is also an auxiliary keyword infers that is interpreted as follows:

• $A \ {\text {infers}} \ m$: m is among the initial knowledge of A or it can be computed on the basis of what A knows.

For a given set of atomic formulae $\Omega$, a formula of the logic is defined inductively as follows:

• Every $p \in \Omega$ is a formula.

• If $\phi$ and $\psi$ are formulae, then so are $\lnot \phi$ and $\phi \rightarrow \psi$.

• If $\phi$ is a formula, then $K_i \phi$ is a formula for every $1 \le i \le n$, where the intended meaning of $K_i \ \phi$ is “Agent $A_i$ knows $\phi$.”

The model of a protocol represents the set of all possible executions of that protocol. An execution can also be interpreted as a set of interactions between agents through the steps defined in the protocol. By such an interpretation, a protocol execution may comprise several interleaving runs of the protocol. In every possible execution of a protocol, agents in $\mathcal {A}$ interact with each other through the actions they take on messages and the knowledge of an agent is characterized by a finite set of atomic formulae which is called the local state for that agent. Each execution of a protocol is then represented by a global state which is the union of agents’ local states. In the view of an agent, there may be a set of conceivable global states, as it does not know the local states of the others. This makes a basis for the access relation in the standard Kripke semantics. In this way, the set of all possible global states would be the set of possible worlds, W, of a Kripke model. In this model, there are also n equivalence relations $\{\sim _i\}_{1 \le i \le n}$ on W. If two global states are in the same class induced by $\sim _i$, then they are indistinguishable in $A_i$’s view in the sense that $A_i$ has equal local states in the two global states. Notice that the idea of using an indistinguishability relation for modeling what an agent sees from a protocol execution has been applied in earlier works, e.g., [1, 2, 17].

A model also includes an interpretation function $\pi$ from $\Omega$ to $2^W$, where $\pi (p)=W' \subseteq W$ means that p holds in every possible world $w \in W'$. Thus, a model is a triple $\langle W,\{\sim _i\},\pi \rangle$. As inspired by the motivating example, however, this model may lead to invalid judgments about protocols. In what follows, it is seen that the problem can be resolved by a modified interpretation of accessibility relation and truth definition.

In epistemic logics for cryptographic properties, encrypted parts in the scope of a modal operator are interpreted under $de \ re$ interpretation [11]. Consider the statement $K_i \ A_i \ {\text {rcvd}} \ \{m\}_k$ which states that $A_i$ knows that he has received $\{m\}_k$. Under $de \ re$ interpretation, $A_i$ knows that he has received the message m encrypted by k as if he has an unlimited decryption power. Such a decryption power may cause logical omniscience. That is, if $\phi \rightarrow \phi '$ is a valid formula, then so is $K_i \phi \rightarrow K_i \phi '$. For example, the formula $A_i \ {\text {rcvd}} \ \{m\}_k \rightarrow {\text {exists}} \ m$ holds for every agent $A_i$, whereas $K_i \ A_i \ {\text {rcvd}} \ \{m\}_k \rightarrow K_i \ {\text {exists}} \ m$ may not be true. In fact, the latter is true only if $A_i$ knows the key k so that it can use this key to compute m. Therefore, logical omniscience may contradict resource-bounded knowledge and it may result in formulae that are not indeed valid.

To avid omniscience, the access relation in an agent’s view is tagged with a message renaming function $\rho : \tau \rightarrow \tau$. The following concepts are required for defining the modified access relation. Note that although $\rho$ is considered as an operation on messages, it can also be applied to statements. In doing so, it is applied to the messages in the given statement. The application of $\rho$ to messages, however, is subject to the messages $\rho$ is consistent with.

Definition 3.1

A message renaming function $\rho :\tau \rightarrow \tau$ is defined to be consistent with a set $\kappa \subseteq \tau$, written $\rho \ \triangleleft \ \kappa$, iff the following conditions are satisfied.

• $\rho (c)=c \$ for any atomic message c.

• $\rho (\{m\}_k)=\{\rho (m)\}_{\rho (k)}$ for every $k \in \kappa$.

• $\rho (m.m')=\rho (m). \rho (m')$.

As agents can distinguish atomic (constant) messages, any consistent message renaming function maps an atomic message to itself. It is also worth noting that message renaming functions are total functions. As an example, assume that $A_i$ infers a set of keys $\kappa$ and $\rho \ \triangleleft \ \kappa$. If $k \in \kappa$, $\rho (\{m\}_k)$ is equal to $\{\rho (m)\}_{\rho (k)}$ in $A_i$’s view. $A_i$ can indeed expand $\rho$ through the encrypted message because he infers the right decryption key k. If $k \not \in \kappa$, $A_i$ may just see $\rho (\{m\}_k)$, which is a message in the form of an atomic or an encrypted message or even the concatenation of two messages.

A WS5 model $\mathcal {M}$ is then defined to be a triple $\langle W, \{\leadsto ^{\rho }_i\}, \pi \rangle$ in which W is the set of all possible executions of a protocol and $\pi$ is the interpretation function. Moreover, when we say that the global state $s \in W$ has access to the global state $t \in W$ in $A_i$’s view with respect to $\rho$, denoted by $s \leadsto _i^{\rho } t$, it means that the application of $\rho$ to the local state of $A_i$ in s is equal to its local state in t and $\rho$ is consistent with the keys $A_i$ infers from s. It is proven that if the global state s has access to the global state t in $A_i$’s view with respect to $\rho$, then t has access to s in $A_i$’s view with respect to $\rho ^{-1}$ [12]. Therefore, we use the notation $\leadsto _i^{\rho }$ to indicate that this relation is not symmetric.

Fig. 4

Truth definition in WS5

Fig. 5

Proof system of WS5

The truth of a formula in a world w of a given model $\mathcal {M}$ can then be inductively defined. Figure 4 gives the definition. A formula $\phi$ is said to be valid, denoted by $\models \phi$, if $(\mathcal {M},w) \models \phi$ holds for every model $\mathcal {M}$ and every possible world w of $\mathcal {M}$. A formula $\phi$ is satisfiable if there exists a model $\mathcal {M}$ and a possible world w of $\mathcal {M}$ such that $(\mathcal {M},w) \models \phi$.

The proof system of WS5 is shown in Fig. 5 in which $\phi$ and $\psi$ are formulae, m and $m'$ are messages, and k is a key. Moreover, note that WS5 is a propositional logic and the symbol $\exists$ in axioms A8–A10 is a syntactic sugar for the disjunction of a finite number of statements. Moreover, the symbol $\forall$ in rule Nec is a syntactic sugar to represent all of the finite number of premises of the rule. It has been proven that WS5 is sound and complete with respect to the generalized Kripke semantics given in this section [11].

4 TWS5: A Temporal Epistemic Logic of Authentication Protocols

In this section, we propose a complete and omniscience-free temporal epistemic logic for the verification of authentication protocols. The underlying attacker model is also defined through the consistent message renaming functions involved in access relations. Our logic extends WS5 with temporal operators and is referred to as Temporal WS5, or TWS5 for short. The main challenging issue in developing this logic is finding intuitive models that reflect precedence among the actions taken by the agents in a protocol execution and the formation of knowledge with respect to performed actions. At the same time, the formulation of models should result in completeness. The reason for incorporating temporal operators in the logic is to provide the capacity for analyzing those protocols whose correctness largely depends on timely formation of agents’ knowledge. Such protocols, e.g., stream authentication protocols, can only be verified by logics involving both knowledge and temporal operators [19]. As stated earlier, omniscience is a feature of epistemic logics that may result in misleading judgments about the protocols being analyzed. In this regard, the logic WS5 can serve as a candidate core for our logic as it is omniscience-free.

4.1 The Formulae and Models of TWS5

The formulae and models of TWS5 are defined on the basis of the set of agents $\mathcal {A}$, the set of keywords $\mathcal {P}$, the sub-message relation $\le$, and the set of messages $\tau$ given in Sect. 3. The formulae of TWS5, however, may involve temporal operators and, in turn, the models should additionally reflect the meaning of these operators.

Definition 4.1

Given a set of atomic formulae $\Omega$, the set $\mathcal {F}$ of TWS5 formulae is defined inductively by the following rules where $\bigcirc$ and $\mathcal {U}$ are symbols for next and until temporal operators.

• If $p \in \Omega$, then $p \in \mathcal {F}$.

• If $\phi , \psi \in \mathcal {F}$, then $\lnot \phi , \phi \rightarrow \psi \in \mathcal {F}$.

• If $\phi \in \mathcal {F}$, then $K_i \phi \in \mathcal {F}$ for every $1 \le i \le n$.

• If $\phi , \psi \in \mathcal {F}, \ \mathrm{then} \bigcirc \phi , \ \phi \ \mathcal {U} \ \psi \in \mathcal {F}$.

The meaning of a TWS5 formulae is given in terms of validity over possible worlds of a Kripke model generated by a message passing interpreted system (MPIS) [16], where agents send and receive messages. In what follows, we develop the semantics of TWS5.

Definition 4.2

For a given set of agents $\mathcal {A}$ and a set of messages $\tau$, the initialization function is defined to be a function $\mathrm{init}_{\mathcal {A},\tau }: \mathcal {A} \rightarrow 2^\tau$ that assigns every agent $A_i \in \mathcal {A}$ a set of messages. An action is also defined to be an element of the set $\Pi _{\mathcal {A},\tau }=\{A_i \ {\text {snd}} \ m, \ A_i \ {\text {rcv}} \ m \ | \ A_i \in \mathcal {A}, \ m \in \tau \}$.

Definition 4.3

Given a set of agents $\mathcal {A}$ and a set of messages $\tau$, an execution h until a time instant t is a finite multiset h(t) such that $h(t-1) \subset h(t)$, $h(t) \setminus h(t-1) \subset \Pi _{\mathcal {A},\tau }$, and $h(0)= \left\{ A_i \ {\text {rcv}} \ m \ | \ A_i \in \mathcal {A}, \ m \in {\text {init}}_{\mathcal {A},\tau }(A_i) \right\}$. In fact, the messages that agents receive in h(0) are those messages that they initially infer. The finite multiset h(t) is also called an execution history.

Definition 4.4

Let $A_i \in \mathcal {A}$. The execution history h(t) in $A_i$’s view, denoted by $h(t)|A_i$, is defined as $h(t)|A_i=h(t) \setminus \left\{ A_j \ {\text {snd}} \ m, A_j \ {\text {rcv}} \ m \ | \ m \in \tau , \ A_j \ne A_i \right\} .$

Definition 4.5

Given a set of agents $\mathcal {A}$ and a set of messages $\tau$, an MPIS, or a TWS5 model, is defined to be a triple $\mathcal {M}= \langle H, \{\leadsto _{i}^{\rho }\}, I\rangle$ such that

• $H=\bigcup _t H_t$ is the set of possible worlds where $H_t$ is the set of all possible executions until t,

• for an agent $A_i \in \mathcal {A}$ and a message renaming function $\rho : \tau \rightarrow \tau$, $\leadsto _{i}^{\rho } \subseteq H \times H$ is the accessibility relation for $A_i$ under $\rho$ such that for every two possible worlds h(t) and $h'(t')$, $h(t) \leadsto _{i}^{\rho } h'(t')$ iff $\rho$ is consistent with the keys $A_i$ infers from h(t) and the application of $\rho$ to $h(t)|A_i$ is equal to $h'(t')|A_i$, and

• I is an interpretation function from the set of atomic formulae to the power set of possible worlds, i.e., $I: \Omega \rightarrow 2^H$, defined by

  • $I(A_i \ {\text {snt}} \ m)=\{h(t) \in H \ | \ A_i \ {\text {snd}} \ m \in h(t)\}$,

  • $I(A_i \ {\text {rcvd}} \ m)=\{h(t) \in H \ | \ A_i \ {\text {rcv}} \ m \in h(t)\}$,

  • $I(A_i \ {\text {sen}} \ m)=\{h(t) \in H \ | \ \exists m' \ge m. \ A_i \ {\text {snd}} \ m' \in h(t)\}$,

  • $I(A_i \ rec \ m)=\{h(t) \in H \ | \ \exists m' \ge m. \ A_i \ {\text {rcv}} \ m' \in h(t)\}$,

  • $I({\text {exists}} \ m)=\{h(t) \in H \ | \ \exists A_i \in \mathcal {A}. \exists m' \ge m. \ A_i \ {\text {snd}} \ m' \in h(t) \vee A_i \ {\text {rcv}} \ m' \in h(t)\}$, and

  • $I({\text {unfresh}} \ m)=\{h(t) \in H \ | \ \exists A_i \in \mathcal {A}. \ \exists t'<t_b. \ h(t') \in I(A_i \ {\text {sen}} \ m)\}$. Here, $t_b$ represents the start of the current epoch containing t. The details can be found in [2], but the interpretation of ${\text {unfresh}}$ is not critical and other interpretations can also be used.

We also make use of an auxiliary keyword infers. The formula “$A \ infers \ m$” is meant to reflect the fact that m is among the initial knowledge of A or can be derived from what A knows. The formula “$K_A \ \mathrm{exists} \ m$” reflects the same and can be regarded as the interpretation of “$A \ \mathrm{infers} \ m$” [11].

Definition 4.6

Given a model $\mathcal {M}=\langle H, \{\leadsto _{i}^{\rho }\}, I \rangle$, for any $\phi , \psi \in \mathcal {F}$, any $a(m) \in \Omega$, and any $h(t) \in H$, the truth of a formula is defined as follows:

• $(\mathcal {M},h(t)) \models a(m)$ iff $h(t) \in I(a(m))$.

• $(\mathcal {M},h(t)) \models \lnot \phi$ iff $(\mathcal {M},h(t)) \not \models \phi$.

• $(\mathcal {M},h(t)) \models \phi \rightarrow \psi$ iff $(\mathcal {M},h(t)) \models \phi$ implies $(\mathcal {M},h(t)) \models \psi$.

• $(\mathcal {M},h(t)) \models \bigcirc \phi$ iff $(\mathcal {M},h(t+1)) \models \phi$.

• $(\mathcal {M},h(t)) \models \phi \ \mathcal {U} \ \psi$ iff for some $t'>t$, $(\mathcal {M},h(l)) \models \phi$ for any $t\le l <t'$ and $(\mathcal {M},h(t')) \models \psi$.

• $(\mathcal {M},h(t)) \models K_i \phi$ iff, for every $h'(t') \in H$ and every message renaming function $\rho :\tau \rightarrow \tau$, $h(t) \leadsto _i^{\rho } h'(t')$ implies that $(\mathcal {M},h'(t'))\models \rho (\phi )$.

Notice that although at the first glance the definition of truth for the formula $K_i \phi$ involves arbitrary renaming functions $\rho$, the premise $h(t)\leadsto _i^{\rho } h'(t')$ limits them to those consistent with the keys inferred in h(t).

Now, we give a proof system for TWS5 formulae.

4.2 Proof System of TWS5

Definition 4.7

Let $\phi , \phi ', \psi \in \mathcal {F}$ and $a(m) \in \Omega$, the proof system of TWS5 consists of the following axioms and rules.

• A1-A10, K, T, 4, and 5: All axioms of WS5.

• A11: $\bigcirc \phi \wedge \bigcirc (\phi \rightarrow \psi ) \rightarrow \bigcirc \psi$

• A12: $\bigcirc \lnot \phi \leftrightarrow \lnot \bigcirc \phi$.

• A13: $\phi \ \mathcal {U} \ \psi \leftrightarrow \psi \vee (\phi \wedge \bigcirc (\phi \ \mathcal {U} \ \psi ))$

• A14: $a(m)\rightarrow \bigcirc a(m)$.

• R1: $\dfrac{\phi }{\bigcirc \phi } (TG)$

• R2: $\dfrac{\phi ' \rightarrow (\lnot \psi \wedge \bigcirc \phi ')}{\phi ' \rightarrow \lnot (\phi \ \mathcal {U} \ \psi )}$(NU).

• R3: $\dfrac{\phi \ \ \phi \rightarrow \psi }{\psi } (MP)$

• R4: $\dfrac{\rho (\phi ), \ \ \ \ \forall \rho \triangleleft \kappa }{A_i \ \mathrm{infers} \ \kappa \rightarrow K_i \phi }$(Nec).

In the rules above, the names TG, NU, MP, and Nec are abbreviations for Temporal Generalization, Next-Until, Modus Ponens, and Necessitation, respectively.

A formula $\phi \in \mathcal {F}$ is true (or holds) in a TWS5 model $\mathcal {M}=\langle H, \{\leadsto ^{\rho }_i\}, I\rangle$ if for any $h(t) \in H$ we have $(\mathcal {M}, h(t)) \models \phi$. A formula $\phi \in \mathcal {F}$ is valid if it is true in every TWS5 model. A TWS5 rule is valid if it preserves validity, that is, the validity of its premises results in the validity of its conclusion.

Theorem 4.8

TWS5 is sound.

Proof

The validity of axioms A11, A12, A13, and rules TG and NU results from Definition 4.6. Axiom A14 is also valid due to Definition 4.3. The validity of those axioms of TWS5 that are inherited from the WS5 proof system as well as the rules MP and NEC are immediate.

5 Completeness

We prove that TWS5 is complete. To do so, we first give a short overview of the needed concepts, see [16]. Assume that $\mathcal {X}$ is an axiomatization system. A formula $\phi$ is $\mathcal {X}$-consistent if $\lnot \phi$ is not provable in $\mathcal {X}$. A finite set $\{\phi _1, \ldots , \phi _k\}$ is $\mathcal {X}$-consistent if $\phi _1 \wedge \cdots \wedge \phi _k$ is $\mathcal {X}$-consistent. An infinite set of formulae is $\mathcal {X}$-consistent if its every finite subset is $\mathcal {X}$-consistent. A set $\Delta$ of formulae is maximal $\mathcal {X}$-consistent if $\Delta$ is $\mathcal {X}$-consistent and for any formula $\phi \not \in \Delta$, $\Delta \cup \{\phi \}$ is not $\mathcal {X}$-consistent. It is known that any $\mathcal {X}$-consistent set $\Delta$ can be extended to a maximal $\mathcal {X}$-consistent set if $\mathcal {X}$ contains all of the tautologies of propositional calculus and the rule MP. Any maximal $\mathcal {X}$-consistent set $\Delta$ satisfies the properties shown in Fig. 6.

Fig. 6

Properties of a maximal consistent set $\Delta$

Let $\mathcal {M}_n$ be the class of all TWS5 models for n agents. To prove the completeness of TWS5, we should show that every formula $\phi \in \mathcal {F}$ that is valid with respect to $\mathcal {M}_n$ is provable in the proof system of TWS5. We can equivalently prove that the following property holds.

$$\begin{aligned} \mathrm{Every} \ {\text {TWS5-consistent}} \ \mathrm{formula} \ \mathrm{is} \ \mathrm{satisfiable} \ \mathrm{with} \ \mathrm{respect} \ \mathrm{to} \ \mathcal {M}_n. \end{aligned}$$

(5.1)

Suppose that we can prove (5.1) and $\phi$ is a valid formula. If $\phi$ is not provable in the TWS5 proof system, its double negation $\lnot \lnot \phi$ is not provable either. Therefore, $\lnot \phi$ is a TWS5-consistent formula and consequently $\lnot \phi$ is satisfiable with respect to $\mathcal {M}_n$. This contradicts the validity of $\phi$. Hence, (5.1) implies completeness.

The sketch of the completeness proof is as follows: To prove completeness, we equivalently prove that every TWS5-consistent formula is satisfiable with respect to $\mathcal {M}_n$. To do so, we employ the general technique of building canonical models. Indeed, we build the canonical model $\mathcal {N}^c$ which has a state w corresponding to every maximal TWS5-consistent set w. We also show that a TWS5 formula $\phi$ belongs to w if it is satisfiable in a maximal TWS5-consistent set w of $\mathcal {N}^c$. Then, we prove that every TWS5-consistent formula is satisfiable with respect to $\mathcal {N}^c$. As $\mathcal {N}^c$ does not have the right shape of an MPIS, we extract a filtration model $\mathcal {M}^c \in \mathcal {M}_n$ from the canonical model. The possible worlds of $\mathcal {M}^c$ are execution histories that build on specific sequences of the possible worlds of $\mathcal {N}^c$. It is proven that if a TWS5 formula is satisfiable in a maximal TWS5-consistent set w of $\mathcal {N}^c$, then it is also satisfiable in the corresponding possible world of $\mathcal {M}^c$. Thus, we can prove that every TWS5-consistent formula is satisfiable with respect to $\mathcal {M}^c$. Since $\mathcal {M}^c \in \mathcal {M}_n$, it follows that TWS5 is complete.

We use the notion of counterpart models to build a canonical model. Counterpart models are used as a semantics for first order modal logics where new values are assigned to variables when we move along the accessibility relation [?]. In TWS5, we use a message renaming function to map a formula of a global state to another one and demand that the resulting formula should hold in the global state to which the current state has access. Intuitively, a message m at a possible world w corresponds to (is a counterpart of ) $m'$ at a possible world $w'$ in $A_i$’s view if $A_i$ cannot distinguish between m and $m'$.

In the following arguments, by $\rho (\Delta )$ we mean the set $\{\rho (\phi ) \ | \ \phi \in \Delta \}$ where $\Delta$ is a set of TWS5 formulae and $\rho$ is a message renaming function.

Lemma 5.1

Let $\mathcal {N}_n$ be the class of all counterpart Kripke models for n agents. There is a model $\mathcal {N}^c \in \mathcal {N}_n$, called a canonical model, where its possible worlds are maximal TWS5-consistent sets such that for any possible world w of $\mathcal {N}^c$ we have $(\mathcal {N}^c, w)\models \phi$ iff $\phi \in w$.

Proof

For a given set of TWS5 formulae w, we define $w/K_i=\{\phi \ | \ K_i \phi \in w\}$ and $w/\bigcirc =\{\phi \ | \bigcirc \phi \in w\}$. Now, define the canonical model $\mathcal {N}^c=\langle W, \pi , \{\rightarrow ^{\rho }_i\}, \prec \rangle$ as follows:

• $W=\{w \ | \ w$ is a maximal TWS5-consistent set$\}$.

• $\pi (w)(a(m))=\mathrm{true}$ if $a(m) \in w$, $a(m) \in \Omega$.

• $\pi (w)(a(m))=\mathrm{false}$ if $a(m) \not \in w$, $a(m) \in \Omega$.

• $\rightarrow ^{\rho }_i=\{(w, w') \ | \ \rho (w/K_i) \subseteq w'\}$ for any message renaming function $\rho :\tau \rightarrow \tau$ with $\rho \triangleleft \kappa$ where $\kappa$ is the set of messages $A_i$ infers from w, that is, $A_i \ \mathrm{infers} \ \kappa \in w$.

• $\prec =\{(w, w') \ | \ w/\bigcirc \subseteq w'\}$.

The proof continues by induction on the number of the logical operators of TWS5 formulae. Assume that the property holds for all formulae with $n-1$ operators, we show that it also holds for any formula $\phi$ with n operators. The proof for atomic formulae and the ones constructed from atomic formulae using $\lnot$ and $\rightarrow$ is immediate. Now, assume that $\phi$ is $K_i \psi$ for some $\psi$. For the ‘if’ part, we have $\phi \in w$. Therefore, $\psi \in w / K_i$. Now for every $(w, w') \in \rightarrow ^{\rho }_i$, $\rho (\psi ) \in w'$. Therefore, by the induction hypothesis, we have $(\mathcal {N}^c,w')\models \rho (\psi )$. Using Definition 4.6, we can conclude that $(\mathcal {N}^c,w) \models K_i \psi$.

For the ‘only if’ part, assume that $(\mathcal {N}^c, w) \models K_i \psi$. Now, for every message renaming function $\rho :\tau \rightarrow \tau$ such that $\rho \triangleleft \kappa$ and $A_i \ infers \ \kappa \in w$, consider the set $\rho (w/K_i) \ \cup \ \rho (\lnot \psi )$. Any such set is not TWS5-consistent as otherwise there exists a maximal TWS5-consistent set $w'$ such that $\rho (w/K_i) \cup \rho (\lnot \psi ) \subseteq w'$ and consequently $(w,w') \in \rightarrow ^{\rho }_i$. Using the induction hypothesis we have $(\mathcal {N}^c,w') \models \rho (\lnot \psi )$ and, in turn, $(\mathcal {N}^c,w) \models \lnot K_i \psi$ which is a contradiction. Therefore, there exists a finite subset $\rho (\phi _1), \ldots , \rho (\phi _l), \rho (\lnot \psi )$ of $\rho (w/K_i)\cup \rho (\lnot \psi )$ which is not TWS5-consistent. We can show that $\vdash \rho (\phi _1) \rightarrow (\rho (\phi _2) \rightarrow (\cdots \rightarrow (\rho (\phi _l) \rightarrow \rho (\psi ))\cdots ))$. Since $\rho$ only applies to messages appearing in the formulae, we have $\vdash \rho (\phi _1 \rightarrow (\phi _2 \rightarrow (\cdots \rightarrow (\phi _l \rightarrow \psi ))\cdots ))$. By the rule Nec, we conclude that $\vdash K_i(\phi _1 \rightarrow (\phi _2 \rightarrow (\cdots \rightarrow (\phi _l \rightarrow \psi )\cdots ))$. By induction on l, axiom K and MP, we have $\vdash K_i\phi _1 \rightarrow (K_i\phi _2 \rightarrow (\cdots \rightarrow (K_i \phi _l \rightarrow K_i \psi )\ldots ))$. Using Property 4 in Fig. 6, we have $K_i\phi _1 \rightarrow (K_i\phi _2\rightarrow (\cdots \rightarrow (K_i \phi _l \rightarrow K_i\psi )\cdots )) \in w$. For any message renaming function $\rho :\tau \rightarrow \tau$ such that $\rho \triangleleft \kappa$ and $A_i \ infers \ \kappa \in w$, we have $\rho (\phi _1), \ldots , \rho (\phi _l)\in \rho (w/K_i)$. Thus, Nec implies $K_i \phi _1, \ldots , K_i \phi _l \in w$. Hence, from Property 3 in Fig. 6, we have $K_i \psi \in w$. The proof when $\phi$ is of the form $\bigcirc \psi$ or $\psi \ \mathcal {U} \ \psi '$ is standard using the definition of $\prec$ as well as the axiom NU. $\square$

Theorem 5.2

Every TWS5-consistent formula is satisfiable with respect to $\mathcal {N}_n$.

Proof

If $\phi$ is TWS5-consistent, then there exists a maximal TWS5-consistent set w such that $\phi \in w$. From Lemma 5.1, we have $(\mathcal {N}^c, w)\models \phi$ and consequently $\phi$ is satisfiable with respect to $\mathcal {N}_n$.

Given maximal $\mathcal {X}$-consistent sets $w_0, w_1, \ldots$, a sequence $\alpha =\langle w_0, w_1, \ldots \rangle$ is acceptable if $(w_k, w_{k+1}) \in \prec$ for any $k\ge 0$ and, for any $\psi _1 \ \mathcal {U} \ \psi _2 \in w_k$, there exists some $l \ge k$ such that $\psi _2 \in w_l$ and $\psi _1 \in w_{k'}$ with $k \le k'< l$. It has been proven that for any maximal $\mathcal {X}$-consistent set w, there exists an acceptable sequence starting with it. Moreover, for any $\mathcal {X}$-consistent set w, there is an acceptable sequence containing w [16].

Lemma 5.3

For any formula $\phi \in \mathcal {F}$ and mapping $\lambda : \tau \rightarrow \tau$, $\vdash \phi$ implies $\vdash \lambda (\phi )$.

Proof

The proof is by induction on the length of the proof of $\phi$. Assume that for every mapping $\lambda$ the above property holds for every proof of $\phi$ of length less than n. Now, we have to show that for every mapping $\lambda$, if $\phi$ is a theorem with a proof of length n, then $\lambda (\phi )$ is also a theorem. We should check that this property is preserved when applying the axioms and rules of TWS5. Assume that $\phi =K_j \psi$ and that we want to check Nec rule

$$\begin{aligned} \dfrac{\rho (\psi ), \forall \rho \triangleleft \kappa }{A_j \ \mathrm{infers} \ \kappa \rightarrow K_j \psi }. \end{aligned}$$

The proof for other axioms and rules is immediate.

Since the set of messages $\tau$ is finite, the set of message renaming functions that are consistent with the keys $A_j$ infers is assumed to be $\{\rho _1, \ldots , \rho _l\}$. Evidently, $\rho _1 (\psi ), \ldots , \rho _l (\psi )$ are theorems with proof length less than n. Hence, if we define message renaming functions $\lambda '=\rho _i \circ \lambda \circ \rho ^{-1}_i$, then $\rho _1 \circ \lambda \circ \rho ^{-1}_1 (\rho _1 (\psi )), \ldots , \rho _l \circ \lambda \circ \rho ^{-1}_l (\rho _l (\psi ))$ are also theorems. Therefore, we have

$$\begin{aligned} \dfrac{\rho _1 (\lambda (\psi )), \ldots , \rho _l (\lambda (\psi ))}{K_j \lambda (\psi )}. \end{aligned}$$

$\square$

If we build an MPIS $\mathcal {M}^c$ from the canonical model $\mathcal {N}^c$, then we say that we can filter $\mathcal {N}^c$ to $\mathcal {M}^c$. For every acceptable sequence $\alpha =\langle w_0, \ldots , w_t, \ldots \rangle$ of the possible worlds of $\mathcal {N}^c$ and every $w_t$ in $\alpha$, we build a possible world of $\mathcal {M}^c$, noted $h^{\alpha }(t)$. To capture such a mapping, we use the notation $w_t,\alpha \mapsto h^{\alpha }(t)$. Let int.act be an internal action on a given formula $\phi$ that returns all actions $A_i \ {\text {snd}} \ m$ and $A_i \ {\text {rcv}} \ m$ corresponding to the atomic formulae of the form $A_i \ {\text {snt}} \ m$ and $A_i \ {\text {rcvd}} \ m$ derivable from $\phi$. The internal action is not interpreted in TWS5 and is only used in the proof of completeness. To build $h^{\alpha }(t)$ from $\alpha$ and $w_t$, we first extract all atomic formulae in $w_t$ and add their corresponding actions to $h^{\alpha }(t)$. At the second step, for the formulae of the form $K_i \phi$, we take an internal action as described above. Figure 7 defines the filtration process.

Fig. 7

The filtration $w_t, \alpha \mapsto h^{\alpha }(t)$

We define $H^{c}$ to be $\bigcup _{\alpha ,t} h^{\alpha }(t)$. Assume that $w_t$ and $w_{t'}$ are maximal TWS5-consistent sets that appear in the acceptable sequences $\alpha$ and $\alpha '$, respectively. Moreover, assume that $w_{t_a}$ and $w_{t'_a}$ are their corresponding atomic formulae. We write $h^{\alpha }(t) \leadsto ^{\rho } h^{\alpha '}(t')$ if $\rho (w_{t_a})=w_{t'_a}$.

Lemma 5.4

Let the TWS5 model $\mathcal {M}^c=\langle H^c, \{\leadsto ^{\rho }_i\}, I^c \rangle$ be a filtration of the canonical model $\mathcal {N}^c=\langle W, \pi , \{\rightarrow ^{\rho }_i\}, \prec \rangle$. Moreover, let $\alpha =\langle w_0, \ldots , w_t, \ldots \rangle$ and $\alpha '=\langle w_{0'}, \ldots , w_{t'}, \ldots \rangle$ be two acceptable sequences of the possible worlds of $\mathcal {N}^c$. Whenever $w_t, \alpha \mapsto h^{\alpha }(t)$, we have

• (a) $h^{\alpha }(t) \in I^c(a(m))$ iff $\pi (w_t)(a(m))=true$ and $a(m) \in \Omega$.

• (b) If $(w_t, w_{t'}) \in \rightarrow ^{\rho }_i$, then there exists $w_{t''}$ in an acceptable sequence $\alpha ''$ of the possible worlds of $\mathcal {N}^c$ such that $w_{t'}, \alpha ' \mapsto h^{\alpha ''}(t'')$ and $h^{\alpha }(t) \leadsto ^{\rho }_i h^{\alpha ''}(t'')$.

• (c) If $h^{\alpha }(t) \leadsto ^{\rho }_i h^{\alpha '}(t')$, then there exists $w_{t''}$ in an acceptable sequence $\alpha ''$ of the possible worlds of $\mathcal {N}^c$ such that $w_{t''},\alpha '' \mapsto h^{\alpha '}(t')$ and $(\mathcal {N}^c, w_t) \models K_i \phi \Rightarrow (\mathcal {N}^c, w_{t''}) \models \rho (\phi )$.

• (d) If $(w_t, w_{t+1}) \in \prec$ with $w_{t+1}$ in $\alpha$, there exists an execution history $h^{\alpha }(t+1)$ such that $w_{t+1},\alpha \mapsto h^{\alpha }(t+1)$ and $h^{\alpha }(t) \subset h^{\alpha }(t+1)$.

• (e) If $h^{\alpha }(t) \subset h^{\alpha }(t+1)$, there exists an acceptable sequence $\alpha '$ equal to $\alpha$ up to $w_t$ such that $w_{t+1},\alpha ' \mapsto h^{\alpha }(t+1)$. Moreover, $(\mathcal {N}^c, w_{t+1}) \models \phi \Rightarrow (\mathcal {N}^c, w_t) \models \bigcirc \phi$.

Proof

(a) We give the proof for the case $a(m)=A_i \ {\text {rcvd}} \ m$.

$\pi (w_t)(A_i \ {\text {rcvd}} \ m)=true$

• $\Leftrightarrow A_i \ {\text {rcvd}} \ m \in w_t$

• $\Leftrightarrow K_i \ A_i \ {\text {rcvd}} \ m \in w_t \ \$ (Axioms A1 and T)

• $\Leftrightarrow A_i \ {\text {rcv}} \ m \in h^{\alpha }(t)|A_i \ \$ ($w_t, \alpha \mapsto h^{\alpha }(t)$)

• $\Leftrightarrow h^{\alpha }(t) \in I^c(A_i \ {\text {rcvd}} \ m)$.

(b) By $(w_t, w_{t'}) \in \rightarrow _i^{\rho }$ and the proof of Lemma 5.1 we have $\rho \triangleleft \kappa$ such that $A_i \ infers \ \kappa \in w_t$. We define $h^{\alpha ''}(t'')|A_i$ to be $\rho (h^{\alpha }(t)|A_i)$ and give the proof for $A_i \ {\text {snd}} \ m \in h^{\alpha }(t)|A_i$.

$A_i \ {\text {snd}} \ m \in h^{\alpha }(t)|A_i$

• $\Leftrightarrow K_i \ A_i \ {\text {snt}} \ m \in w_t \ \$ ($w_t,\alpha \mapsto h^{\alpha }(t)$)

• $\Leftrightarrow A_i \ {\text {snt}} \ \rho (m) \in w_{t'} \ \$ ($(w_t, w_{t'}) \in \rightarrow _i^{\rho }$)

• $\Leftrightarrow K_i \ A_i \ {\text {snt}} \ \rho (m) \in w_{t'} \ \$ (Axioms A1 and T)

• $\Leftrightarrow A_i \ {\text {snd}} \ \rho (m) \in h^{\alpha '}(t')|A_i \ \$ ($w_{t'}, \alpha ' \mapsto h^{\alpha '}(t')$).

(c) Let $w_{t_a}$ and $w_{t'_a}$ be the sets of the atomic formulae of the TWS5-consistent sets $w_t$ and $w_{t'}$, respectively. Since $h^{\alpha }(t) \leadsto ^{\rho }_i h^{\alpha '}(t')$, we have $\rho (w_{t_a})=w_{t'_a}$. Now, we have to show that the set $h^{\alpha '}(t') \cup \{\rho (\phi ) \ | \ K_i \phi \in w_t, \phi \in \mathcal {F} \}$ is TWS5-consistent. Let $h^{\alpha '}(t')=\{\rho (\theta _1), \ldots , \rho (\theta _k)\}$ and $\Delta =\{\rho (\phi _1), \ldots , \rho (\phi _l)\}$ be a finite subset of $\{\rho (\phi ) \ | \ K_i \phi \in w_t, \phi \in \mathcal {F}\}$. Now, we have to show that $h^{\alpha '}(t') \cup \Delta$ is TWS5-consistent, as otherwise $\rho (\theta _1, \ldots , \theta _k) \vdash \lnot \rho (\phi _1, \ldots , \phi _l)$. Since the message renaming function $\rho$ only applies to messages, we have $\vdash \rho ((\theta _1 \wedge \cdots \wedge \theta _k) \rightarrow \lnot (\phi _1 \wedge \cdots \wedge \phi _l))$. From Lemma 5.3, we can conclude that $\vdash \theta _1 \wedge \cdots \wedge \theta _k \rightarrow \lnot (\phi _1 \wedge \cdots \wedge \phi _l)$. Hence, the set $\{\theta _1, \ldots , \theta _k, \phi _1, \ldots , \phi _l \}$ is TWS5-inconsistent which is a contradiction. Let $w_{t''}$ be the maximal TWS5-consistent set containing $h^{\alpha '}(t') \cup \Delta$. For any $m \in \tau$ and $A_j \in \mathcal {A}$, consider the following two cases. In the first case, we give the proof for $\phi = A_j \ {\text {rcvd}} \ m$.

$(\mathcal {N}^c, w_t) \models K_i A_j \ {\text {rcvd}} \ m \$

• $\Rightarrow K_i A_j \ {\text {rcvd}} \ m \in w_t \ \$ (Lemma 5.1)

• $\Rightarrow A_j \ {\text {rcv}} \ m \in h^{\alpha }(t)|A_i \ \$ ($w_t, \alpha \mapsto h^{\alpha }(t)$)

• $\Rightarrow A_j \ {\text {rcv}} \ \rho (m) \in h^{\alpha '}(t')|A_i \ \$ ($h^{\alpha }(t) \leadsto _i^{\rho } h^{\alpha '}(t')$)

• $\Rightarrow A_j \ {\text {rcvd}} \ \rho (m) \in w_{t''} \ \$ ($w_{t''}, \alpha '' \mapsto h^{\alpha '}(t')$)

• $\Rightarrow (\mathcal {N}^c, w_{t''}) \models A_j \ {\text {rcvd}} \ \rho (m) \ \$ (Lemma 5.1).

  Now, we prove the second case where $\phi$ is not an atomic formula.

  $(\mathcal {N}^c, w_t) \models K_i \phi \ \$

• $\Rightarrow K_i \phi \in w_t \ \$ (Lemma 5.1)

• $\Rightarrow A_i \ int.act \ \phi \in h^{\alpha }(t)|A_i \ \$ ($w_t, \alpha \mapsto h^{\alpha }(t)$)

• $\Rightarrow A_i \ int.act \ \rho (\phi ) \in h^{\alpha '}(t')|A_i \ \$ ($h^{\alpha }(t) \leadsto _i^{\rho } h^{\alpha '}(t')$)

• $\Rightarrow K_i \rho (\phi ) \in w_{t''} \ \$ ($w_{t''}, \alpha '' \mapsto h^{\alpha '}(t')$)

• $\Rightarrow (\mathcal {N}^c, w_{t''}) \models K_i \rho (\phi ) \ \$ (Lemma 5.1)

(d) From the way $\mathcal {M}^c$ is constructed from $\mathcal {N}^c$, we can conclude that there exists $h^{\alpha }(t+1)$ such that $w_{t+1}, \alpha \mapsto h^{\alpha }(t+1)$. We give the proof when $A_i \ {\text {snd}} \ m \in h^{\alpha }(t)|A_i$.

$A_i \ {\text {snd}} \ m \in h^{\alpha }(t)|A_i$

• $\Rightarrow K_i \ A_i \ {\text {snt}} \ m \in w_t \ \$ ($w_t, \alpha \mapsto h^{\alpha }(t)$)

• $\Rightarrow A_i \ {\text {snt}} \ m \in w_t \ \$ (Axiom T)

• $\Rightarrow \bigcirc A_i \ {\text {snt}} \ m \in w_t \ \$ (Axiom TG)

• $\Rightarrow A_i \ {\text {snt}} \ m \in w_{t+1} \ \$ ($(w_t, w_{t+1}) \in \prec$).

• $\Rightarrow A_i \ {\text {snd}} \ m \in h^{\alpha }(t+1) | A_i \ \$ ($w_{t+1}, \alpha \mapsto h^{\alpha }(t+1)$)

(e) From the way $\mathcal {M}^c$ is constructed from $\mathcal {N}^c$, there exists a maximal TWS5-consistent set $w_{t+1}$ in $\alpha$ such that $w_{t+1}, \alpha \mapsto h^{\alpha }(t+1)$.

$(\mathcal {N}^c, w_{t+1}) \models \phi$

• $\Rightarrow \phi \in w_{t+1} \ \$ (Lemma 5.1)

• $\Rightarrow \bigcirc \phi \in w_{t} \ \$ ($(w_t, w_{t+1}) \in \prec$)

• $\Rightarrow (\mathcal {N}^c, w_t) \models \bigcirc \phi \ \$ (Lemma 5.1)

$\square$

Now, we prove that a TWS5 formula is valid with respect to $\mathcal {N}^c$ iff it is valid with respect to $\mathcal {M}^c$, and hence, it is satisfiable with respect to $\mathcal {M}_n$.

Lemma 5.5

Let the TWS5 model $\mathcal {M}^c=\langle H^c, \{\leadsto ^{\rho }_i\}, I^c \rangle$ be a filtration of the canonical model $\mathcal {N}^c=\langle W, \pi , \{\rightarrow ^{\rho }_i\}, \prec \rangle$. For any $\phi \in \mathcal {F}$ and every $w_t$ in any acceptable sequence $\alpha$ of possible worlds of $\mathcal {N}^c$, the following property holds.

$$\begin{aligned} (\mathcal {N}^c, w_t) \models \phi \; \mathrm{iff}\; (\mathcal {M}^c, h^{\alpha }(t)) \models \phi . \end{aligned}$$

Proof

The proof is by induction on the number of the logical operators in $\phi$. Assume that the property holds for all formulae with $n-1$ operators. We show that it also holds for any formula with n operators. The proof for atomic formulae and the ones with only $\lnot$ and $\wedge$ is trivial by Lemma 5.4a. Assume that $(\mathcal {M}^c, h^{\alpha }(t))\models K_i \psi$. As demonstrated in the proof of Lemma 5.4b, $(w_t, w_{t'}) \in \rightarrow _i^{\rho }$ implies that there exists $w_{t''}$ in an acceptable sequence $\alpha ''$ of the possible worlds of $\mathcal {N}^c$ such that $w_{t'}, \alpha ' \mapsto h^{\alpha ''}(t'')$ and $h^{\alpha }(t)\leadsto ^{\rho }_i h^{\alpha ''}(t'')$ where $h^{\alpha ''}(t'')$ can be taken $\rho (h^{\alpha }(t)|A_i)$. Therefore, for every $w_{t'} \in W$ in an acceptable sequence $\alpha '$ and any message renaming function $\rho :\tau \rightarrow \tau$, if $w_{t'}$ is an antecedent of $w_t$ induced by $\rho$, we have $h^{\alpha }(t) \leadsto _i^{\rho } h^{\alpha '}(t')$. This implies that $(\mathcal {M}^c,h^{\alpha '}(t')) \models \rho (\psi )$. By induction hypothesis, we have $(\mathcal {N}^c, w_{t'}) \models \rho (\psi )$. From Definition 4.6, we conclude that $(\mathcal {N}^c, w_t) \models K_i \psi$. Conversely, assume that $(\mathcal {N}^c, w_t)\models K_i \psi$. Using Lemma 5.4.c, for every $h^{\alpha '}(t') \in H^c$ and any message renaming function $\rho :\tau \rightarrow \tau$, if $h^{\alpha }(t) \leadsto _i^{\rho } h^{\alpha '}(t')$, then there exists $w_{t''} \in W$ in an acceptable sequence $\alpha ''$ such that $w_{t''}, \alpha '' \mapsto h^{\alpha '}(t')$ and $(\mathcal {N}^c, w_t)\models K_i \psi \Rightarrow (\mathcal {N}^c, w_{t''}) \models \rho (\psi )$. Therefore, $(\mathcal {N}^c, w_{t''}) \models \rho (\psi )$. By induction hypothesis, we have $(\mathcal {M}^c, h^{\alpha '}(t')) \models \rho (\phi )$. From Definition 4.6, $(\mathcal {M}^c, h^{\alpha }(t)) \models K_i \psi$.

Assume that $(\mathcal {N}^c, w_t)\models \bigcirc \psi$. For any $w_{t'}$ that is an antecedent of $w_t$ induced by $\prec$, $(w_t, w_{t+1}) \in \prec$, we have $(\mathcal {N}^c, w_{t+1})\models \psi$. From Lemma 5.4.d, there exists $h^{\alpha }(t+1) \in H$ such that $w_{t+1}, \alpha \mapsto h^{\alpha }(t+1)$. Induction hypothesis implies $(\mathcal {M}^c, h^{\alpha }(t+1))\models \psi$. From Definition 4.6, we have $(\mathcal {M}^c, h^{\alpha }(t))\models \bigcirc \psi$. Conversely, assume that $(\mathcal {M}^c, h^{\alpha }(t))\models \bigcirc \psi$. By Definition 4.6, we have $(\mathcal {M}^c, h^{\alpha }(t+1))\models \psi$. From Lemma 5.4.e, there exists an acceptable sequence $\alpha '$ equal to $\alpha$ up to $w_t$ such that $w_{t+1}, \alpha ' \mapsto h^{\alpha }(t+1)$. By induction hypothesis, we conclude that $(\mathcal {N}^c, w_{t+1})\models \psi$. Through applying Lemma 5.4.e another time, it can be concluded that $(\mathcal {N}^c, w_{t})\models \bigcirc \psi$. $\square$

Theorem 5.6

TWS5 is complete.

Proof

According to Theorem 5.2 and since $\mathcal {N}^c\in \mathcal {N}_n$, we conclude that every TWS5-consistent formula is satisfiable with respect to $\mathcal {N}^c$. According to Lemma 5.5, if $\mathcal {M}^c$ is the filtration model resulting from the canonical model $\mathcal {N}^c$, every TWS5-consistent formula is satisfiable with respect to $\mathcal {M}^c$. From Property 5.1 (on p. 12), $\mathcal {M}^c \in \mathcal {M}_n$ implies that every TWS5-consistent formula is satisfiable with respect to $\mathcal {M}_n$. This is equivalent to the completeness of TWS5. $\square$

6 Analyzing Some Example Protocols Using TWS5

In this section, we employ TWS5 to verify some authentication protocols. The first example is Lowe’s modified Wide-Mouth Frog protocol [26] shown in Fig. 8. In this protocol, A and B are two agents and S is a trusted server. The timestamps $t_a$ and $t_{\text {s}}$ are generated by A and S, respectively. The symmetric key $k_{as}$ is shared between A and S. Similarly, $k_{bs}$ is a symmetric key only known to B and S. The symmetric key $k_{ab}$ is generated by A and intended to serve as the session key between A and B. The random number $n_b$ is a nonce generated by B and ${\text {succ}}(n_b)$ is its successor. In this example, we assume that the roles of A and B can not be swapped as otherwise a message received by an agent could actually be sent by itself.

Fig. 8

Lowe’s wide-mouth frog protocol

Fig. 9

The properties we prove for the protocol shown in Fig. 8

Fig. 10

The specification of the protocol shown in Fig. 8

Now, we assume that the following set of statements hold for some $u,v \in \mathbb {N}$ where $u<v$.

$\Gamma = \big \{S \ {\text {rcvd}} \ A\cdot \{t_a.B.k_\mathrm{ab}\}_{k_\mathrm{as}}, \ \bigcirc ^u \ B \ {\text {rcvd}} \ \{t_{\text {s}}\cdot A\cdot k_{ab}\}_{k_{bs}}, \ \bigcirc ^{v} A \ {\text {rcvd}} \ \{n_b\}_{k_{ab}},$ $A \ \mathrm{infers} \ k_{ab}, k_{as} \ \mathrm{secret \ of} \ \{A, S\}, \ k_{bs} \ \mathrm{secret \ of} \ \{B, S\}, K_{\text {s}} \ \lnot {\text {unfresh}} \ t_a,$ $\bigcirc ^u K_B \lnot {\text {unfresh}} \ t_{\text {s}}\}.$

These assumptions are based on what agents have received through the protocol steps shown in Fig. 8. In the set of assumptions, the formula $k \ secret \ of \ G$ is a syntactic sugar defined by

$$\begin{aligned} k \ \mathrm{{secret}} \ \mathrm{{of}} \ G \leftrightarrow&\big ( \big ( \bigwedge _{A \in G} A \ \mathrm{{infers}} \ k \big ) \wedge \big (\bigwedge _{A \not \in G} \lnot \ A \ \mathrm{{infers}} \ k \big ) \big ). \end{aligned}$$

Moreover, $\bigcirc ^u \ B \ {\text {rcvd}} \ \{t_{\text {s}}\cdot A\cdot k_{ab}\}_{k_{bs}}$ means that $B \ {\text {rcvd}} \ \{t_{\text {s}}\cdot A\cdot k_{ab}\}_{k_{bs}}$ holds after u steps from the start of the protocol execution.

Fig. 11

Lowe’s wide-mouth frog protocol meets the properties in Fig. 9

We prove that Lowe’s modified Wide-Mouth Frog protocol meets the properties in Fig. 9. These properties collectively make the belief that A will be certain that B is communicating with A using the key A has generated in the first step of the protocol. To verify the protocol against these properties (requirements), we should first build a trust theory [3, 30, 31] comprising the assumptions made and the protocol specification. Figure 10 shows the protocol specification in terms of TWS5 formulae. In this specification A, B, and S range over $\mathcal {A}$ including attackers. The formula $S_1$ says that if a server S receives a packet of the form $A\cdot \{t_a\cdot B\cdot k_{ab}\}$ and it knows that the timestamp $t_a$ is not unfresh by checking its own clock, then at the next step it will send a packet of the form $\{t_{\text {s}}\cdot A\cdot k_{ab}\}_{k_{bs}}$. The formulae $S_2$ and $S_3$ reflect similar facts. Let $Tr=\{S_1, S_2, S3\} \cup \Gamma$ be the trust theory of the protocol in Fig. 8. We should prove that the properties shown in Fig. 9 hold in each execution of the protocol under this trust theory. The proofs are given in Fig. 11.

Fig. 12

Executions $h_1$ and $h_2$ of the protocol shown in Fig. 1 with mode m([1,4],2)

The Second example is the protocol of Sect. 2 which operates in the mode m([1, 4], 2). Two executions of this protocol are shown in Fig. 12 where it is assumed that $h_1(t-3)=h_2(t-3)$. Moreover, the model of the protocol is denoted by $\mathcal {M}$. Let $\rho$ be a message renaming function such that $\rho (\{m_i\}_{k_{\text {s}}})=\{m'_i\}_{k_{\text {c}}}$, $\rho (\{m'_i\}_{k_{\text {c}}})=\{m_i\}_{k_{\text {s}}}$, and $\rho (m)=m$ for other messages. As R does not infer the keys $k_{\text {s}}$ and $k_{\text {c}}$, this message renaming function is consistent with the keys R infers. Now, Since $h_1(t+1) \leadsto ^{\rho }_R h_2(t+4)$, we have

$$\begin{aligned}&(\mathcal {M},h_1(t+1)) \not \models K_R \ S \ {\text {snt}} \ \{m_i\}_{k_{\text {s}}}\cdot f(k_{i+1})\nonumber \\&\quad \cdot k_{i-1}\cdot {\text {mac}}(g(k_i)\cdot \{m_i\}_{k_{\text {s}}}\cdot f(k_{i+1}). k_{i-1})\cdot \end{aligned}$$

(6.1)

Since TWS5 is complete, (6.1) implies that the protocol does not fulfill the intended requirement. Note that in this example, we need to update the message algebra for specifying mac and the protocol.

7 Conclusion

We have presented an omniscience-free and complete temporal logic of knowledge for verifying authentication protocols. By this logic, in particular, one can analyze those protocols whose successful operation highly depends on timely actions by the principals involved in the protocol. The application of this logic to some example protocols evidences its capacity for verifying different kinds of authentication protocols. There is still much to be done. Developing an automated prover based on this logic is among the topics deserving future research.